From 86f3d84d5ccb20fa40213f1b6045a5a4d0f36c87 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 19 Aug 2026 17:37:55 +0200 Subject: [PATCH 1/4] chore: bump to current mathlib Just a few deprecation warnings, very uneventful. --- SphereEversion/Global/Localisation.lean | 10 ++++----- SphereEversion/Global/SmoothEmbedding.lean | 8 +++---- SphereEversion/Local/OneJet.lean | 8 +++---- SphereEversion/Loops/Exists.lean | 8 +++---- .../ToMathlib/Analysis/Convex/Basic.lean | 2 +- .../Geometry/Manifold/VectorBundle/Misc.lean | 4 ++-- .../ToMathlib/SmoothBarycentric.lean | 12 +++++----- SphereEversion/ToMathlib/Topology/Misc.lean | 6 ++--- SphereEversion/ToMathlib/Topology/Path.lean | 8 +++---- lake-manifest.json | 22 +++++++++---------- lakefile.toml | 1 - lean-toolchain | 2 +- 12 files changed, 45 insertions(+), 46 deletions(-) diff --git a/SphereEversion/Global/Localisation.lean b/SphereEversion/Global/Localisation.lean index 687887f8..90b43126 100644 --- a/SphereEversion/Global/Localisation.lean +++ b/SphereEversion/Global/Localisation.lean @@ -196,11 +196,11 @@ theorem ChartPair.mkHtpy_congr (F : FormalSol R) {𝓕 : (R.localize p.φ p.ψ). {t t' : ℝ} (h : 𝓕 t = 𝓕 t') : p.mkHtpy F 𝓕 t = p.mkHtpy F 𝓕 t' := by unfold ChartPair.mkHtpy by_cases hF : p.compat' F 𝓕 - · simp only [dif_pos hF] + · simp only [dite_eq_left hF] apply FormalSol.coe_inj fun x ↦ ?_ rw [p.φ.updateFormalSol_apply, p.φ.updateFormalSol_apply, RelLoc.HtpyFormalSol.unloc_congr' p h] - · simp only [dif_neg hF]; rfl + · simp only [dite_eq_right hF]; rfl theorem ChartPair.mkHtpy_eq_self (F : FormalSol R) (𝓕 : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol) {t m} (hm : ∀ hF : range (F.bs ∘ p.φ) ⊆ range p.ψ, ∀ x ∈ p.K₁, @@ -250,7 +250,7 @@ theorem ChartPair.mkHtpy_eq_of_forall {F : FormalSol R} theorem ChartPair.mkHtpy_localize {F : FormalSol R} {𝓕 : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol} {t e} (h : p.compat' F 𝓕) (rg : range ((p.mkHtpy F 𝓕 t).bs ∘ p.φ) ⊆ range p.ψ) : (p.mkHtpy F 𝓕 t).toOneJetSec.localize p.φ p.ψ rg e = (𝓕 t).unloc e := by - simp_rw [ChartPair.mkHtpy, dif_pos h] at rg ⊢ + simp_rw [ChartPair.mkHtpy, dite_eq_left h] at rg ⊢ exact p.φ.Jupdate_localize p.ψ p.hK₁ (p.mkHtpy_aux h) t rg e theorem ChartPair.mkHtpy_isHolonomicAt_iff {F : FormalSol R} @@ -259,7 +259,7 @@ theorem ChartPair.mkHtpy_isHolonomicAt_iff {F : FormalSol R} have rg : range ((p.mkHtpy F 𝓕 t).bs ∘ p.φ) ⊆ range p.ψ := by rintro - ⟨e, rfl⟩ dsimp only [ChartPair.mkHtpy] - simp only [dif_pos h] + simp only [dite_eq_left h] rw [p.φ.updateFormalSol_bs p.ψ p.hK₁] simp only [Function.comp_apply, OpenSmoothEmbedding.update_apply_embedding, mem_range_self] rw [← isHolonomicAt_localize_iff _ p.φ p.ψ rg e, ← JetSec.unloc_hol_at_iff] @@ -278,7 +278,7 @@ theorem ChartPair.dist_update' [FiniteDimensional ℝ E'] {δ : M → ℝ} (hδ_ intro 𝓕 h𝓕 t e change (p.mkHtpy F 𝓕 t (p.φ e)).1.2 = p.φ.update p.ψ bsF (fun e ↦ (𝓕.unloc p t).bs e) (p.φ e) dsimp only [ChartPair.mkHtpy] - rw [dif_pos h𝓕, OpenSmoothEmbedding.updateFormalSol_apply] + rw [dite_eq_left h𝓕, OpenSmoothEmbedding.updateFormalSol_apply] simp_rw [OpenSmoothEmbedding.update_apply_embedding, OneJetBundle.embedding_toFun, OpenSmoothEmbedding.transfer_proj_snd] rfl diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean index 8062257f..9be52199 100644 --- a/SphereEversion/Global/SmoothEmbedding.lean +++ b/SphereEversion/Global/SmoothEmbedding.lean @@ -397,11 +397,11 @@ def update (m : M) : N := end @[simp] -theorem update_of_nmem_range {m : M} (hm : m ∉ range φ) : update φ ψ f g m = f m := if_neg hm +theorem update_of_nmem_range {m : M} (hm : m ∉ range φ) : update φ ψ f g m = f m := ite_eq_right hm @[simp] theorem update_of_mem_range {m : M} (hm : m ∈ range φ) : update φ ψ f g m = ψ (g (φ.invFun m)) := - if_pos hm + ite_eq_left hm theorem update_apply_embedding (x : X) : update φ ψ f g (φ x) = ψ (g x) := by simp @@ -413,7 +413,7 @@ theorem nice_update_of_eq_outside_compact_aux {K : Set X} (g : X → Y) · obtain ⟨x, rfl⟩ := hm' replace hm : x ∉ K := by contrapose! hm; exact mem_image_of_mem φ hm simp [hg x hm] - · exact if_neg hm' + · exact ite_eq_right hm' open Function @@ -433,7 +433,7 @@ theorem contMDiff_update (f : M' → M → N) (g : M' → X → Y) {k : M' → M rw [← compl_subset_iff_union, compl_compl] exact image_subset_range φ K have h₄ (x) : k x ∈ U → update φ ψ (f x) (g x) (k x) = (ψ ∘ g x ∘ φ.invFun) (k x) := - fun hm ↦ if_pos hm + fun hm ↦ ite_eq_left hm by_cases hx : k x ∈ U · exact ⟨k ⁻¹' U, φ.isOpen_range.preimage hk.continuous, hx, (contMDiffOn_congr h₄).mpr <| ψ.contMDiff_to.comp_contMDiffOn <| hg.comp_contMDiffOn diff --git a/SphereEversion/Local/OneJet.lean b/SphereEversion/Local/OneJet.lean index 7724e567..5857f207 100644 --- a/SphereEversion/Local/OneJet.lean +++ b/SphereEversion/Local/OneJet.lean @@ -251,7 +251,7 @@ theorem htpy_jet_sec_comp_aux {f g : ℝ → E → F} (hf : 𝒞 ∞ ↿f) (hg : obtain ⟨t, x⟩ := p replace hp : t < 1 / 2 := (prodMk_mem_set_prod_eq.mp hp).1 change ite (t ≤ 1 / 2) (f (smoothStep (2 * t)) x) (g (smoothStep (2 * t - 1)) x) = _ - rw [if_pos hp.le] + rw [ite_eq_left hp.le] rfl · apply (hf (1 / 2, x₀)).congr_of_eventuallyEq have : (Ioo (3 / 8) (5 / 8) : Set ℝ) ×ˢ univ ∈ 𝓝 (1 / (2 : ℝ), x₀) := by @@ -273,7 +273,7 @@ theorem htpy_jet_sec_comp_aux {f g : ℝ → E → F} (hf : 𝒞 ∞ ↿f) (hg : obtain ⟨t, x⟩ := p replace hp : ¬t ≤ 1 / 2 := by push Not; exact (prodMk_mem_set_prod_eq.mp hp).1 change ite (t ≤ 1 / 2) (f (smoothStep (2 * t)) x) (g (smoothStep (2 * t - 1)) x) = _ - rw [if_neg hp] + rw [ite_eq_right hp] rfl /-- Concatenation of homotopies of formal solution. The result depend on our choice of @@ -287,7 +287,7 @@ def HtpyJetSec.comp (𝓕 𝓖 : HtpyJetSec E F) (h : 𝓕 1 = 𝓖 0) : HtpyJet @[simp] theorem HtpyJetSec.comp_of_le (𝓕 𝓖 : HtpyJetSec E F) (h) {t : ℝ} (ht : t ≤ 1 / 2) : 𝓕.comp 𝓖 h t = 𝓕 (smoothStep <| 2 * t) := by - ext x : 2 <;> · dsimp [HtpyJetSec.comp]; exact if_pos ht + ext x : 2 <;> · dsimp [HtpyJetSec.comp]; exact ite_eq_left ht theorem HtpyJetSec.comp_le_0 (𝓕 𝓖 : HtpyJetSec E F) (h) : ∀ᶠ t near Iic 0, 𝓕.comp 𝓖 h t = 𝓕 0 := by @@ -310,7 +310,7 @@ theorem HtpyJetSec.comp_0 (𝓕 𝓖 : HtpyJetSec E F) (h) : 𝓕.comp 𝓖 h 0 theorem HtpyJetSec.comp_of_not_le (𝓕 𝓖 : HtpyJetSec E F) (h) {t : ℝ} (ht : ¬t ≤ 1 / 2) : 𝓕.comp 𝓖 h t = 𝓖 (smoothStep <| 2 * t - 1) := by rw [one_div] at ht - ext x : 2 <;> simp [comp, if_neg ht] <;> rfl + ext x : 2 <;> simp [comp, ite_eq_right ht] <;> rfl theorem HtpyJetSec.comp_ge_1 (𝓕 𝓖 : HtpyJetSec E F) (h) : ∀ᶠ t near Ici 1, 𝓕.comp 𝓖 h t = 𝓖 1 := by have : Ioi (7 / 8 : ℝ) ∈ 𝓝ˢ (Ici (1 : ℝ)) := diff --git a/SphereEversion/Loops/Exists.lean b/SphereEversion/Loops/Exists.lean index 06199ee6..6a6e2ebf 100644 --- a/SphereEversion/Loops/Exists.lean +++ b/SphereEversion/Loops/Exists.lean @@ -127,9 +127,9 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : have h2f : ∀ x : E, Continuous (f x) := fun x ↦ h1f.comp₂ continuous_const continuous_id have h3f : ∀ {x y}, 0 < f x y := by intro x y; by_cases hΩ : Ωᶜ.Nonempty - · simp_rw [f, if_pos hΩ, ← hΩ_op.isClosed_compl.notMem_iff_infDist_pos hΩ, notMem_compl_iff, - hγ₃.val_in (mem_univ _)] - · simp_rw [f, if_neg hΩ, zero_lt_one] + · simp_rw [f, ite_eq_left hΩ, ← hΩ_op.isClosed_compl.notMem_iff_infDist_pos hΩ, + notMem_compl_iff, hγ₃.val_in (mem_univ _)] + · simp_rw [f, ite_eq_right hΩ, zero_lt_one] let ε₂ : E → ℝ := fun x ↦ min (min ε₀ (ε₁ x)) (sInf (f x '' I ×ˢ I)) have hcε₂ : Continuous ε₂ := (continuous_const.min hcε₁).min (hI.continuous_sInf h1f) have hε₂ : ∀ {x}, 0 < ε₂ x := fun {x} ↦ @@ -227,7 +227,7 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : refine (hγ₅₄ (x, _, fract s)).trans_le ((min_le_right _ _).trans <| csInf_le ?_ ?_) · exact (isCompact_Icc.prod isCompact_Icc).bddBelow_image (h2f x).continuousOn · rw [← hγ₃.projI] - simp_rw [f, if_pos hΩ] + simp_rw [f, ite_eq_left hΩ] apply mem_image_of_mem _ (mk_mem_prod projI_mem_Icc (unitInterval.fract_mem s)) · refine eventually_of_mem (Filter.inter_mem hV hγ₂₁) fun x hx t s ↦ ?_ refine (closedBall_subset_ball ?_).trans (hΩ x hx.1) diff --git a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean index 96f375c4..54221a86 100644 --- a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean +++ b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean @@ -28,7 +28,7 @@ theorem finite_of_finprod_ne_one {M : Type*} {ι : Sort _} [CommMonoid M] {f : classical rw [finprod_def] at h contrapose h - rw [dif_neg (by exact h)] + rw [dite_eq_right (by exact h)] theorem support_finite_of_finsum_eq_of_neZero {M : Type*} {ι : Sort _} [AddCommMonoid M] {f : ι → M} {x : M} [NeZero x] (h : ∑ᶠ i, f i = x) : (support f).Finite := by diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean index a719d8af..e95f8727 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean @@ -81,7 +81,7 @@ theorem trivialization_continuousLinearMapAt (x : B) : (Trivial.trivialization B F).continuousLinearMapAt 𝕜 x = ContinuousLinearMap.id 𝕜 F := by ext v simp_rw [Trivialization.continuousLinearMapAt_apply, Trivialization.coe_linearMapAt] - rw [if_pos] + rw [ite_eq_left] exacts [rfl, mem_univ _] end Bundle.Trivial @@ -138,7 +138,7 @@ theorem pullback_symm (e : Trivialization F (π F E)) (x : B') : simp_rw [Trivialization.symm, Pretrivialization.symm] congr; ext (hx : f x ∈ e.toPretrivialization.baseSet) change cast _ (e.symm (f x) y) = cast _ (e.toOpenPartialHomeomorph.symm (f x, y)).2 - simp_rw [Trivialization.symm, Pretrivialization.symm, dif_pos hx, cast_cast] + simp_rw [Trivialization.symm, Pretrivialization.symm, dite_eq_left hx, cast_cast] rfl end Trivialization diff --git a/SphereEversion/ToMathlib/SmoothBarycentric.lean b/SphereEversion/ToMathlib/SmoothBarycentric.lean index e753822f..f09e06fb 100644 --- a/SphereEversion/ToMathlib/SmoothBarycentric.lean +++ b/SphereEversion/ToMathlib/SmoothBarycentric.lean @@ -41,12 +41,12 @@ def evalBarycentricCoords [DecidablePred (· ∈ affineBases ι R P)] (p : P) (v theorem evalBarycentricCoords_apply_of_mem_bases [DecidablePred (· ∈ affineBases ι R P)] (p : P) {v : ι → P} (h : v ∈ affineBases ι R P) : evalBarycentricCoords ι R P p v = (AffineBasis.mk v h.1 h.2).coords p := - dif_pos h + dite_eq_left h @[simp] theorem evalBarycentricCoords_apply_of_not_mem_bases [DecidablePred (· ∈ affineBases ι R P)] (p : P) {v : ι → P} (h : v ∉ affineBases ι R P) : evalBarycentricCoords ι R P p v = 0 := - dif_neg h + dite_eq_right h variable {ι R P} @@ -56,7 +56,7 @@ theorem evalBarycentricCoords_eq_det [Fintype ι] [DecidableEq ι] (S : Type*) [ (b.toMatrix v).det⁻¹ • (b.toMatrix v)ᵀ.cramer (b.coords p) := by ext i by_cases h : v ∈ affineBases ι S P - · simp only [evalBarycentricCoords, h, dif_pos, smul_eq_mul, Pi.smul_apply, + · simp only [evalBarycentricCoords, h, dite_eq_left, smul_eq_mul, Pi.smul_apply, AffineBasis.coords_apply] erw [← b.det_smul_coords_eq_cramer_coords ⟨v, h.1, h.2⟩ p] simp only [Pi.smul_apply, AffineBasis.coords_apply, smul_eq_mul] @@ -64,7 +64,7 @@ theorem evalBarycentricCoords_eq_det [Fintype ι] [DecidableEq ι] (S : Type*) [ rw [Matrix.isUnit_iff_isUnit_det] at hu erw [← mul_assoc, ← Ring.inverse_eq_inv, Ring.inverse_mul_cancel _ hu, one_mul] · simp only [evalBarycentricCoords, h, smul_eq_mul, Pi.zero_apply, inv_eq_zero, - dif_neg, not_false_iff, zero_eq_mul, Pi.smul_apply] + dite_eq_right, not_false_iff, zero_eq_mul, Pi.smul_apply] left rwa [mem_affineBases_iff ι S P b v, Matrix.isUnit_iff_isUnit_det, isUnit_iff_ne_zero, Classical.not_not] at h @@ -144,9 +144,9 @@ theorem smooth_barycentric [DecidablePred (· ∈ affineBases ι 𝕜 F)] [Finit simp only [Matrix.updateRow_apply] simp only [AffineBasis.toMatrix_apply, AffineBasis.coords_apply] by_cases hij : j = i - · simp only [hij, if_true] + · simp only [hij, ite_true] exact (smooth_barycentric_coord b j').fst'.of_le le_top - · simp only [hij, if_false] + · simp only [hij, ite_false] exact ((smooth_barycentric_coord b j').of_le le_top).comp (contDiff_pi.mp contDiff_snd j) end smooth_barycentric diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean index 004223f2..54cf8cb7 100644 --- a/SphereEversion/ToMathlib/Topology/Misc.lean +++ b/SphereEversion/ToMathlib/Topology/Misc.lean @@ -185,7 +185,7 @@ open scoped Classical in theorem isOpen_slice_of_isOpen_over {Ω : Set (α × β)} {x₀ : α} (hΩ_op : ∃ U ∈ 𝓝 x₀, IsOpen (Ω ∩ Prod.fst ⁻¹' U)) : IsOpen (Prod.mk x₀ ⁻¹' Ω) := by rcases hΩ_op with ⟨U, hU, hU_op⟩; convert hU_op.preimage (Continuous.prodMk_right x₀) using 1 - simp_rw [preimage_inter, preimage_preimage, preimage_const, mem_of_mem_nhds hU, if_pos, + simp_rw [preimage_inter, preimage_preimage, preimage_const, mem_of_mem_nhds hU, ite_eq_left, inter_univ] end @@ -411,9 +411,9 @@ theorem cover_nat_nhdsWithin' {α} [TopologicalSpace α] [SecondCountableTopolog {f : ∀ x ∈ s, Set α} (hf : ∀ (x) (hx : x ∈ s), f x hx ∈ 𝓝[s] x) (hs : s.Nonempty) : ∃ (x : ℕ → α) (hx : range x ⊆ s), s ⊆ ⋃ n, f (x n) (range_subset_iff.mp hx n) := by let g x := if hx : x ∈ s then f x hx else ∅ - have hg : ∀ x ∈ s, g x ∈ 𝓝[s] x := fun x hx ↦ by simp_rw [g, dif_pos hx]; exact hf x hx + have hg : ∀ x ∈ s, g x ∈ 𝓝[s] x := fun x hx ↦ by simp_rw [g, dite_eq_left hx]; exact hf x hx obtain ⟨x, hx, h⟩ := TopologicalSpace.cover_nat_nhdsWithin hg hs - simp_rw [g, dif_pos (range_subset_iff.mp hx _)] at h + simp_rw [g, dite_eq_left (range_subset_iff.mp hx _)] at h exact ⟨x, hx, h⟩ end TopologicalSpace diff --git a/SphereEversion/ToMathlib/Topology/Path.lean b/SphereEversion/ToMathlib/Topology/Path.lean index f09fd795..604675e5 100644 --- a/SphereEversion/ToMathlib/Topology/Path.lean +++ b/SphereEversion/ToMathlib/Topology/Path.lean @@ -62,11 +62,11 @@ theorem strans_zero (γ γ' : Path x x) : γ.strans γ' 0 = γ' := by @[simp] theorem strans_one {x : X} (γ γ' : Path x x) : γ.strans γ' 1 = γ := by ext t - simp only [strans, unitInterval.le_one', Path.coe_mk_mk, if_pos, div_one, extend_extends', + simp only [strans, unitInterval.le_one', Path.coe_mk_mk, ite_eq_left, div_one, extend_extends', Icc.coe_one] theorem strans_self {x : X} (γ γ' : Path x x) (t₀ : I) : γ.strans γ' t₀ t₀ = x := by - simp only [strans, Path.coe_mk_mk, extend_div_self, if_pos, le_rfl] + simp only [strans, Path.coe_mk_mk, extend_div_self, ite_eq_left, le_rfl] @[simp] theorem refl_strans_refl {x : X} {t₀ : I} : (refl x).strans (refl x) t₀ = refl x := by @@ -95,8 +95,8 @@ theorem range_strans_subset {x : X} {γ γ' : Path x x} {t₀ : I} : range (γ.strans γ' t₀) ⊆ range γ ∪ range γ' := by rintro _ ⟨t, rfl⟩ by_cases h : t ≤ t₀ - · rw [strans_def, dif_pos h]; exact Or.inl (mem_range_self _) - · rw [strans_def, dif_neg h]; exact Or.inr (mem_range_self _) + · rw [strans_def, dite_eq_left h]; exact Or.inl (mem_range_self _) + · rw [strans_def, dite_eq_right h]; exact Or.inr (mem_range_self _) theorem Continuous.path_strans {X Y : Type*} [UniformSpace X] [LocallyCompactSpace X] [UniformSpace Y] {f : X → Y} {t : X → I} {s : X → I} diff --git a/lake-manifest.json b/lake-manifest.json index cf559274..8bee5af2 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,17 +15,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "db584cd6d46c92f209a44c0f1c829460d327499d", + "rev": "1fe0a51a5ecdee23c424b6e29ecb1d40eb35316d", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0", + "inputRev": "master", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", + "rev": "38e9c3ce15cbb63c92e90bb9a92e4eb82131f669", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", + "rev": "2bc7cf064315b26bc38dac2e9612fb581be9b75f", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "16f02aa7642864af59f1ff0e384a015994db9118", + "rev": "978b7ec9fbbf9a535114f1de8fe5b3778b358870", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", + "rev": "ebeca04ecd5ee2ba9740e13576d80d4ab6b5779c", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", + "rev": "c1c4362a130f12e632d252180a6c2a31d8fd4726", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", + "rev": "3b55e9d00c6b0018e5d984eb011b6f93c09bd163", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", + "rev": "36cc05ca2d0e469bfbeea9437f460e19238e885e", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,10 +95,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "rev": "af8bc067a4cc6c6df472a68909a3f40b1c76c43e", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0", + "inputRev": "v4.34.0-rc1", "inherited": true, "configFile": "lakefile.toml"}], "name": "SphereEversion", diff --git a/lakefile.toml b/lakefile.toml index 5aafe34f..f2a95077 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -11,7 +11,6 @@ weak.linter.style.header = false [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.33.0" [[require]] name = "checkdecls" diff --git a/lean-toolchain b/lean-toolchain index 6a884ba1..e2a0e356 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0 \ No newline at end of file +leanprover/lean4:v4.34.0-rc1 \ No newline at end of file From 7b86df0b8b5a6de7dc1d85d7bd995db2f7cc1caf Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 19 Aug 2026 17:56:57 +0200 Subject: [PATCH 2/4] chore(Unused): fix a few warnings --- .../ToMathlib/Unused/EventuallyConstant.lean | 35 +++++++++++-------- 1 file changed, 21 insertions(+), 14 deletions(-) diff --git a/SphereEversion/ToMathlib/Unused/EventuallyConstant.lean b/SphereEversion/ToMathlib/Unused/EventuallyConstant.lean index 08710c5f..cd5c7a64 100644 --- a/SphereEversion/ToMathlib/Unused/EventuallyConstant.lean +++ b/SphereEversion/ToMathlib/Unused/EventuallyConstant.lean @@ -6,7 +6,7 @@ Authors: Floris van Doorn ! This file was ported from Lean 3 source module to_mathlib.unused.eventually_constant -/ import Mathlib.Data.Nat.Lattice -import Mathlib.Topology.Separation.Basic +import Mathlib.Topology.Separation.Hausdorff /-! # Eventually constant sequences @@ -33,11 +33,11 @@ def unionElim [DecidablePred (· ∈ s)] (f : s → β) (g : t → β) (x : s theorem unionElim_eq_left [DecidablePred (· ∈ s)] (hx : x ∈ s) : unionElim f g ⟨x, mem_union_left _ hx⟩ = f ⟨x, hx⟩ := - dif_pos hx + dite_eq_left hx theorem unionElim_eq_right [DecidablePred (· ∈ s)] (h1x : x ∈ s ∪ t) (h2x : x ∉ s) : unionElim f g ⟨x, h1x⟩ = g ⟨x, h1x.resolve_left h2x⟩ := - dif_neg h2x + dite_eq_right h2x theorem unionElim_eq_right_of_eq [DecidablePred (· ∈ s)] (hxt : x ∈ t) (hfg : ∀ (x) (hxs : x ∈ s) (hxt : x ∈ t), f ⟨x, hxs⟩ = g ⟨x, hxt⟩) : @@ -45,7 +45,7 @@ theorem unionElim_eq_right_of_eq [DecidablePred (· ∈ s)] (hxt : x ∈ t) if hxs : x ∈ s then (unionElim_eq_left hxs).trans (hfg x hxs hxt) else unionElim_eq_right _ hxs _ theorem unionElim_restrict [DecidablePred (· ∈ s)] (f : α → β) : - unionElim (s.restrict f) (t.restrict f) = (s ∪ t).restrict f := by + unionElim (s.domRestrict f) (t.domRestrict f) = (s ∪ t).domRestrict f := by ext ⟨x, hx⟩ --cases (mem_union _ _ _).mp hx <;> simp [union_elim_eq_left, union_elim_eq_right_of_eq, h] @@ -63,16 +63,18 @@ variable {α β γ : Type*} {g : α → β} {f : Filter α} {x : α} {y : β} def EventuallyConstant (g : α → β) (f : Filter α) : Prop := ∃ y : β, ∀ᶠ x in f, g x = y -theorem eventuallyConstant_iff_tendsto : EventuallyConstant g f ↔ ∃ x : β, Tendsto g f (pure x) := by simp_rw [EventuallyConstant, tendsto_pure] +theorem eventuallyConstant_iff_tendsto : + EventuallyConstant g f ↔ ∃ x : β, Tendsto g f (pure x) := by + simp_rw [EventuallyConstant, tendsto_pure] theorem EventuallyConstant.nonempty (h : EventuallyConstant g f) : Nonempty β := nonempty_of_exists h theorem eventuallyConstant_const (y₀ : β) : EventuallyConstant (fun _ ↦ y₀) f := - ⟨y₀, eventually_of_forall fun _ ↦ rfl⟩ + ⟨y₀, Eventually.of_forall fun _ ↦ rfl⟩ theorem eventuallyConstant_of_unique [Unique β] : EventuallyConstant g f := - ⟨default, eventually_of_forall fun _ ↦ Unique.uniq _ _⟩ + ⟨default, Eventually.of_forall fun _ ↦ Unique.uniq _ _⟩ theorem eventuallyConstant_atTop [SemilatticeSup α] [Nonempty α] : (∃ i, ∀ j, i ≤ j → g j = g i) ↔ EventuallyConstant g atTop := by @@ -86,12 +88,17 @@ theorem eventuallyConstant_atTop_nat {g : ℕ → α} : rw [← eventuallyConstant_atTop] apply exists_congr; intro n constructor - · intro h m hm; induction' hm with m hm ih; rfl; rw [Nat.succ_eq_add_one, h m hm, ih] + · intro h m hm + induction hm with + | refl => rfl + | step hm ih => + rename_i m0 + rw [Nat.succ_eq_add_one, h m0 hm, ih] · intro h m hm; rw [h m hm, h (m + 1) hm.step] theorem EventuallyConstant.compose (h : EventuallyConstant g f) (g' : β → γ) : EventuallyConstant (g' ∘ g) f := by - cases' h with y hy; + obtain ⟨y, hy⟩ := h exact ⟨g' y, hy.mono fun x ↦ congr_arg g'⟩ theorem EventuallyConstant.apply {ι : Type*} {p : ι → Type*} {g : α → ∀ x, p x} @@ -137,7 +144,7 @@ theorem EventuallyConstant.tendsto [Nonempty β] (h : EventuallyConstant g f) : theorem eventualValue_compose [f.NeBot] (h : EventuallyConstant g f) (g' : β → γ) : @eventualValue _ _ (h.compose g').nonempty (g' ∘ g) f = g' (@eventualValue _ _ h.nonempty g f) := - (eventualValue_unique <| (eventually_eq_eventualValue h).mono fun x ↦ congr_arg g').symm + (eventualValue_unique <| (eventually_eq_eventualValue h).mono fun _x ↦ congr_arg g').symm theorem eventualValue_apply {ι : Type*} {p : ι → Type*} [f.NeBot] {g : α → ∀ x, p x} (h : EventuallyConstant g f) (i : ι) : @@ -184,11 +191,11 @@ section EventuallyConstantOn `g` restricted to `O` is eventually constant. -/ def EventuallyConstantOn (g : α → β → γ) (f : Filter α) (O : Set β) : Prop := - EventuallyConstant (fun n ↦ O.restrict (g n)) f + EventuallyConstant (fun n ↦ O.domRestrict (g n)) f theorem EventuallyConstantOn.eventuallyConstant (hg : EventuallyConstantOn g f O) (hx : x ∈ O) : EventuallyConstant (fun n ↦ g n x) f := by - cases' hg with y hg; + obtain ⟨y, hg⟩ := hg exact ⟨y ⟨x, hx⟩, hg.mono fun n hn ↦ (Function.funext_iff.mp hn ⟨x, hx⟩ : _)⟩ theorem EventuallyConstantOn.nonempty (hg : EventuallyConstantOn g f O) (hx : x ∈ O) : Nonempty γ := @@ -196,11 +203,11 @@ theorem EventuallyConstantOn.nonempty (hg : EventuallyConstantOn g f O) (hx : x theorem eventuallyConstantOn_atTop [SemilatticeSup α] [Nonempty α] : (∃ x, ∀ x', x ≤ x' → ∀ y ∈ O, g x' y = g x y) ↔ EventuallyConstantOn g atTop O := by - simp_rw [EventuallyConstantOn, ← eventuallyConstant_atTop, restrict_eq_restrict_iff, eq_on] + simp_rw [EventuallyConstantOn, ← eventuallyConstant_atTop, domRestrict_eq_domRestrict_iff, EqOn] theorem EventuallyConstantOn.exists_eventualValue_eq [f.NeBot] (hg : EventuallyConstantOn g f O) : ∃ i, ∀ (x) (hx : x ∈ O), @eventualValue _ _ (hg.nonempty hx) (fun n ↦ g n x) f = g i x := by - simpa only [@eq_restrict_iff β fun _ ↦ γ, eventualValue_apply hg] using + simpa only [@eq_domRestrict_iff β fun _ ↦ γ, eventualValue_apply hg] using hg.exists_eventualValue_eq -- lemma EventuallyConstantOn.exists_eventualValue_eq [f.NeBot] (h : EventuallyConstant g f) : From 887ecfcc1ce90c669afcb2e884da4ba0c9b8c199 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 19 Aug 2026 18:09:02 +0200 Subject: [PATCH 3/4] chore: minor fun_prop golfs --- SphereEversion/Loops/Exists.lean | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/SphereEversion/Loops/Exists.lean b/SphereEversion/Loops/Exists.lean index 6a6e2ebf..7a66dde3 100644 --- a/SphereEversion/Loops/Exists.lean +++ b/SphereEversion/Loops/Exists.lean @@ -124,23 +124,21 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : let f : E → ℝ × ℝ → ℝ := fun x y ↦ if Ωᶜ.Nonempty then infDist (x, γ₃ x y.1 y.2) (Ωᶜ) else 1 have hI : IsCompact (I ×ˢ I) := isCompact_Icc.prod isCompact_Icc have h1f : Continuous ↿f := (continuous_fst.prodMk hγ₃.cont).infDist.if_const _ continuous_const - have h2f : ∀ x : E, Continuous (f x) := fun x ↦ h1f.comp₂ continuous_const continuous_id - have h3f : ∀ {x y}, 0 < f x y := by - intro x y; by_cases hΩ : Ωᶜ.Nonempty + have h3f {x y} : 0 < f x y := by + by_cases hΩ : Ωᶜ.Nonempty · simp_rw [f, ite_eq_left hΩ, ← hΩ_op.isClosed_compl.notMem_iff_infDist_pos hΩ, notMem_compl_iff, hγ₃.val_in (mem_univ _)] · simp_rw [f, ite_eq_right hΩ, zero_lt_one] let ε₂ : E → ℝ := fun x ↦ min (min ε₀ (ε₁ x)) (sInf (f x '' I ×ˢ I)) - have hcε₂ : Continuous ε₂ := (continuous_const.min hcε₁).min (hI.continuous_sInf h1f) + have hcε₂ : Continuous ε₂ := by + have := hI.continuous_sInf h1f; unfold ε₂; fun_prop have hε₂ : ∀ {x}, 0 < ε₂ x := fun {x} ↦ lt_min (lt_min hε₀ (hε₁ x)) ((hI.lt_sInf_iff_of_continuous - ((nonempty_Icc.mpr zero_le_one).prod (nonempty_Icc.mpr zero_le_one)) - (h2f x).continuousOn _).mpr + ((nonempty_Icc.mpr zero_le_one).prod (nonempty_Icc.mpr zero_le_one)) (by fun_prop) _).mpr fun x _ ↦ h3f) let γ₄ := ↿γ₃ have h0γ₄ : ∀ x t s, γ₄ (x, t, s) = γ₃ x t s := fun x t s ↦ rfl - have hγ₄ : Continuous γ₄ := hγ₃.cont let C₁ : Set ℝ := Iic (5⁻¹ : ℝ) ∪ Ici (4 / 5) have h0C₁ : (0 : ℝ) ∈ C₁ := Or.inl (by rw [mem_Iic]; norm_num1) have h2C₁ : ∀ (s : ℝ) (hs : fract s = 0), fract ⁻¹' C₁ ∈ 𝓝 s := by @@ -181,7 +179,7 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : exact Or.imp le_of_lt le_of_lt hs have h3γ₄ : ContDiffOn ℝ ∞ γ₄ U := hb.fst'.contDiffOn.congr h2γ₄ obtain ⟨γ₅, hγ₅, hγ₅₄, hγ₅C⟩ := - exists_smooth_and_eqOn hγ₄ hcε₂.fst' (fun x ↦ hε₂) hC ⟨U, hUC, h3γ₄⟩ + exists_smooth_and_eqOn hγ₃.cont hcε₂.fst' (fun x ↦ hε₂) hC ⟨U, hUC, h3γ₄⟩ let γ : E → ℝ → Loop F := fun x t ↦ ⟨fun s ↦ γ₅ (x, smoothTransition t, fract s), fun s ↦ by rw [fract_add_one s]⟩ have hγ : 𝒞 ∞ ↿γ := by @@ -225,7 +223,7 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : · exact (x, γ₃ x (smoothTransition t) (fract s)) · rw [dist_comm, dist_prod_same_left] refine (hγ₅₄ (x, _, fract s)).trans_le ((min_le_right _ _).trans <| csInf_le ?_ ?_) - · exact (isCompact_Icc.prod isCompact_Icc).bddBelow_image (h2f x).continuousOn + · exact (isCompact_Icc.prod isCompact_Icc).bddBelow_image (by fun_prop) · rw [← hγ₃.projI] simp_rw [f, ite_eq_left hΩ] apply mem_image_of_mem _ (mk_mem_prod projI_mem_Icc (unitInterval.fract_mem s)) @@ -233,7 +231,7 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : refine (closedBall_subset_ball ?_).trans (hΩ x hx.1) refine (dist_triangle ..).trans_lt (add_lt_add_of_le_of_lt ((hγ₅₄ (x, _, fract s)).le.trans <| (min_le_left _ _).trans <| min_le_left ..) ?_) - simp_rw [γ₄, γ₃, HasUncurry.uncurry, Loop.reparam_apply, show γ₂ x = γ₁ x from hx.2] + simp_rw [γ₃, HasUncurry.uncurry, Loop.reparam_apply, show γ₂ x = γ₁ x from hx.2] exact h2γ₁ x hx.1 .. variable (g b Ω U K) From 0ff5bcd14d06c6eee7eb26767ec7f4fa4482d84a Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 7 Sep 2026 12:38:30 +0200 Subject: [PATCH 4/4] chore: bump to current mathlib Most changes are routine or minor. One mfderiv proof needed a fix, but the new proof is nicer anyway. --- SphereEversion/Global/OneJetSec.lean | 3 ++- SphereEversion/Global/Relation.lean | 5 ++++- SphereEversion/InductiveConstructions.lean | 6 +++--- SphereEversion/Local/HPrinciple.lean | 6 +++--- SphereEversion/Loops/Surrounding.lean | 6 +++--- .../ToMathlib/Topology/Paracompact.lean | 2 +- lake-manifest.json | 20 +++++++++---------- lean-toolchain | 2 +- 8 files changed, 27 insertions(+), 23 deletions(-) diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean index 8a948d01..be812fa7 100644 --- a/SphereEversion/Global/OneJetSec.lean +++ b/SphereEversion/Global/OneJetSec.lean @@ -148,7 +148,8 @@ def IsHolonomicGerm {x : M} (φ : Germ (𝓝 x) (OneJetBundle I M I' M')) : Prop intro f g hfg hf have hfg' : (fun x' ↦ (f x').1.2) =ᶠ[𝓝 x] fun x' ↦ (g x').1.2 := hfg.fun_comp fun s ↦ s.1.2 - rw [← hfg'.mfderiv_eq, hf, hfg.self_of_nhds] + rw [hfg'.symm.mfderiv_eq, hf, hfg.self_of_nhds] + rfl exact fun f g H ↦ propext ⟨key f g H, key g f H.symm⟩) /-- The one-jet extension of a function, seen as a section of the 1-jet bundle. -/ diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean index eff4d325..fc6da8ce 100644 --- a/SphereEversion/Global/Relation.lean +++ b/SphereEversion/Global/Relation.lean @@ -474,7 +474,10 @@ theorem OpenSmoothEmbedding.smooth_transfer : ContMDiffAt.mfderiv (fun _ ↦ φ.invFun) (fun x : OneJetBundle IX X IY Y ↦ φ x.1.1) ((φ.contMDiffAt_inv <| _).comp (x, φ x.1.1) contMDiffAt_snd) (φ.contMDiff_to.contMDiffAt.comp x (contMDiff_oneJetBundle_proj.fst x)) (mod_cast le_top) - · simp only [left_inv] at this; exact this + · convert this + · simp + · simp + rfl exact mem_range_self _ theorem OneJetBundle.continuous_transfer : Continuous (φ.transfer ψ) := diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean index 1df3a5e0..bacf5d40 100644 --- a/SphereEversion/InductiveConstructions.lean +++ b/SphereEversion/InductiveConstructions.lean @@ -346,7 +346,7 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ · have hp : ∀ᶠ p : ℝ × X in 𝓝 (t, x), p.1 ≤ T i.toNat := continuousAt_fst (p := (t, x)) (Iic_mem_nhds ht) apply Quotient.sound - exact hp.mono fun p hp ↦ if_pos hp + exact hp.mono fun p hp ↦ ite_eq_left hp have loc₂ : ∀ p : ℝ × X, p.1 > T i.toNat → (F'' : Germ (𝓝 p) Y) = fun p : ℝ × X ↦ F' ((2 : ℝ) ^ (i.toNat + 1) * (p.1 - T i.toNat)) p.2 := fun (t, x) ht ↦ by @@ -355,7 +355,7 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ apply mem_of_superset (prod_mem_nhds (Ioi_mem_nhds ht) univ_mem) rintro ⟨t', x'⟩ ⟨ht', -⟩ simpa using ht' - exact hp.mono fun q hq ↦ if_neg hq + exact hp.mono fun q hq ↦ ite_eq_right hq refine ⟨F'', ?_, ?_, ?_, ?_⟩ · intro p by_cases! ht : p.1 ≤ T i.toNat @@ -373,7 +373,7 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ rw [i.toNat_succ hi] at ht ⊢ have h₂t : ¬t ≤ T i.toNat := ((T_lt_succ i.toNat).trans_le ht).not_ge dsimp only [F''] - rw [if_neg h₂t, if_neg] + rw [ite_eq_right h₂t, ite_eq_right] · rw [hfutur_F'.self_of_nhdsSet, mul_T_succ_sub] conv => rw [mem_Ici] diff --git a/SphereEversion/Local/HPrinciple.lean b/SphereEversion/Local/HPrinciple.lean index 8ab338a4..ed9d5c72 100644 --- a/SphereEversion/Local/HPrinciple.lean +++ b/SphereEversion/Local/HPrinciple.lean @@ -315,9 +315,9 @@ theorem bu_lt {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] (t : ℝ) ( calc ‖(smoothStep t * L.ρ x) • v‖ = |smoothStep t| * |L.ρ x| * ‖v‖ := by rw [norm_smul, Real.norm_eq_abs, abs_mul] - _ ≤ ‖v‖ := - (mul_le_of_le_one_left (norm_nonneg _) - (mul_le_one₀ (smoothStep.abs_le t) (abs_nonneg _) (L.ρ_le x))) + _ ≤ ‖v‖ := by + apply mul_le_of_le_one_left (norm_nonneg _) + exact Bound.mul_le_one (smoothStep.abs_le t) (L.ρ_le x) (by grind) _ < ε := hv theorem improveStep_c0_close {ε : ℝ} (ε_pos : 0 < ε) : diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean index 44fc05a0..dff8128f 100644 --- a/SphereEversion/Loops/Surrounding.lean +++ b/SphereEversion/Loops/Surrounding.lean @@ -153,7 +153,7 @@ theorem surrounded_iff_mem_interior_convexHull_aff_basis [FiniteDimensional ℝ basis.coord_apply_combination_of_mem (Finset.mem_univ i) w_sum] exact w_pos i · rintro ⟨b, h₀, h₁, h₂, h₃⟩ - have : Fintype b := (finite_set_of_fin_dim_affineIndependent ℝ h₁).fintype + have : Fintype b := ((finiteDimensional_iff_setFinite ℝ h₁).mp (by infer_instance)).fintype have hb : Fintype.card b = d + 1 := by rw [← h₁.affineSpan_eq_top_iff_card_eq_finrank_add_one, Subtype.range_coe_subtype, ofPred_mem_eq, h₂] @@ -184,7 +184,7 @@ theorem surrounded_of_convexHull [FiniteDimensional ℝ F] {f : F} {s : Set F} ( exact hsf have htne : (t : Set F).Nonempty := convexHull_nonempty_iff.mp ⟨f, hf⟩ obtain ⟨b, hb₁, hb₂, hb₃, hb₄⟩ := hs.exists_between_affineIndependent_span_eq_top hts htne hai - have hb₀ : b.Finite := finite_set_of_fin_dim_affineIndependent ℝ hb₃ + have hb₀ : b.Finite := ((finiteDimensional_iff_setFinite ℝ hb₃).mp (by infer_instance)) obtain ⟨c, hc⟩ := interior_convexHull_nonempty_iff_affineSpan_eq_top.mpr hb₄ rw [← hs.interior_eq] at hb₂ obtain ⟨ε, hε, hcs⟩ := @@ -193,7 +193,7 @@ theorem surrounded_of_convexHull [FiniteDimensional ℝ F] {f : F} {s : Set F} ( rw [AffineMap.image_convexHull] at hbε let t : Units ℝ := Units.mk0 ε (by linarith) refine ⟨AffineMap.homothety c (t : ℝ) '' b, hcs, ?_, ?_, hbε (convexHull_mono hb₁ hf)⟩ - · rw [(AffineEquiv.homothetyUnitsMulHom c t).affineIndependent_set_of_eq_iff]; assumption + · rwa [(AffineEquiv.homothetyUnitsMulHom c t).affineIndependent_set_of_eq_iff] · exact (AffineEquiv.homothetyUnitsMulHom c t).span_eq_top_iff.mp hb₄ /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ diff --git a/SphereEversion/ToMathlib/Topology/Paracompact.lean b/SphereEversion/ToMathlib/Topology/Paracompact.lean index f9d5f945..9a8281b7 100644 --- a/SphereEversion/ToMathlib/Topology/Paracompact.lean +++ b/SphereEversion/ToMathlib/Topology/Paracompact.lean @@ -1,5 +1,5 @@ import Mathlib.Topology.Separation.Hausdorff -import Mathlib.Data.Real.Basic +import Mathlib.Basic.Real.Basic import Mathlib.Order.Interval.Finset.Nat open scoped Topology diff --git a/lake-manifest.json b/lake-manifest.json index 8bee5af2..49feddd3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1fe0a51a5ecdee23c424b6e29ecb1d40eb35316d", + "rev": "5bc1283b23926af94593ce7c66fccdbbe49f4d12", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "38e9c3ce15cbb63c92e90bb9a92e4eb82131f669", + "rev": "d9598f07b1bc701f1e3aae163d2681c1fd978793", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2bc7cf064315b26bc38dac2e9612fb581be9b75f", + "rev": "ba67e212be1197b84c1f1f6299488a10a3002713", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "978b7ec9fbbf9a535114f1de8fe5b3778b358870", + "rev": "1681d78dd6e65e38b143f9740d829c826673807c", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ebeca04ecd5ee2ba9740e13576d80d4ab6b5779c", + "rev": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c1c4362a130f12e632d252180a6c2a31d8fd4726", + "rev": "18889deb9e83ea7420ef51c160d6f88552e744e3", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3b55e9d00c6b0018e5d984eb011b6f93c09bd163", + "rev": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "36cc05ca2d0e469bfbeea9437f460e19238e885e", + "rev": "4cac2177c37f5530c4da76aa8e4307f3fc9e4dcb", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,10 +95,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "af8bc067a4cc6c6df472a68909a3f40b1c76c43e", + "rev": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.34.0-rc1", + "inputRev": "v4.34.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "SphereEversion", diff --git a/lean-toolchain b/lean-toolchain index e2a0e356..d5ae4e31 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.34.0-rc1 \ No newline at end of file +leanprover/lean4:v4.34.0-rc2 \ No newline at end of file