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/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean

@@ -255,19 +255,19 @@ The formalization below confirms that this assumption is sufficient.
 The unique factorization theorem says that any natural number other
 than zero can be written as the product of primes in a unique way.
 Mathlib contains a formal version of this, expressed in terms of a function
-``Nat.factors``, which returns the list of
+``Nat.primeFactorsList``, which returns the list of
 prime factors of a number in nondecreasing order.
-The library proves that all the elements of ``Nat.factors n``
+The library proves that all the elements of ``Nat.primeFactorsList n``
 are prime, that any ``n`` greater than zero is equal to the
 product of its factors,
 and that if ``n`` is equal to the product of another list of prime numbers,
-then that list is a permutation of ``Nat.factors n``.
+then that list is a permutation of ``Nat.primeFactorsList n``.
 EXAMPLES: -/
 -- QUOTE:
-#check Nat.factors
-#check Nat.prime_of_mem_factors
-#check Nat.prod_factors
-#check Nat.factors_unique
+#check Nat.primeFactorsList
+#check Nat.prime_of_mem_primeFactorsList
+#check Nat.prod_primeFactorsList
+#check Nat.primeFactorsList_unique
 -- QUOTE.
 
 /- TEXT:

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

@@ -2,7 +2,7 @@
 import Mathlib.RingTheory.Ideal.QuotientOperations
 import Mathlib.RingTheory.Localization.Basic
 import Mathlib.RingTheory.DedekindDomain.Ideal
-import Mathlib.Analysis.Complex.Polynomial
+import Mathlib.Analysis.Complex.Polynomial.Basic
 import Mathlib.Data.ZMod.Quotient
 import MIL.Common
 
@@ -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/C10_Topology/S02_Metric_Spaces.lean

@@ -1,6 +1,6 @@
 import MIL.Common
 import Mathlib.Topology.Instances.Real
-import Mathlib.Analysis.NormedSpace.BanachSteinhaus
+import Mathlib.Analysis.Normed.Operator.BanachSteinhaus
 
 open Set Filter
 open Topology Filter
@@ -285,12 +285,12 @@ example {s : Set X} (hs : IsCompact s) {u : ℕ → X} (hu : ∀ n, u n ∈ s) :
 example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ}
       (hfs : ContinuousOn f s) :
     ∃ x ∈ s, ∀ y ∈ s, f x ≤ f y :=
-  hs.exists_forall_le hs' hfs
+  hs.exists_isMinOn hs' hfs
 
 example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ}
       (hfs : ContinuousOn f s) :
     ∃ x ∈ s, ∀ y ∈ s, f y ≤ f x :=
-  hs.exists_forall_ge hs' hfs
+  hs.exists_isMaxOn hs' hfs
 
 example {s : Set X} (hs : IsCompact s) : IsClosed s :=
   hs.isClosed
@@ -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

MIL/C10_Topology/S03_Topological_Spaces.lean

@@ -1,6 +1,6 @@
 import MIL.Common
 import Mathlib.Topology.Instances.Real
-import Mathlib.Analysis.NormedSpace.BanachSteinhaus
+import Mathlib.Analysis.Normed.Operator.BanachSteinhaus
 
 open Set Filter Topology
 

MIL/C11_Differential_Calculus/S02_Differential_Calculus_in_Normed_Spaces.lean

@@ -1,6 +1,6 @@
 import MIL.Common
-import Mathlib.Analysis.NormedSpace.BanachSteinhaus
-import Mathlib.Analysis.NormedSpace.FiniteDimension
+import Mathlib.Analysis.Normed.Operator.BanachSteinhaus
+import Mathlib.Analysis.Normed.Module.FiniteDimension
 import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
 import Mathlib.Analysis.Calculus.ContDiff.RCLike
 import Mathlib.Analysis.Calculus.FDeriv.Prod

MIL/C12_Integration_and_Measure_Theory/S02_Measure_Theory.lean

@@ -1,5 +1,5 @@
 import MIL.Common
-import Mathlib.Analysis.NormedSpace.FiniteDimension
+import Mathlib.Analysis.Normed.Module.FiniteDimension
 import Mathlib.Analysis.Convolution
 import Mathlib.MeasureTheory.Function.Jacobian
 import Mathlib.MeasureTheory.Integral.Bochner

MIL/C12_Integration_and_Measure_Theory/S03_Integration.lean

@@ -1,5 +1,5 @@
 import MIL.Common
-import Mathlib.Analysis.NormedSpace.FiniteDimension
+import Mathlib.Analysis.Normed.Module.FiniteDimension
 import Mathlib.Analysis.Convolution
 import Mathlib.MeasureTheory.Function.Jacobian
 import Mathlib.MeasureTheory.Integral.Bochner

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "937cd3219c0beffa7b623d2905707d1304da259e",
+   "rev": "31fb27d6b89dc94cf7349df247fc44d2a1d130af",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
+   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
+   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,27 +35,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.39",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3ecbc03527e97b43b4d52ae2deca999b58b43b34",
+   "rev": "9969491998149c8810b296185d71fcf1c23b2f1c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

lean-toolchain

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