wip: bump to current mathlib --- still a handful of broken proofs

SphereEversion/Global/LocalisationData.lean

@@ -50,8 +50,7 @@ omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 theorem iUnion_succ' {β : Type*} (s : ld.ι → Set β) (i : IndexType ld.N) :
     (⋃ j ≤ i, s j) = (⋃ j < i, s j) ∪ s i := by
   simp only [(fun _ ↦ le_iff_lt_or_eq : ∀ j, j ≤ i ↔ j < i ∨ j = i)]
-  erw [biUnion_union, biUnion_singleton]
-  rfl
+  simp_rw [iUnion_or, iUnion_union_distrib, iUnion_iUnion_eq_left]
 
 open Filter
 

SphereEversion/Global/SmoothEmbedding.lean

@@ -415,7 +415,7 @@ theorem nice_update_of_eq_outside_compact_aux {K : Set X} (g : X → Y)
     φ.update ψ f g m = f m := by
   by_cases hm' : m ∈ range φ
   · obtain ⟨x, rfl⟩ := hm'
-    replace hm : x ∉ K := by contrapose! hm; exact mem_image_of_mem φ hm
+    replace hm : x ∉ K := by contrapose hm; exact mem_image_of_mem φ hm
     simp [hg x hm]
   · exact ite_eq_right hm'
 

SphereEversion/Local/SphereEversion.lean

@@ -194,7 +194,7 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank 
       rw [← toDual_symm_apply]
       change ¬⟪u, pr[x]ᗮ u⟫ = 0
       rw [inner_projection_self_eq_zero_iff.not]
-      contrapose! H
+      contrapose H
       rw [orthogonal_orthogonal] at H
       rw [← orthogonal_span_toDual_symm, spanOrthogonal, spanLine,
           span_singleton_eq_span_singleton_of_ne u_ne H]

SphereEversion/Loops/Basic.lean

@@ -382,22 +382,42 @@ theorem ContDiff.partial_loop {γ : E → Loop F} {n : ℕ∞} (hγ_diff : 𝒞
 
 variable [FiniteDimensional ℝ F]
 
+
+
+#click_suggestions
 set_option backward.isDefEq.respectTransparency.types false in
 theorem Loop.support_diff {γ : E → Loop F} : Loop.support (Loop.diff γ) ⊆ Loop.support γ := by
   unfold Loop.support
-  erw [closure_compl, closure_compl]
-  rw [compl_subset_compl]
-  intro x hx
-  rw [mem_interior_iff_mem_nhds] at *
-  rcases mem_nhds_iff.mp hx with ⟨U, hU, U_op, hxU⟩
-  apply Filter.mem_of_superset (U_op.mem_nhds hxU) fun y hy ↦ ?_
-  have Hy : ∀ t, (fun z ↦ γ z t) =ᶠ[𝓝 y] fun z ↦ (γ z).average :=
-    fun t ↦ Filter.mem_of_superset (U_op.mem_nhds hy)
-      (fun z hz ↦ Loop.isConst_iff_forall_avg.mp (hU hz) t)
-  have : ∀ t : ℝ, Loop.diff γ y t = D (fun z : E ↦ (γ z).average) y := fun t ↦ (Hy t).fderiv_eq
-  intro t s
-  simp only [this]
-
+  gcongr
+  intro hx
+  sorry
+  -- have Hy : ∀ t, (fun z ↦ γ z t) =ᶠ[𝓝 y] fun z ↦ (γ z).average :=
+  --   fun t ↦ Filter.mem_of_superset (U_op.mem_nhds hy)
+  --     (fun z hz ↦ Loop.isConst_iff_forall_avg.mp (hU hz) t)
+  -- have (y) : ∀ t : ℝ, Loop.diff γ y t = D (fun z : E ↦ (γ z).average) y := fun t ↦ (Hy t).fderiv_eq
+  -- intro y s
+  -- trans 0
+  -- sorry
+  -- sorry
+  -- --suffices ∀()
+  -- --intro s t
+  -- unfold IsConst at hx ⊢
+  --change closure {x | (diff γ x).IsConst}ᶜ ⊆ closure {x | (γ x).IsConst}ᶜ
+  --rw [Set.compl_def]
+  --rw [closure_compl]
+
+  --, closure_compl]
+  --rw [compl_subset_compl]
+  --intro x hx
+  --rw [mem_interior_iff_mem_nhds] at *
+  -- rcases mem_nhds_iff.mp hx with ⟨U, hU, U_op, hxU⟩
+  -- --apply Filter.mem_of_superset (U_op.mem_nhds hxU) fun y hy ↦ ?_
+  -- have Hy : ∀ t, (fun z ↦ γ z t) =ᶠ[𝓝 y] fun z ↦ (γ z).average :=
+  --   fun t ↦ Filter.mem_of_superset (U_op.mem_nhds hy)
+  --     (fun z hz ↦ Loop.isConst_iff_forall_avg.mp (hU hz) t)
+  -- have : ∀ t : ℝ, Loop.diff γ y t = D (fun z : E ↦ (γ z).average) y := fun t ↦ (Hy t).fderiv_eq
+  -- intro t s
+  -- simp only [this]
 
 variable [FiniteDimensional ℝ E]
 

SphereEversion/Loops/Exists.lean

@@ -169,11 +169,12 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op :
     in Lean 3.
     -/
     apply hU.mem_nhdsSet.mpr
+    sorry /- proof was
     refine (union_subset_union fun (x : E × ℝ × ℝ)
       (hx : x.2.1 ≤ 5⁻¹) ↦ lt_of_le_of_lt hx (by norm_num)) ?_
     refine union_subset_union (fun (x : E × ℝ × ℝ)
       (hx : fract x.2.2 ≤ 5⁻¹) ↦ lt_of_le_of_lt hx (by norm_num)) ?_
-    exact fun x hx ↦ lt_of_lt_of_le (by norm_num : (3 / 4 : ℝ) < 4 / 5) hx
+    exact fun x hx ↦ lt_of_lt_of_le (by norm_num : (3 / 4 : ℝ) < 4 / 5) hx -/
   have h2γ₄ : EqOn γ₄ (fun x ↦ b x.1) U := by
     rintro ⟨x, t, s⟩ hxts
     simp_rw [h0γ₄, γ₃, Loop.reparam_apply]

SphereEversion/Loops/Reparametrization.lean

@@ -275,7 +275,7 @@ theorem contDiffOn_localCenteringDensity :
         fun x ↦ (x, x)
     change ContDiffOn ℝ ∞ ((w ∘ z) ∘ Prod.fst) (γ.localCenteringDensityNhd x ×ˢ (univ : Set ℝ))
     rw [prod_univ]
-    refine ContDiffOn.comp ?_ contDiff_fst.contDiffOn Subset.rfl
+    sorry /-refine ContDiffOn.comp ?_ contDiff_fst.contDiffOn ?_--(by simp)--Subset.rfl
     have h₁ := contDiff_barycentric ι ℝ F (Fintype.card_fin _) (n := ∞)
     have h₂ : 𝒞 ∞ (eval i : (ι → ℝ) → ℝ) := contDiff_apply _ _ i
     refine (h₂.comp_contDiffOn h₁).comp ?_ ?_
@@ -284,7 +284,7 @@ theorem contDiffOn_localCenteringDensity :
       refine γ.smooth_surrounded.contDiffOn.prodMap (ContDiff.contDiffOn ?_)
       exact γ.approxSurroundingPointsAt_smooth x _
     · intro y hy
-      simp [z, γ.approxSurroundingPointsAt_mem_affineBases x y hy]
+      simp [z, γ.approxSurroundingPointsAt_mem_affineBases x y hy] -/
   · exact contDiff_deltaMollifier.comp contDiff_snd
 
 variable [FiniteDimensional ℝ E] in

SphereEversion/ToMathlib/Analysis/Convex/Basic.lean

@@ -158,7 +158,7 @@ theorem ReallyConvex.preimageₛₗ (f : E →ₛₗ[σ.toRingHom] E') {s : Set
     apply hs.finsum_mem
     · intro i; rw [← map_zero σ]; apply σ.monotone'; apply hw
     · rw [← map_finsum _ h4w, h3w, map_one]
-    · intro i hi; apply h2w; rw [mem_support] at hi ⊢; contrapose! hi; rw [hi, map_zero]
+    · intro i hi; apply h2w; rw [mem_support] at hi ⊢; contrapose hi; rw [hi, map_zero]
 
 theorem ReallyConvex.preimage [IsOrderedRing 𝕜]
     (f : E →ₗ[𝕜] E₂) {s : Set E₂} (hs : ReallyConvex 𝕜 s) :

SphereEversion/ToMathlib/ExistsOfConvex.lean

@@ -76,8 +76,8 @@ theorem exists_contMDiff_of_convex {P : M → F → Prop} (hP : ∀ x, Convex 
     ∃ f : M → F, CMDiff n f ∧ ∀ x, P x (f x) := by
   let PP : (Σ x : M, Germ (𝓝 x) F) → Prop := fun p ↦ p.2.ContMDiffAt I n ∧ P p.1 p.2.value
   have hPP : ∀ x : M, ReallyConvex (smoothGerm I x) {φ | PP ⟨x, φ⟩} := fun x ↦ by
-    apply ReallyConvex.inter
-    · apply reallyConvex_contMDiffAt
+    rw [ofPred_and]
+    apply (reallyConvex_contMDiffAt ..).inter
     let v : Germ (𝓝 x) F →ₛₗ[smoothGerm.valueRingHom I x] F := Filter.Germ.valueₛₗ I x
     change ReallyConvex (smoothGerm I x) (v ⁻¹' {y | P x y})
     dsimp only [← smoothGerm.valueOrderRingHom_toRingHom] at v
@@ -140,8 +140,8 @@ theorem exists_contMDiff_of_convex₂ {P : M₁ → (M₂ → F) → Prop} [Sigm
   let PP : (Σ x : M₁, Germ (𝓝 x) (M₂ → F)) → Prop := fun p ↦
     p.2.ContMDiffAtProd I₁ I₂ n ∧ P p.1 p.2.value
   have hPP : ∀ x : M₁, ReallyConvex (smoothGerm I₁ x) {φ | PP ⟨x, φ⟩} := fun x ↦ by
-    apply ReallyConvex.inter
-    · apply reallyConvex_contMDiffAtProd
+    rw [ofPred_and]
+    apply (reallyConvex_contMDiffAtProd ..).inter
     let v : Germ (𝓝 x) (M₂ → F) →ₛₗ[smoothGerm.valueRingHom I₁ x] M₂ → F := Filter.Germ.valueₛₗ I₁ x
     change ReallyConvex (smoothGerm I₁ x) (v ⁻¹' {y | P x y})
     dsimp only [← smoothGerm.valueOrderRingHom_toRingHom] at v

SphereEversion/ToMathlib/SmoothBarycentric.lean

@@ -136,7 +136,7 @@ theorem contDiff_barycentric [DecidablePred (· ∈ affineBases ι 𝕜 F)] [Fin
   simp only [Matrix.cramer_transpose_apply]
   have hcont : ContDiff 𝕜 n fun x : ι → F ↦ b.toMatrix x :=
     contDiff_pi.mpr fun j ↦ contDiff_pi.mpr fun j' ↦
-      ((smooth_barycentric_coord b j').of_le le_top).comp (contDiff_apply 𝕜 _ j)
+      ((contDiff_barycentric_coord b j').of_le le_top).comp (contDiff_apply 𝕜 _ j)
   have h_snd : ContDiff 𝕜 n fun x : F × (ι → F) ↦ b.toMatrix x.snd := hcont.comp contDiff_snd
   apply ContDiffOn.mul
   · apply ((Matrix.contDiff_det ι 𝕜 n).comp h_snd).contDiffOn.inv
@@ -150,8 +150,8 @@ theorem contDiff_barycentric [DecidablePred (· ∈ affineBases ι 𝕜 F)] [Fin
     simp only [AffineBasis.toMatrix_apply, AffineBasis.coords_apply]
     by_cases hij : j = i
     · simp only [hij, ite_true]
-      exact (smooth_barycentric_coord b j').fst'.of_le le_top
+      exact (contDiff_barycentric_coord b j').fst'.of_le le_top
     · simp only [hij, ite_false]
-      exact ((smooth_barycentric_coord b j').of_le le_top).comp (contDiff_pi.mp contDiff_snd j)
+      exact ((contDiff_barycentric_coord b j').of_le le_top).comp (contDiff_pi.mp contDiff_snd j)
 
 end contDiff_barycentric

lake-manifest.json

@@ -15,17 +15,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "56a005855ea17e0b0958f73ec801ae140b0a1679",
+   "rev": "b575e0bbdec41cf856f3f53ee0d30f83820c645b",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.35.0",
+   "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dfa4f38190d07c37e315953e08b90fe2d95b3c24",
+   "rev": "c2d7840c65673533e15b499f25beecdc6227f7d8",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d6b4c7be5be75ec4917c873ac50c756dc1436372",
+   "rev": "9d39f9bb0c30aa2f6200808805ff16e6ce950890",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93",
+   "rev": "19a8e822bfeace1ae4e090045aad81e0c930e6cf",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "df72b022e558978a1c50264cfc4d7fec86fa8e04",
+   "rev": "ff78fbc75a9bffb4ef08f8c290e268d120cd27d7",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4a174c490d8707121c4a9290800489f105d85e07",
+   "rev": "29c64c56cc38211d39b306db2df11701e3d3de11",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dce0ad79c486cb1fb504af04f953c3466b0c6db8",
+   "rev": "6d26f8bb4b2bb78f929ad160feac508866821316",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "66e469188fe07963e5cf666c7d4433f45b8131c5",
+   "rev": "8e746d768c73b716c7d4bc07bd8e73f2a75bdb60",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "c24fe6078c630e89b489bffe59b3e20ac30d12c8",
+   "rev": "34d2efffcb6dc8d5f3537cf6a7f88bfaa999ec49",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.35.0",
+   "inputRev": "v4.36.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "SphereEversion",

lakefile.toml

@@ -11,7 +11,6 @@ weak.linter.style.header = false
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.35.0"
 
 [[require]]
 name = "checkdecls"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.35.0
+leanprover/lean4:v4.36.0-rc1