upgrade to latest mathlib and Lean 3.23.0

conf.py

@@ -54,9 +54,9 @@
 # built documents.
 #
 # The short X.Y version.
-version = u'3.20.0'
+version = u'3.23.0'
 # The full version, including alpha/beta/rc tags.
-release = u'3.20.0'
+release = u'3.23.0'
 
 # The language for content autogenerated by Sphinx. Refer to documentation
 # for a list of supported languages.

leanpkg.toml

@@ -1,8 +1,8 @@
 [package]
 name = "theorem_proving_in_lean"
 version = "0.1"
-lean_version = "leanprover-community/lean:3.20.0"
+lean_version = "leanprover-community/lean:3.23.0"
 path = "src"
 
 [dependencies]
-mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "565efec29c97cd6d523fb959379de8e41cfcec04"}
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "eba2a79649144a8e1922bab3d5fe988955c82397"}

quantifiers_and_equality.rst

@@ -841,40 +841,9 @@ Exercises
 
    .. code-block:: lean
 
-<<<<<<< HEAD
        import data.nat.basic
-=======
-       namespace hidden
 
-       def divides (m n : ℕ) : Prop := ∃ k, m * k = n
-
-       instance : has_dvd nat := ⟨divides⟩
-
-       def even (n : ℕ) : Prop := 2 ∣ n -- You can enter the '∣' character by typing \mid
-
-       section
-       variables m n : ℕ
-
-       #check m ∣ n
-       #check m^n
-       #check even (m^n +3)
-       end
-
-       end hidden
-
-   Remember that, without any parameters, an expression of type ``Prop`` is just an assertion. Fill in the definitions of ``prime`` and ``Fermat_prime`` below, and construct the given assertion. For example, you can say that there are infinitely many primes by asserting that for every natural number ``n``, there is a prime number greater than ``n``. Goldbach's weak conjecture states that every odd number greater than 5 is the sum of three primes. Look up the definition of a Fermat prime or any of the other statements, if necessary.
-
-   .. code-block:: lean
-
-       namespace hidden
-
-       def divides (m n : ℕ) : Prop := ∃ k, m * k = n
-
-       instance : has_dvd nat := ⟨divides⟩
->>>>>>> Don't indent for sections and namespaces.
-
-       -- You can enter the '∣' character by typing \mid
-       def even (n : ℕ) : Prop := 2 ∣ n
+       #check even
 
        def prime (n : ℕ) : Prop := sorry