chore: bump to current mathlib

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

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. -/

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 ψ) :=

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

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]

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 < ε) :

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 : ℝ)) :=

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
-    · 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]
+  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,15 +223,15 @@ 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, 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)
     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)

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 -/

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

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

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,15 +56,15 @@ 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]
     have hu := b.isUnit_toMatrix ⟨v, h.1, h.2⟩
     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

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

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