diff --git a/.gitignore b/.gitignore index cc75e48..d89e0dc 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ /build /lake-packages/* .lake/* +.claude diff --git a/ComputableReal/ComputableRSeq.lean b/ComputableReal/ComputableRSeq.lean index ab7a818..220b78a 100644 --- a/ComputableReal/ComputableRSeq.lean +++ b/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 diff --git a/ComputableReal/ComputableReal.lean b/ComputableReal/ComputableReal.lean index 286f6ab..2fa08ee 100644 --- a/ComputableReal/ComputableReal.lean +++ b/ComputableReal/ComputableReal.lean @@ -152,6 +152,12 @@ 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 @@ -159,7 +165,7 @@ instance instCommRing : CommRing Computableℝ := by | 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 diff --git a/ComputableReal/IsComputable.lean b/ComputableReal/IsComputable.lean index 48ee05f..3ea8fd5 100644 --- a/ComputableReal/IsComputable.lean +++ b/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 diff --git a/ComputableReal/SpecialFunctions/Exp.lean b/ComputableReal/SpecialFunctions/Exp.lean index 4a53a45..185603e 100644 --- a/ComputableReal/SpecialFunctions/Exp.lean +++ b/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 diff --git a/ComputableReal/SpecialFunctions/Pi.lean b/ComputableReal/SpecialFunctions/Pi.lean index 86d5996..160ef72 100644 --- a/ComputableReal/SpecialFunctions/Pi.lean +++ b/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 diff --git a/ComputableReal/SpecialFunctions/Sqrt.lean b/ComputableReal/SpecialFunctions/Sqrt.lean index 18cbf6e..0444a14 100644 --- a/ComputableReal/SpecialFunctions/Sqrt.lean +++ b/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 diff --git a/ComputableReal/aux_lemmas.lean b/ComputableReal/aux_lemmas.lean index 9ee77b0..9e473f0 100644 --- a/ComputableReal/aux_lemmas.lean +++ b/ComputableReal/aux_lemmas.lean @@ -2,7 +2,7 @@ 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 => @@ -10,7 +10,7 @@ theorem abs_ite_le [inst : LinearOrderedAddCommGroup α] (x : α) : 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 diff --git a/lake-manifest.json b/lake-manifest.json index 92699ce..ae1ecdc 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "2e4bea3590e14768d39b454d51bc438cf1731503", + "rev": "5e932f97dd25535344f80f9dd8da3aab83df0fe6", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "v4.29.1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "59a8514bb0ee5bae2689d8be717b5272c9b3dc1c", + "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5013810061a18ca1f5510106172b94c6fbd0a2fc", + "rev": "48d5698bc464786347c1b0d859b18f938420f060", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8fff3f074da9237cd4e179fd6dd89be6c4022d41", + "rev": "4dd0959c44d1af0462bd604d0f87c5781307d709", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.52-pre", + "inputRev": "v0.0.95+lean-v4.29.1", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ba9a63be53f16b3b6e4043641c6bad4883e650b4", + "rev": "7152850e7b216a0d409701617721b6e469d34bf6", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7b3b0c8327b3c0214ac49ca6d6922edbb81ab8c9", + "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "24cbb071689802fd6d3ff42198b19b125004c4e3", + "rev": "756e3321fd3b02a85ffda19fef789916223e578c", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "a2eb24a3dbf681f2b655f82ba5ee5b139d4a5abc", + "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.29.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "computableReal", diff --git a/lakefile.lean b/lakefile.lean index 0ff1d58..d1fbbcd 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ package «computableReal» { } require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" + "https://github.com/leanprover-community/mathlib4.git"@"v4.29.1" @[default_target] lean_lib «ComputableReal» { diff --git a/lean-toolchain b/lean-toolchain index 3ca992c..05a063a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.17.0-rc1 +leanprover/lean4:v4.29.1 \ No newline at end of file