Bump Lean and Mathlib

MIL/C04_Sets_and_Functions/S01_Sets.lean

@@ -347,13 +347,16 @@ def odds : Set ℕ :=
 example : evens ∪ odds = univ := by
   rw [evens, odds]
   ext n
-  simp
+  simp [-Nat.not_even_iff_odd]
   apply Classical.em
 -- QUOTE.
 
 /- TEXT:
 You should step through this proof and make sure
 you understand what is going on.
+Note we tell the simplifier to *not* use the lemma
+``Nat.not_even_iff`` because we want to keep
+``¬ Even n`` in our goal.
 Try deleting the line ``rw [evens, odds]``
 and confirm that the proof still works.
 
@@ -385,7 +388,7 @@ Use ``intro n`` to unfold the definition of subset,
 and use the simplifier to reduce the
 set-theoretic constructions to logic.
 We also recommend using the theorems
-``Nat.Prime.eq_two_or_odd`` and ``Nat.even_iff``.
+``Nat.Prime.eq_two_or_odd`` and ``Nat.odd_iff``.
 TEXT. -/
 -- QUOTE:
 example : { n | Nat.Prime n } ∩ { n | n > 2 } ⊆ { n | ¬Even n } := by
@@ -396,13 +399,11 @@ example : { n | Nat.Prime n } ∩ { n | n > 2 } ⊆ { n | ¬Even n } := by
 example : { n | Nat.Prime n } ∩ { n | n > 2 } ⊆ { n | ¬Even n } := by
   intro n
   simp
-  intro nprime
+  intro nprime n_gt
   rcases Nat.Prime.eq_two_or_odd nprime with h | h
   · rw [h]
-    intro
     linarith
-  rw [Nat.even_iff, h]
-  norm_num
+  · rw [Nat.odd_iff, h]
 
 /- TEXT:
 Be careful: it is somewhat confusing that the library has multiple versions

MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean

@@ -179,7 +179,7 @@ instance instCommRing : CommRing GaussInt where
   add_zero := by
     intro
     ext <;> simp
-  add_left_neg := by
+  neg_add_cancel := by
     intro
     ext <;> simp
   add_comm := by

MIL/C07_Hierarchies/S02_Morphisms.lean

@@ -234,7 +234,7 @@ class MonoidHomClass₃ (F : Type) (M N : outParam Type) [Monoid M] [Monoid N] e
 
 instance (M N : Type) [Monoid M] [Monoid N] : MonoidHomClass₃ (MonoidHom₁ M N) M N where
   coe := MonoidHom₁.toFun
-  coe_injective' := MonoidHom₁.ext
+  coe_injective' _ _ := MonoidHom₁.ext
   map_one := MonoidHom₁.map_one
   map_mul := MonoidHom₁.map_mul
 -- QUOTE.
@@ -272,15 +272,15 @@ extends DFunLike F α (fun _ ↦ β) where
 instance (α β : Type) [LE α] [LE β] : OrderPresHomClass (OrderPresHom α β) α β where
 -- SOLUTIONS:
   coe := OrderPresHom.toFun
-  coe_injective' := OrderPresHom.ext
+  coe_injective' _ _ := OrderPresHom.ext
   le_of_le := OrderPresHom.le_of_le
 -- BOTH:
 
 instance (α β : Type) [LE α] [Monoid α] [LE β] [Monoid β] :
     OrderPresHomClass (OrderPresMonoidHom α β) α β where
 -- SOLUTIONS:
   coe := fun f ↦ f.toOrderPresHom.toFun
-  coe_injective' := OrderPresMonoidHom.ext
+  coe_injective' _ _ := OrderPresMonoidHom.ext
   le_of_le := fun f ↦ f.toOrderPresHom.le_of_le
 -- BOTH:
 
@@ -291,7 +291,7 @@ instance (α β : Type) [LE α] [Monoid α] [LE β] [Monoid β] :
 SOLUTIONS: -/
 where
   coe := fun f ↦ f.toOrderPresHom.toFun
-  coe_injective' := OrderPresMonoidHom.ext
+  coe_injective' _ _ := OrderPresMonoidHom.ext
   map_one := fun f ↦ f.toMonoidHom₁.map_one
   map_mul := fun f ↦ f.toMonoidHom₁.map_mul
 -- QUOTE.

MIL/C07_Hierarchies/S03_Subobjects.lean

@@ -1,5 +1,5 @@
 import MIL.Common
-import Mathlib.GroupTheory.QuotientGroup
+import Mathlib.GroupTheory.QuotientGroup.Basic
 
 set_option autoImplicit true
 
@@ -34,7 +34,7 @@ structure Submonoid₁ (M : Type) [Monoid M] where
 /-- Submonoids in `M` can be seen as sets in `M`. -/
 instance [Monoid M] : SetLike (Submonoid₁ M) M where
   coe := Submonoid₁.carrier
-  coe_injective' := Submonoid₁.ext
+  coe_injective' _ _ := Submonoid₁.ext
 
 -- QUOTE.
 
@@ -125,12 +125,12 @@ structure Subgroup₁ (G : Type) [Group G] extends Submonoid₁ G where
 /-- Subgroups in `M` can be seen as sets in `M`. -/
 instance [Group G] : SetLike (Subgroup₁ G) G where
   coe := fun H ↦ H.toSubmonoid₁.carrier
-  coe_injective' := Subgroup₁.ext
+  coe_injective' _ _ := Subgroup₁.ext
 
 instance [Group G] (H : Subgroup₁ G) : Group H :=
 { SubMonoid₁Monoid H.toSubmonoid₁ with
   inv := fun x ↦ ⟨x⁻¹, H.inv_mem x.property⟩
-  mul_left_inv := fun x ↦ SetCoe.ext (mul_left_inv (x : G)) }
+  inv_mul_cancel := fun x ↦ SetCoe.ext (inv_mul_cancel (x : G)) }
 
 class SubgroupClass₁ (S : Type) (G : Type) [Group G] [SetLike S G]
     extends SubmonoidClass₁ S G  : Prop where

MIL/C08_Groups_and_Rings/S02_Rings.lean

@@ -539,8 +539,9 @@ open Complex Polynomial
 example : aroots (X ^ 2 + 1 : ℝ[X]) ℂ = {Complex.I, -I} := by
   suffices roots (X ^ 2 + 1 : ℂ[X]) = {I, -I} by simpa [aroots_def]
   have factored : (X ^ 2 + 1 : ℂ[X]) = (X - C I) * (X - C (-I)) := by
+    have key : (C I * C I : ℂ[X]) = -1 := by simp [← C_mul]
     rw [C_neg]
-    linear_combination show (C I * C I : ℂ[X]) = -1 by simp [← C_mul]
+    linear_combination key
   have p_ne_zero : (X - C I) * (X - C (-I)) ≠ 0 := by
     intro H
     apply_fun eval 0 at H

MIL/C09_Topology/S02_Metric_Spaces.lean

@@ -370,7 +370,7 @@ example {X : Type*} [MetricSpace X] [CompactSpace X] {Y : Type*} [MetricSpace Y]
     intro x y _
     have : (x, y) ∉ K := by simp [hK]
     simpa [K] using this
-  · rcases K_cpct.exists_forall_le hK continuous_dist.continuousOn with ⟨⟨x₀, x₁⟩, xx_in, H⟩
+  · rcases K_cpct.exists_isMinOn hK continuous_dist.continuousOn with ⟨⟨x₀, x₁⟩, xx_in, H⟩
     use dist x₀ x₁
     constructor
     · change _ < _
@@ -380,8 +380,8 @@ example {X : Type*} [MetricSpace X] [CompactSpace X] {Y : Type*} [MetricSpace Y]
       linarith
     · intro x x'
       contrapose!
-      intro hxx'
-      exact H (x, x') hxx'
+      intro (hxx' : (x, x') ∈ K)
+      exact H hxx'
 
 /- TEXT:
 Completeness

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "41bc768e2224d6c75128a877f1d6e198859b3178",
+   "rev": "31fb27d6b89dc94cf7349df247fc44d2a1d130af",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5",
+   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6058ab8d938c5104eace7d0fb5ac17b21cb067b1",
+   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c87908619cccadda23f71262e6898b9893bffa36",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.40",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e7e90d90a62e6d12cbb27cbbfc31c094ee4ecc58",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "10a631f1d3d9d99b990791ca0a251a5e78a15d84",
+   "rev": "9969491998149c8810b296185d71fcf1c23b2f1c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.10.0
+leanprover/lean4:v4.11.0-rc2