Discussion: Upgrading to Lean v4.29.1 / current Mathlib

.gitignore

@@ -1,3 +1,4 @@
 /build
 /lake-packages/*
 .lake/*
+.claude

ComputableReal/ComputableRSeq.lean

@@ -1,6 +1,6 @@
 import Mathlib.Algebra.Order.Interval.Basic
 import Mathlib.Data.Real.Archimedean
-import Mathlib.Data.Sign
+import Mathlib.Data.Sign.Basic
 import Mathlib.Tactic.Rify
 
 import ComputableReal.aux_lemmas
@@ -44,9 +44,9 @@ theorem mul_pair_lb_is_lb {x y : ℚInterval} : ∀ xv ∈ x, ∀ yv ∈ y,
   intro xv ⟨hxl,hxu⟩ yv ⟨hyl,hyu⟩
   dsimp [mul_pair]
   push_cast
-  rcases le_or_lt xv 0 with hxn|hxp
-  all_goals rcases le_or_lt (y.fst:ℝ) 0 with hyln|hylp
-  all_goals rcases le_or_lt (y.snd:ℝ) 0 with hyun|hyup
+  rcases le_or_gt xv 0 with hxn|hxp
+  all_goals rcases le_or_gt (y.fst:ℝ) 0 with hyln|hylp
+  all_goals rcases le_or_gt (y.snd:ℝ) 0 with hyun|hyup
   all_goals try linarith
   all_goals repeat rw [min_def]
   all_goals split_ifs with h₁ h₂ h₃ h₃ h₂ h₃ h₃
@@ -57,9 +57,9 @@ theorem mul_pair_ub_is_ub {x y : ℚInterval} : ∀ xv ∈ x, ∀ yv ∈ y,
   intro xv ⟨hxl,hxu⟩ yv ⟨hyl,hyu⟩
   dsimp [mul_pair]
   push_cast
-  rcases le_or_lt xv 0 with hxn|hxp
-  all_goals rcases le_or_lt (y.1.1:ℝ) 0 with hyln|hylp
-  all_goals rcases le_or_lt (y.1.2:ℝ) 0 with hyun|hyup
+  rcases le_or_gt xv 0 with hxn|hxp
+  all_goals rcases le_or_gt (y.1.1:ℝ) 0 with hyln|hylp
+  all_goals rcases le_or_gt (y.1.2:ℝ) 0 with hyun|hyup
   all_goals try linarith
   all_goals repeat rw [max_def]
   all_goals split_ifs with h₁ h₂ h₃ h₃ h₂ h₃ h₃
@@ -575,7 +575,7 @@ noncomputable def sign_witness_term (x : ComputableℝSeq) (hnz : x.val ≠ 0) :
 theorem sign_witness_term_prop (x : ComputableℝSeq) (n : ℕ) (hnz : x.val ≠ 0)
     (hub : ¬(x.ub).val n < 0) (hlb: ¬(x.lb).val n > 0) :
     n + Nat.succ 0 ≤ (x.sign_witness_term hnz).val.1 := by
-  push_neg at hub hlb
+  push Not at hub hlb
   obtain ⟨⟨k, q⟩, ⟨h₁, h₂, h₃⟩⟩ := x.sign_witness_term hnz
   by_contra hn
   replace h₃ := h₃ n (by linarith)
@@ -802,7 +802,7 @@ theorem lb_inv_converges {x : ComputableℝSeq} (hnz : x.val ≠ 0) :
   rw [Real.cauchy_inv, Real.cauchy, Real.cauchy, Real.mk, val_eq_mk_ub, Real.mk,
     CauSeq.Completion.inv_mk (neg_LimZero_ub_of_val hnz), CauSeq.Completion.mk_eq, lb_inv]
   split_ifs with h
-  · rfl
+  · rw [sub_self]; exact CauSeq.zero_limZero
   · exact fun _ hε ↦
       have hxv : x.val < 0 := by
         rw [is_pos_iff] at h
@@ -832,7 +832,7 @@ theorem ub_inv_converges {x : ComputableℝSeq} (hnz : x.val ≠ 0) :
       ⟨i, fun j hj ↦
         have : ¬x.lb j ≤ 0 := by linarith [H _ hj]
         by simp [this, hε]⟩
-  · rfl
+  · rw [sub_self]; exact CauSeq.zero_limZero
 
 /-- When applied to a `dropTilSigned`, `ub_inv` is converges to x⁻¹.
 TODO: version without hnz hypothesis. -/
@@ -844,12 +844,13 @@ theorem ub_inv_signed_converges {x : ComputableℝSeq} (hnz : x.val ≠ 0) :
  nonzero, then we can prove that at some point we learn the sign, and so can start giving actual
  upper and lower bounds. There is a separate `inv` that uses `sign` to construct the proof of
  nonzeroness by searching along the sequence (but isn't guaranteed to terminate). -/
-def safe_inv (x : ComputableℝSeq) (hnz : x.val ≠ 0) : ComputableℝSeq :=
+noncomputable def safe_inv (x : ComputableℝSeq) (hnz : x.val ≠ 0) : ComputableℝSeq :=
   --TODO currently this passes the sequence to lb_inv and ub_inv separately, which means we evaluate
   --things twice (and this can lead to exponential slowdown for long series of inverses). This should
   --be bundled
   let signed := x.dropTilSigned hnz
   let hnz' := val_dropTilSigned hnz ▸ hnz
+  -- x.val⁻¹ use `Real.instInv` here, which is noncomputable.
   mk (x := x.val⁻¹)
   (lub := fun n ↦ ⟨⟨(signed.lb_inv hnz') n, (signed.ub_inv hnz') n⟩,
     Rat.cast_le.mp ((lb_inv_correct hnz n).trans (ub_inv_correct hnz n))⟩)
@@ -870,14 +871,14 @@ theorem val_safe_inv_ne_zero {x : ComputableℝSeq} (hnz : x.val ≠ 0) : (x.saf
 /-- Subtype of sequences with nonzero values. These admit a (terminating) inverse function. -/
 def nzSeq := {x : ComputableℝSeq // x.val ≠ 0}
 
-def inv_nz : nzSeq → nzSeq :=
+noncomputable def inv_nz : nzSeq → nzSeq :=
   fun x ↦ ⟨x.val.safe_inv x.prop, val_safe_inv_ne_zero _⟩
 
 @[simp]
 theorem val_inv_nz (x : nzSeq) : (inv_nz x).val.val = x.val.val⁻¹ :=
   val_safe_inv _
 
-instance instNzInv : Inv nzSeq :=
+noncomputable instance instNzInv : Inv nzSeq :=
   ⟨inv_nz⟩
 
 end safe_inv
@@ -887,16 +888,16 @@ section inv
 /-- Inverse of a computable real. Will terminate if the argument is nonzero, or if it is zero and the
   upper and lower bounds become exactly zero at some point. See `ComputableℝSeq.sign`. If you want
   to only call this in a way guaranteed to terminate, use `ComputableℝSeq.safe_inv`. -/
-def inv : ComputableℝSeq → ComputableℝSeq :=
+noncomputable def inv : ComputableℝSeq → ComputableℝSeq :=
   fun x ↦ match h : x.sign with
   | SignType.pos => x.safe_inv (x.sign_pos_iff.1 h).ne'
   | SignType.neg => x.safe_inv (x.sign_neg_iff.1 h).ne
   | SignType.zero => 0
 
-instance instInv : Inv ComputableℝSeq :=
+noncomputable instance instInv : Inv ComputableℝSeq :=
   ⟨inv⟩
 
-instance instDiv : Div ComputableℝSeq :=
+noncomputable instance instDiv : Div ComputableℝSeq :=
   ⟨fun x y ↦ x * y⁻¹⟩
 
 theorem inv_def (x : ComputableℝSeq) : x⁻¹ = x.inv :=
@@ -941,7 +942,7 @@ theorem add_comm (x y: ComputableℝSeq) : x + y = y + x := by
 
 theorem mul_comm (x y : ComputableℝSeq) : x * y = y * x := by
   ext n
-  <;> simp only [lb_mul, ub_mul, mul_lb, mul_ub]
+  <;> simp only [lb_mul, ub_mul]
   · repeat rw [_root_.mul_comm (lb x)]
     repeat rw [_root_.mul_comm (ub x)]
     dsimp
@@ -983,13 +984,13 @@ theorem right_distrib (x y z : ComputableℝSeq) : (x + y) * z = x * z + y * z :
 theorem neg_mul (x y : ComputableℝSeq) : -x * y = -(x * y) := by
   ext
   · rw [lb_neg, lb_mul, ub_mul]
-    simp only [lb_neg, ub_neg, CauSeq.coe_inf, CauSeq.coe_mul, CauSeq.coe_neg, neg_mul,
+    simp only [lb_neg, ub_neg, CauSeq.coe_inf, CauSeq.coe_mul, CauSeq.coe_neg,
       Pi.inf_apply, Pi.neg_apply, Pi.mul_apply, CauSeq.neg_apply, CauSeq.coe_sup, Pi.sup_apply, neg_sup]
     nth_rewrite 2 [inf_comm]
     nth_rewrite 3 [inf_comm]
     ring_nf
   · rw [ub_neg, lb_mul, ub_mul]
-    simp only [lb_neg, ub_neg, CauSeq.coe_inf, CauSeq.coe_mul, CauSeq.coe_neg, neg_mul,
+    simp only [lb_neg, ub_neg, CauSeq.coe_inf, CauSeq.coe_mul, CauSeq.coe_neg,
       Pi.inf_apply, Pi.neg_apply, Pi.mul_apply, CauSeq.neg_apply, CauSeq.coe_sup, Pi.sup_apply, neg_inf]
     nth_rewrite 2 [sup_comm]
     nth_rewrite 3 [sup_comm]
@@ -1028,7 +1029,7 @@ class CompSeqClass (G : Type u) extends
   AddCommMonoid G, CommMagma G, MulZeroOneClass G, Inv G, Div G,
   HasDistribNeg G, SubtractionCommMonoid G, NatCast G, IntCast G, RatCast G
 
-instance instSeqCompSeqClass : CompSeqClass ComputableℝSeq := by
+noncomputable instance instSeqCompSeqClass : CompSeqClass ComputableℝSeq := by
   refine' {
             natCast := fun n => n
             intCast := fun z => z
@@ -1062,8 +1063,8 @@ instance instSeqCompSeqClass : CompSeqClass ComputableℝSeq := by
     | rfl
     | ext
       all_goals
-        try simp only [natCast_ub, natCast_lb, Nat.cast_add, Nat.cast_one, CauSeq.add_apply, CauSeq.one_apply,
-           CauSeq.zero_apply, CauSeq.neg_apply, lb_add, ub_add, one_ub, one_lb, zero_ub, zero_lb, ub_neg,
+        try simp only [CauSeq.add_apply,
+           CauSeq.zero_apply, CauSeq.neg_apply, lb_add, ub_add, zero_ub, zero_lb, ub_neg,
            lb_neg, neg_add_rev, neg_neg, zero_add, add_zero]
         try ring_nf
         try rfl

ComputableReal/ComputableReal.lean

@@ -152,14 +152,20 @@ instance instCommRing : CommRing Computableℝ := by
             npow := npowRec --todo faster instances
             nsmul := nsmulRec
             zsmul := zsmulRec
+            natCast_succ := fun n => by
+              rw [← eq_iff_eq_val]
+              simp only [val_mk_eq_val, val_add, val_one, ComputableℝSeq.val_natCast]
+              push_cast; ring
+            sub_eq_add_neg := fun a b => by
+              rw [← eq_iff_eq_val, val_sub, val_add, val_neg]; ring
             .. }
   all_goals
     intros
     first
     | rfl
     | rw [← eq_iff_eq_val]
       simp
-      try ring_nf!
+      try ring
 
 @[simp]
 theorem val_natpow (x : Computableℝ) (n : ℕ): (x ^ n).val = x.val ^ n := by
@@ -191,14 +197,14 @@ private def nz_quot_equiv := Equiv.subtypeQuotientEquivQuotientSubtype
     (fun _ _ ↦ Iff.rfl)
 
 /-- Auxiliary inverse definition that operates on the nonzero Computableℝ values. -/
-def safe_inv' : { x : Computableℝ // x ≠ 0 } → { x : Computableℝ // x ≠ 0 } :=
+noncomputable def safe_inv' : { x : Computableℝ // x ≠ 0 } → { x : Computableℝ // x ≠ 0 } :=
   fun v ↦ nz_quot_equiv.invFun <| Quotient.map _ fun x y h₁ ↦ by
     change (ComputableℝSeq.inv_nz x).val.val = (ComputableℝSeq.inv_nz y).val.val
     rw [ComputableℝSeq.val_inv_nz x, ComputableℝSeq.val_inv_nz y, h₁]
   (nz_quot_equiv.toFun v)
 
 /-- Inverse of a nonzero Computableℝ, safe (terminating) as long as x is nonzero. -/
-irreducible_def safe_inv (hnz : x ≠ 0) : Computableℝ := safe_inv' ⟨x, hnz⟩
+noncomputable irreducible_def safe_inv (hnz : x ≠ 0) : Computableℝ := safe_inv' ⟨x, hnz⟩
 
 @[simp]
 theorem safe_inv_val (hnz : x ≠ 0) : (x.safe_inv hnz).val = x.val⁻¹ := by
@@ -219,7 +225,7 @@ end safe_inv
 
 section field
 
-instance instComputableInv : Inv Computableℝ :=
+noncomputable instance instComputableInv : Inv Computableℝ :=
   ⟨mapℝ' (·⁻¹) ⟨(·⁻¹), ComputableℝSeq.val_inv⟩⟩
 
 @[simp]
@@ -230,7 +236,7 @@ theorem inv_val : (x⁻¹).val = (x.val)⁻¹ := by
 
 example : True := ⟨⟩
 
-instance instField : Field Computableℝ := { instCommRing with
+noncomputable instance instField : Field Computableℝ := { instCommRing with
   qsmul := _
   nnqsmul := _
   exists_pair_ne := ⟨0, 1, by
@@ -302,26 +308,39 @@ instance instDecidableLE : DecidableRel (fun (x y : Computableℝ) ↦ x ≤ y)
     infer_instance
 
 --TODO: add a faster `min` and `max` that don't require sign computation.
-instance instLinearOrderedField : LinearOrderedField Computableℝ := by
-  refine' { instField, instLT, instLE with
-      decidableLE := inferInstance
-      le_refl := _
-      le_trans := _
-      le_antisymm := _
-      add_le_add_left := _
-      zero_le_one := _
-      mul_pos := _
-      le_total := _
-      lt_iff_le_not_le := _
-    }
-  all_goals
-    intros
-    simp only [← le_iff_le, ← lt_iff_lt, ← eq_iff_eq_val, val_add, val_mul, val_zero, val_one] at *
-    first
-    | linarith (config := {splitNe := true})
-    | apply mul_pos ‹_› ‹_›
-    | apply le_total
-    | apply lt_iff_le_not_le
+instance instLinearOrder : LinearOrder Computableℝ where
+  le_refl x := by rw [← le_iff_le]
+  le_trans a b c h₁ h₂ := by rw [← le_iff_le] at *; exact le_trans h₁ h₂
+  lt_iff_le_not_ge a b := by
+    simp only [← lt_iff_lt, ← le_iff_le]
+    exact lt_iff_le_not_ge
+  le_antisymm a b h₁ h₂ := by
+    rw [← le_iff_le] at h₁ h₂; rw [← eq_iff_eq_val]; exact le_antisymm h₁ h₂
+  le_total a b := by simp only [← le_iff_le]; exact le_total _ _
+  toDecidableLE := instDecidableLE
+
+instance instIsOrderedAddMonoid : IsOrderedAddMonoid Computableℝ where
+  add_le_add_left a b h c := by
+    simp only [← le_iff_le, val_add] at *; linarith
+
+instance instIsOrderedCancelAddMonoid : IsOrderedCancelAddMonoid Computableℝ where
+  le_of_add_le_add_left a b c h := by
+    simp only [← le_iff_le, val_add] at *; linarith
+
+noncomputable instance instPosMulStrictMono : PosMulStrictMono Computableℝ where
+  mul_lt_mul_of_pos_left := by
+    intro a ha b c hbc
+    simp only [← lt_iff_lt, val_mul, val_zero] at *
+    exact mul_lt_mul_of_pos_left hbc ha
+
+noncomputable instance instMulPosStrictMono : MulPosStrictMono Computableℝ where
+  mul_lt_mul_of_pos_right := by
+    intro c hc a b hab
+    simp only [← lt_iff_lt, val_mul, val_zero] at *
+    exact mul_lt_mul_of_pos_right hab hc
+
+instance instIsStrictOrderedRing : IsStrictOrderedRing Computableℝ where
+  zero_le_one := by rw [← le_iff_le, val_zero, val_one]; exact zero_le_one
 
 end ordered
 

ComputableReal/IsComputable.lean

@@ -13,15 +13,18 @@ namespace IsComputable
 
 /-- Turns one `IsComputable` into another one, given a proof that they're equal. This is directly
 analogous to `decidable_of_iff`, as a way to avoid `Eq.rec` on data-carrying instances. -/
+@[reducible]
 def lift_eq {x y : ℝ} (h : x = y) :
     IsComputable x → IsComputable y :=
   fun ⟨sx, hsx⟩ ↦ ⟨sx, h ▸ hsx⟩
 
+@[reducible]
 def lift (fr : ℝ → ℝ) (fs : ComputableℝSeq → ComputableℝSeq)
     (h : ∀ a, (fs a).val = fr a.val) :
     IsComputable x → IsComputable (fr x) :=
   fun ⟨sx, hsx⟩ ↦ ⟨fs sx, hsx ▸ h sx⟩
 
+@[reducible]
 def lift₂ (fr : ℝ → ℝ → ℝ) (fs : ComputableℝSeq → ComputableℝSeq → ComputableℝSeq)
     (h : ∀a b, (fs a b).val = fr a.val b.val) :
     IsComputable x → IsComputable y → IsComputable (fr x y) :=
@@ -55,7 +58,7 @@ instance instComputableOfNatAtLeastTwo : (n : ℕ) → [n.AtLeastTwo] → IsComp
 instance instComputableNeg (x : ℝ) [hx : IsComputable x] : IsComputable (-x) :=
   lift _ (- ·) ComputableℝSeq.val_neg hx
 
-instance instComputableInv (x : ℝ) [hx : IsComputable x] : IsComputable (x⁻¹) :=
+noncomputable instance instComputableInv (x : ℝ) [hx : IsComputable x] : IsComputable (x⁻¹) :=
   lift _ (·⁻¹) ComputableℝSeq.val_inv hx
 
 instance instComputableAdd [hx : IsComputable x] [hy : IsComputable y] : IsComputable (x + y) :=
@@ -67,7 +70,7 @@ instance instComputableSub [hx : IsComputable x] [hy : IsComputable y] : IsCompu
 instance instComputableMul [hx : IsComputable x] [hy : IsComputable y] : IsComputable (x * y) :=
   lift₂ _ (· * ·) ComputableℝSeq.val_mul hx hy
 
-instance instComputableDiv [hx : IsComputable x] [hy : IsComputable y] : IsComputable (x / y) :=
+noncomputable instance instComputableDiv [hx : IsComputable x] [hy : IsComputable y] : IsComputable (x / y) :=
   lift₂ _ (· / ·) ComputableℝSeq.val_div hx hy
 
 instance instComputableNatPow [hx : IsComputable x] (n : ℕ) : IsComputable (x ^ n) := by
@@ -82,14 +85,14 @@ instance instComputableNatPow [hx : IsComputable x] (n : ℕ) : IsComputable (x
   · rw [pow_succ]
     infer_instance
 
-instance instComputableZPow [hx : IsComputable x] (z : ℤ) : IsComputable (x ^ z) := by
+noncomputable instance instComputableZPow [hx : IsComputable x] (z : ℤ) : IsComputable (x ^ z) := by
   cases z
-  · rw [Int.ofNat_eq_coe, zpow_natCast]
+  · rw [Int.ofNat_eq_natCast, zpow_natCast]
     infer_instance
   · simp only [zpow_negSucc]
     infer_instance
 
-instance instComputableNSMul [hx : IsComputable x] (n : ℕ) : IsComputable (n • x) :=
+noncomputable instance instComputableNSMul [hx : IsComputable x] (n : ℕ) : IsComputable (n • x) :=
   lift _ (n • ·) (by
     --TODO move to a ComputableℝSeq lemma
     intro a
@@ -194,7 +197,7 @@ theorem Real_mk_of_TendstoLocallyUniformly' (fImpl : ℕ → ℚ → ℚ) (f : 
 
   calc |↑(fImpl j (x j)) - f (Real.mk ⟨x, hx⟩)| =
     |(↑(fImpl j (x j)) - f ↑(x j)) + (f ↑(x j) - f (Real.mk ⟨x, hx⟩))| := by congr; ring_nf
-    _ ≤ |(↑(fImpl j (x j)) - f ↑(x j))| + |(f ↑(x j) - f (Real.mk ⟨x, hx⟩))| := abs_add _ _
+    _ ≤ |(↑(fImpl j (x j)) - f ↑(x j))| + |(f ↑(x j) - f (Real.mk ⟨x, hx⟩))| := abs_add_le _ _
     _ < ε := by rw [abs_sub_comm]; linarith
 
 open scoped QInterval

ComputableReal/SpecialFunctions/Exp.lean

@@ -1,5 +1,5 @@
 import ComputableReal.IsComputable
-import Mathlib.Data.Complex.Exponential
+import Mathlib.Analysis.Complex.Exponential
 import Mathlib.Analysis.SpecialFunctions.Exp
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 

ComputableReal/SpecialFunctions/Pi.lean

@@ -1,5 +1,5 @@
 import ComputableReal.SpecialFunctions.Sqrt
-import Mathlib.Data.Real.Pi.Bounds
+import Mathlib.Analysis.Real.Pi.Bounds
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
 
 open scoped QInterval

ComputableReal/SpecialFunctions/Sqrt.lean

@@ -1,7 +1,7 @@
 import ComputableReal.IsComputable
 import Mathlib.Data.Real.Sqrt
 import Mathlib.Analysis.SpecialFunctions.Log.Base
-import Mathlib.Data.Real.GoldenRatio
+import Mathlib.NumberTheory.Real.GoldenRatio
 
 namespace ComputableℝSeq
 

ComputableReal/aux_lemmas.lean

@@ -2,15 +2,15 @@ import Mathlib.Data.Real.Archimedean
 
 --============
 --silly lemmas
-theorem abs_ite_le [inst : LinearOrderedAddCommGroup α] (x : α) :
+theorem abs_ite_le [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (x : α) :
     abs x = if 0 ≤ x then x else -x := by
   split_ifs <;> simp_all
   next h =>
     exact LT.lt.le h
 
 namespace CauSeq
 
-variable [LinearOrderedField α] {a b : CauSeq α abs}
+variable [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b : CauSeq α abs}
 
 theorem sup_equiv_of_equivs (ha : a ≈ c) (hb : b ≈ c) : a ⊔ b ≈ c := by
   intro n hn