Bump Lean+Mathlib

MIL/C01_Introduction/S02_Overview.lean

@@ -1,4 +1,3 @@
-import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Nat.Parity
 import MIL.Common
 

MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean

@@ -237,7 +237,7 @@ TEXT. -/
 -- QUOTE.
 
 /- TEXT:
-Use it to prove the following variant:
+Use it to prove the following variant, using also ``add_sub_cancel_right``:
 TEXT. -/
 -- QUOTE:
 -- BOTH:
@@ -250,7 +250,7 @@ SOLUTIONS: -/
     _ ≤ |a - b| + |b| - |b| := by
       apply sub_le_sub_right
       apply abs_add
-    _ ≤ |a - b| := by rw [add_sub_cancel]
+    _ ≤ |a - b| := by rw [add_sub_cancel_right]
 
 
 -- alternatively

MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean

@@ -258,10 +258,10 @@ section
 variable {α : Type*} [DistribLattice α]
 variable (x y z : α)
 
-#check (inf_sup_left : x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z)
-#check (inf_sup_right : (x ⊔ y) ⊓ z = x ⊓ z ⊔ y ⊓ z)
-#check (sup_inf_left : x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z))
-#check (sup_inf_right : x ⊓ y ⊔ z = (x ⊔ z) ⊓ (y ⊔ z))
+#check (inf_sup_left x y z : x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z)
+#check (inf_sup_right x y z : (x ⊔ y) ⊓ z = x ⊓ z ⊔ y ⊓ z)
+#check (sup_inf_left x y z : x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z))
+#check (sup_inf_right x y z : x ⊓ y ⊔ z = (x ⊔ z) ⊓ (y ⊔ z))
 -- QUOTE.
 end
 

MIL/C03_Logic/S02_The_Existential_Quantifier.lean

@@ -420,7 +420,7 @@ example {c : ℝ} : Surjective fun x ↦ x + c := by
 -- QUOTE.
 
 /- TEXT:
-Try this example yourself using the theorem ``mul_div_cancel'``.:
+Try this example yourself using the theorem ``mul_div_cancel₀``.:
 TEXT. -/
 -- QUOTE:
 example {c : ℝ} (h : c ≠ 0) : Surjective fun x ↦ c * x := by
@@ -431,12 +431,12 @@ example {c : ℝ} (h : c ≠ 0) : Surjective fun x ↦ c * x := by
 example {c : ℝ} (h : c ≠ 0) : Surjective fun x ↦ c * x := by
   intro x
   use x / c
-  dsimp; rw [mul_div_cancel' _ h]
+  dsimp; rw [mul_div_cancel₀ _ h]
 
 example {c : ℝ} (h : c ≠ 0) : Surjective fun x ↦ c * x := by
   intro x
   use x / c
-  field_simp [h] ; ring
+  field_simp
 
 /- TEXT:
 .. index:: field_simp, tactic ; field_simp

MIL/C03_Logic/S06_Sequences_and_Convergence.lean

@@ -227,7 +227,7 @@ theorem convergesTo_mul_constαα {s : ℕ → ℝ} {a : ℝ} (c : ℝ) (cs : Co
   calc
     |c * s n - c * a| = |c| * |s n - a| := by rw [← abs_mul, mul_sub]
     _ < |c| * (ε / |c|) := (mul_lt_mul_of_pos_left (hs n ngt) acpos)
-    _ = ε := mul_div_cancel' _ (ne_of_lt acpos).symm
+    _ = ε := mul_div_cancel₀ _ (ne_of_lt acpos).symm
 
 /- TEXT:
 The next theorem is also independently interesting:
@@ -299,7 +299,7 @@ theorem auxαα {s t : ℕ → ℝ} {a : ℝ} (cs : ConvergesTo s a) (ct : Conve
   calc
     |s n * t n - 0| = |s n| * |t n - 0| := by rw [sub_zero, abs_mul, sub_zero]
     _ < B * (ε / B) := (mul_lt_mul'' (h₀ n ngeN₀) (h₁ n ngeN₁) (abs_nonneg _) (abs_nonneg _))
-    _ = ε := mul_div_cancel' _ (ne_of_lt Bpos).symm
+    _ = ε := mul_div_cancel₀ _ (ne_of_lt Bpos).symm
 
 /- TEXT:
 If you have made it this far, congratulations!
@@ -379,7 +379,7 @@ theorem convergesTo_uniqueαα {s : ℕ → ℝ} {a b : ℝ}
     _ ≤ |(-(s N - a))| + |s N - b| := (abs_add _ _)
     _ = |s N - a| + |s N - b| := by rw [abs_neg]
     _ < ε + ε := (add_lt_add absa absb)
-    _ = |a - b| := by norm_num
+    _ = |a - b| := by norm_num [ε]
 
   exact lt_irrefl _ this
 

MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean

@@ -245,7 +245,7 @@ theorem sb_injective (hf : Injective f) : Injective (sbFun f g) := by
     · symm
       apply this hxeq.symm xA.symm (xA.resolve_left x₁A)
     have x₂A : x₂ ∈ A := by
-      apply not_imp_self.mp
+      apply _root_.not_imp_self.mp
       intro (x₂nA : x₂ ∉ A)
       rw [if_pos x₁A, if_neg x₂nA] at hxeq
       rw [A_def, sbSet, mem_iUnion] at x₁A

MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean

@@ -452,8 +452,6 @@ variable (r : ℚ)
 #check r.pos
 #check r.reduced
 
-#check Rat.num_den'
-
 end
 
 -- example (r : ℚ) : r ^ 2 ≠ 2 := by

MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean

@@ -146,7 +146,8 @@ function.
 It turns out to be easier to start with a proof by cases,
 so that the remainder of the proof starts with the case
 :math:`n = 1`.
-See if you can complete the argument with a proof by induction.
+See if you can complete the argument with a proof by induction using ``pow_succ``
+or ``pow_succ'``.
 BOTH: -/
 -- QUOTE:
 theorem pow_two_le_fac (n : ℕ) : 2 ^ (n - 1) ≤ fac n := by
@@ -158,7 +159,7 @@ SOLUTIONS: -/
   induction' n with n ih
   · simp [fac]
   simp at *
-  rw [pow_succ, fac]
+  rw [pow_succ', fac]
   apply Nat.mul_le_mul _ ih
   repeat' apply Nat.succ_le_succ
   apply zero_le
@@ -280,7 +281,7 @@ theorem sum_id (n : ℕ) : ∑ i in range (n + 1), i = n * (n + 1) / 2 := by
   symm; apply Nat.div_eq_of_eq_mul_right (by norm_num : 0 < 2)
   induction' n with n ih
   · simp
-  rw [Finset.sum_range_succ, mul_add 2, ← ih, Nat.succ_eq_add_one]
+  rw [Finset.sum_range_succ, mul_add 2, ← ih]
   ring
 -- QUOTE.
 
@@ -297,7 +298,7 @@ SOLUTIONS: -/
   apply Nat.div_eq_of_eq_mul_right (by norm_num : 0 < 6)
   induction' n with n ih
   · simp
-  rw [Finset.sum_range_succ, mul_add 6, ← ih, Nat.succ_eq_add_one]
+  rw [Finset.sum_range_succ, mul_add 6, ← ih]
   ring
 -- QUOTE.
 

MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean

@@ -1,5 +1,5 @@
 import Mathlib.Data.Nat.Prime
-import Mathlib.Algebra.BigOperators.Order
+import Mathlib.Algebra.BigOperators.Basic
 import MIL.Common
 
 open BigOperators
@@ -484,22 +484,21 @@ the facts about this function that we will need to use below.
 The first named theorem is another illustration of reasoning by
 a small number of cases.
 In the second named theorem, remember that the semicolon means that
-the subsequent tactic block is applied to both of the goals
-that result from the application of ``two_le``.
+the subsequent tactic block is applied to all the goals created by the
+preceding tactic.
 EXAMPLES: -/
 -- QUOTE:
 example (n : ℕ) : (4 * n + 3) % 4 = 3 := by
   rw [add_comm, Nat.add_mul_mod_self_left]
-  norm_num
 
 -- BOTH:
 theorem mod_4_eq_3_or_mod_4_eq_3 {m n : ℕ} (h : m * n % 4 = 3) : m % 4 = 3 ∨ n % 4 = 3 := by
   revert h
   rw [Nat.mul_mod]
   have : m % 4 < 4 := Nat.mod_lt m (by norm_num)
-  interval_cases hm : m % 4 <;> simp [hm]
+  interval_cases m % 4 <;> simp [-Nat.mul_mod_mod]
   have : n % 4 < 4 := Nat.mod_lt n (by norm_num)
-  interval_cases hn : n % 4 <;> simp [hn]
+  interval_cases n % 4 <;> simp
 
 theorem two_le_of_mod_4_eq_3 {n : ℕ} (h : n % 4 = 3) : 2 ≤ n := by
   apply two_le <;>
@@ -605,7 +604,6 @@ theorem primes_mod_4_eq_3_infinite : ∀ n, ∃ p > n, Nat.Prime p ∧ p % 4 = 3
     sorry
 SOLUTIONS: -/
     rw [add_comm, Nat.add_mul_mod_self_left]
-    norm_num
 -- BOTH:
   rcases exists_prime_factor_mod_4_eq_3 h₁ with ⟨p, pp, pdvd, p4eq⟩
   have ps : p ∈ s := by

MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean

@@ -1,4 +1,3 @@
-import Mathlib.Data.Int.Basic
 import Mathlib.Algebra.EuclideanDomain.Basic
 import Mathlib.RingTheory.PrincipalIdealDomain
 import MIL.Common
@@ -152,11 +151,15 @@ that appears in VS Code, and then ask Lean to fill in a skeleton for the
 structure definition, you will see a scary number of entries.
 Jumping to the definition of the structure, however, shows that many of the
 fields have default definitions that Lean will fill in for you automatically.
-The essential ones appear in the definition below. In each case, the relevant
+The essential ones appear in the definition below.
+A special case are ``nsmul`` and ``zsmul`` which should be ignored for now
+and will be explained in the next chapter.
+In each case, the relevant
 identity is proved by unfolding definitions, using the ``ext`` tactic
 to reduce the identities to their real and imaginary components,
 simplifying, and, if necessary, carrying out the relevant ring calculation in
-the integers.
+the integers. Note that we could easily avoid repeating all this code, but
+this is not the topic of the current discussion.
 BOTH: -/
 -- QUOTE:
 instance instCommRing : CommRing gaussInt where
@@ -165,6 +168,8 @@ instance instCommRing : CommRing gaussInt where
   add := (· + ·)
   neg x := -x
   mul := (· * ·)
+  nsmul := nsmulRec
+  zsmul := zsmulRec
   add_assoc := by
     intros
     ext <;> simp <;> ring
@@ -198,8 +203,12 @@ instance instCommRing : CommRing gaussInt where
   mul_comm := by
     intros
     ext <;> simp <;> ring
-  zero_mul := sorry
-  mul_zero := sorry
+  zero_mul := by
+    intros
+    ext <;> simp
+  mul_zero := by
+    intros
+    ext <;> simp
 -- QUOTE.
 
 @[simp]
@@ -631,7 +640,7 @@ instance : EuclideanDomain gaussInt :=
     quotient := (· / ·)
     remainder := (· % ·)
     quotient_mul_add_remainder_eq :=
-      fun x y ↦ by simp only; rw [mod_def, add_comm, sub_add_cancel]
+      fun x y ↦ by simp only; rw [mod_def, add_comm] ; ring
     quotient_zero := fun x ↦ by
       simp [div_def, norm, Int.div']
       rfl

MIL/C08_Groups_and_Rings/S01_Groups.lean

@@ -826,6 +826,9 @@ open MonoidHom
 #check Subgroup.index_mul_card
 #check Nat.eq_of_mul_eq_mul_right
 
+-- The following line is working around a Lean bug that will be fixed very soon.
+attribute [-instance] Subtype.instInhabited
+
 lemma aux_card_eq [Fintype G] (h' : card G = card H * card K) : card (G ⧸ H) = card K := by
 /- EXAMPLES:
   sorry

MIL/C08_Groups_and_Rings/S02_Rings.lean

@@ -336,7 +336,6 @@ SOLUTIONS: -/
     replace he : ∀ j, j ≠ i → e ∈ I j := by simpa using he
     refine ⟨e, ?_, ?_⟩
     · simp [eq_sub_of_add_eq' hue, map_sub, eq_zero_iff_mem.mpr hu]
-      rfl
     · exact fun j hj ↦ eq_zero_iff_mem.mpr (he j hj)
 -- BOTH:
   choose e he using key

MIL/C09_Topology/S02_Metric_Spaces.lean

@@ -369,14 +369,14 @@ example {X : Type*} [MetricSpace X] [CompactSpace X] {Y : Type*} [MetricSpace Y]
   · use 1, by norm_num
     intro x y _
     have : (x, y) ∉ K := by simp [hK]
-    simpa using this
+    simpa [K] using this
   · rcases K_cpct.exists_forall_le hK continuous_dist.continuousOn with ⟨⟨x₀, x₁⟩, xx_in, H⟩
     use dist x₀ x₁
     constructor
     · change _ < _
       rw [dist_pos]
       intro h
-      have : ε ≤ 0 := by simpa [*] using xx_in
+      have : ε ≤ 0 := by simpa [K, φ, *] using xx_in
       linarith
     · intro x x'
       contrapose!

MIL/C10_Differential_Calculus/S02_Differential_Calculus_in_Normed_Spaces.lean

@@ -2,7 +2,7 @@ import MIL.Common
 import Mathlib.Analysis.NormedSpace.BanachSteinhaus
 import Mathlib.Analysis.NormedSpace.FiniteDimension
 import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
-import Mathlib.Analysis.Calculus.ContDiff.IsROrC
+import Mathlib.Analysis.Calculus.ContDiff.RCLike
 import Mathlib.Analysis.Calculus.FDeriv.Prod
 
 
@@ -169,7 +169,7 @@ into a normed space is pointwise
 bounded, then the norms of these linear maps are uniformly bounded.
 The main ingredient is Baire's theorem
 ``nonempty_interior_of_iUnion_of_closed``. (You proved a version of this in the topology chapter.)
-Minor ingredients include ``continuous_linear_map.op_norm_le_of_shell``,
+Minor ingredients include ``continuous_linear_map.opNorm_le_of_shell``,
 ``interior_subset`` and ``interior_iInter_subset`` and ``is_closed_le``.
 BOTH: -/
 section
@@ -200,7 +200,7 @@ example {ι : Type*} [CompleteSpace E] {g : ι → E →L[𝕜] F} (h : ∀ x, 
   have real_norm_le : ∀ z ∈ ball x ε, ∀ (i : ι), ‖g i z‖ ≤ m
   sorry
   have εk_pos : 0 < ε / ‖k‖ := sorry
-  refine' ⟨(m + m : ℕ) / (ε / ‖k‖), fun i ↦ ContinuousLinearMap.op_norm_le_of_shell ε_pos _ hk _⟩
+  refine' ⟨(m + m : ℕ) / (ε / ‖k‖), fun i ↦ ContinuousLinearMap.opNorm_le_of_shell ε_pos _ hk _⟩
   sorry
   sorry
 -- QUOTE.
@@ -230,11 +230,11 @@ example {ι : Type*} [CompleteSpace E] {g : ι → E →L[𝕜] F} (h : ∀ x, 
     replace hz := mem_iInter.mp (interior_iInter_subset _ (hε hz)) i
     apply interior_subset hz
   have εk_pos : 0 < ε / ‖k‖ := div_pos ε_pos (zero_lt_one.trans hk)
-  refine' ⟨(m + m : ℕ) / (ε / ‖k‖), fun i ↦ ContinuousLinearMap.op_norm_le_of_shell ε_pos _ hk _⟩
+  refine' ⟨(m + m : ℕ) / (ε / ‖k‖), fun i ↦ ContinuousLinearMap.opNorm_le_of_shell ε_pos _ hk _⟩
   · exact div_nonneg (Nat.cast_nonneg _) εk_pos.le
   intro y le_y y_lt
   calc
-    ‖g i y‖ = ‖g i (y + x) - g i x‖ := by rw [(g i).map_add, add_sub_cancel]
+    ‖g i y‖ = ‖g i (y + x) - g i x‖ := by rw [(g i).map_add, add_sub_cancel_right]
     _ ≤ ‖g i (y + x)‖ + ‖g i x‖ := (norm_sub_le _ _)
     _ ≤ m + m :=
       (add_le_add (real_norm_le (y + x) (by rwa [add_comm, add_mem_ball_iff_norm]) i)
@@ -335,7 +335,7 @@ Over ``ℝ`` or ``ℂ``, continuously differentiable
 functions are strictly differentiable.
 EXAMPLES: -/
 -- QUOTE:
-example {𝕂 : Type*} [IsROrC 𝕂] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type*}
+example {𝕂 : Type*} [RCLike 𝕂] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type*}
     [NormedAddCommGroup F] [NormedSpace 𝕂 F] {f : E → F} {x : E} {n : WithTop ℕ}
     (hf : ContDiffAt 𝕂 n f x) (hn : 1 ≤ n) : HasStrictFDerivAt f (fderiv 𝕂 f x) x :=
   hf.hasStrictFDerivAt hn

MIL/C11_Integration_and_Measure_Theory/S03_Integration.lean

@@ -50,7 +50,7 @@ So in all cases we have the following lemma.
 EXAMPLES: -/
 -- QUOTE:
 example {s : Set α} (c : E) : ∫ x in s, c ∂μ = (μ s).toReal • c :=
-  set_integral_const c
+  setIntegral_const c
 -- QUOTE.
 
 /- TEXT: