chore: bump to mathlib 4.33

SphereEversion/Global/Gromov.lean

@@ -29,12 +29,13 @@ variable {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] [FiniteDimens
 
 @[inherit_doc] local notation "J¹" => OneJetBundle IM M IX X
 
+set_option backward.isDefEq.respectTransparency.types false in
 theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R) (hA : IsClosed A)
     (hδ_pos : ∀ x, 0 < δ x) (hδ_cont : Continuous δ) : R.SatisfiesHPrinciple A δ := by
   borelize EX
-  letI := manifoldMetric IM M
-  haveI := Manifold.locallyCompact_of_finiteDimensional (M := M) (I := IM)
-  haveI := Manifold.locallyCompact_of_finiteDimensional (M := X) (I := IX)
+  let := manifoldMetric IM M
+  have := Manifold.locallyCompact_of_finiteDimensional (M := M) (I := IM)
+  have := Manifold.locallyCompact_of_finiteDimensional (M := X) (I := IX)
   refine RelMfld.satisfiesHPrinciple_of_weak hA fun A hA 𝓕₀ h𝓕₀ ↦ ?_
   obtain (hM | hM) := isEmpty_or_nonempty M
   · refine ⟨emptyHtpyFormalSol R, ?_, ?_, ?_, ?_⟩ <;> intro
@@ -201,13 +202,11 @@ variable {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimens
   {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
   [IsManifold I' ∞ M'] [SigmaCompactSpace M'] [T2Space M']
 
-/-
-Since every (σ-compact) manifold is metrizable, the metric space assumption can be removed.
--/
+/- Since every (σ-compact) manifold is metrizable, the metric space assumption can be removed. -/
 /-- Gromov's Theorem without metric space assumption -/
 theorem RelMfld.Ample.satisfiesHPrincipleWith' {R : RelMfld IM M I' M'} (hRample : R.Ample)
     (hRopen : IsOpen R) (hC : IsClosed C) (hδ_pos : ∀ x, 0 < δ x) (hδ_cont : Continuous δ) :
     letI := manifoldMetric I' M'
     R.SatisfiesHPrincipleWith IP C δ := by
-  letI := manifoldMetric I' M'
+  let := manifoldMetric I' M'
   apply RelMfld.Ample.satisfiesHPrincipleWith <;> assumption

SphereEversion/Global/Immersion.lean

@@ -85,7 +85,7 @@ theorem immersionRel_ample (h : finrank ℝ E < finrank ℝ E') : (immersionRel
   rw [RelMfld.ample_iff]
   rintro ⟨⟨m, m'⟩, φ : TangentSpace% m →L[ℝ] TangentSpace% m'⟩ (p : DualPair (TangentSpace% m))
     (hφ : Injective φ)
-  haveI : FiniteDimensional ℝ (TangentSpace% m) := (by infer_instance : FiniteDimensional ℝ E)
+  have : FiniteDimensional ℝ (TangentSpace% m) := inferInstanceAs <| FiniteDimensional ℝ E
   have hcodim := one_lt_rank_of_rank_lt_rank p.ker_pi_ne_top h φ.toLinearMap
   rw [immersionRel_slice_eq I I' hφ]
   exact AmpleSet.of_one_lt_codim hcodim
@@ -132,7 +132,7 @@ variable {n : ℕ} (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E]
 theorem immersion_inclusion_sphere : Immersion (𝓡 n) 𝓘(ℝ, E)
     (fun x : sphere (0 : E) 1 ↦ (x : E)) ∞ where
   contMDiff := contMDiff_coe_sphere.of_le le_top
-  diff_injective := mfderiv_coe_sphere_injective
+  diff_injective := injective_mvfderiv_subtypeVal_sphere
 
 /-- The antipodal map on `𝕊^n ⊆ ℝ^{n+1}` is an immersion. -/
 theorem immersion_antipodal_sphere : Immersion (𝓡 n) 𝓘(ℝ, E)
@@ -144,7 +144,7 @@ theorem immersion_antipodal_sphere : Immersion (𝓡 n) 𝓘(ℝ, E)
   diff_injective x := by
     change Injective (mfderiv% (-fun x : sphere (0 : E) 1 ↦ (x : E)) x)
     rw [mfderiv_neg]
-    exact neg_injective.comp (mfderiv_coe_sphere_injective x)
+    exact neg_injective.comp (injective_mvfderiv_subtypeVal_sphere x)
 
 end sanitycheck
 
@@ -191,7 +191,7 @@ def formalEversionAux : FamilyOneJetSec (𝓡 2) 𝕊² 𝓘(ℝ, E) E 𝓘(ℝ,
 /-- A formal eversion of a two-sphere into its ambient Euclidean space. -/
 def formalEversionAux2 : HtpyFormalSol 𝓡_imm :=
   { formalEversionAux E ω with
-    is_sol' := fun t x ↦ (ω.isometry_rot t x).injective.comp (mfderiv_coe_sphere_injective x) }
+    is_sol' t x := (ω.isometry_rot t x).injective.comp (injective_mvfderiv_subtypeVal_sphere x) }
 
 def formalEversion : HtpyFormalSol 𝓡_imm :=
   (formalEversionAux2 E ω).reindex ⟨smoothStep, contMDiff_iff_contDiff.mpr smoothStep.smooth⟩
@@ -206,6 +206,7 @@ theorem formalEversion_zero (x : 𝕊²) : (formalEversion E ω 0).bs x = x := b
 
 theorem formalEversion_one (x : 𝕊²) : (formalEversion E ω 1).bs x = -x := by simp
 
+set_option backward.isDefEq.respectTransparency.types false in
 theorem formalEversionHolAtZero {t : ℝ} (ht : t < 1 / 4) :
     (formalEversion E ω t).toOneJetSec.IsHolonomic := by
   intro x
@@ -232,7 +233,7 @@ theorem formalEversionHolAtOne {t : ℝ} (ht : 3 / 4 < t) :
   erw [mfderiv_neg, ContinuousLinearMap.coe_comp, Function.comp_apply, _root_.neg_apply,
     smoothStep.of_gt ht]
   rw [ω.rot_one]; · rfl
-  rw [← range_mfderiv_coe_sphere (n := 2) x]
+  rw [← range_mvfderiv_subtypeVal (n := 2) x]
   exact LinearMap.mem_range_self ..
 
 theorem formalEversion_hol_near_zero_one :
@@ -308,13 +309,13 @@ theorem sphere_eversion :
     ((stdOrthonormalBasis _ _).reindex <|
           finCongr (Fact.out : finrank ℝ E = 3)).toBasis.orientation
   have rankE : finrank ℝ E = 3 := Fact.out
-  haveI : FiniteDimensional ℝ E := FiniteDimensional.of_finrank_eq_succ rankE
+  have : FiniteDimensional ℝ E := FiniteDimensional.of_finrank_eq_succ rankE
   have ineq_rank : finrank ℝ (EuclideanSpace ℝ (Fin 2)) < finrank ℝ E := by simp [rankE]
   let ε : 𝕊² → ℝ := fun _ ↦ 1
   have hε_pos : ∀ x, 0 < ε x := fun _ ↦ zero_lt_one
   have hε_cont : Continuous ε := continuous_const
-  haveI : Nontrivial E := nontrivial_of_finrank_eq_succ (Fact.out : finrank ℝ E = 3)
-  haveI : Nonempty (sphere 0 1 : Set E) :=
+  have : Nontrivial E := nontrivial_of_finrank_eq_succ (Fact.out : finrank ℝ E = 3)
+  have : Nonempty (sphere 0 1 : Set E) :=
     (NormedSpace.sphere_nonempty.mpr zero_le_one).to_subtype
   rcases(immersionRel_satisfiesHPrincipleWith (𝓡 2) 𝕊² 𝓘(ℝ, E) E 𝓘(ℝ, ℝ) ℝ ineq_rank
           ((Finite.isClosed (by simp : ({0, 1} : Set ℝ).Finite)).prod isClosed_univ) hε_pos

SphereEversion/Global/Localisation.lean

@@ -24,6 +24,7 @@ Now we really bridge the gap all the way to vector spaces.
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
   {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E']
 
+set_option backward.isDefEq.respectTransparency.types false in
 /-- Convert a 1-jet section between vector spaces seen as manifold to a 1-jet section
 between those vector spaces. -/
 def OneJetSec.loc (F : OneJetSec 𝓘(ℝ, E) E 𝓘(ℝ, E') E') : JetSec E E' where
@@ -68,6 +69,7 @@ section Unloc
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
   {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E']
 
+set_option backward.isDefEq.respectTransparency.types false in
 /-- Convert a 1-jet section between vector spaces to a 1-jet section
 between those vector spaces seen as manifolds. -/
 def JetSec.unloc (𝓕 : JetSec E E') : OneJetSec 𝓘(ℝ, E) E 𝓘(ℝ, E') E' where

SphereEversion/Global/OneJetBundle.lean

@@ -402,6 +402,7 @@ theorem ContMDiff.oneJetExt {f : M → M'} (hf : CMDiff ∞ f) :
     ContMDiff I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ (oneJetExt I I' f) :=
   fun x ↦ ((hf x).contMDiffAt univ_mem).oneJetExt
 
+set_option backward.isDefEq.respectTransparency.types false in
 theorem ContinuousAt.inTangentCoordinates_comp {f : N → M} {g : N → M'} {h : N → N'}
     {ϕ' : N → E' →L[𝕜] F'} {ϕ : N → E →L[𝕜] E'} {x₀ : N} (hg : ContinuousAt g x₀) :
     inTangentCoordinates I J' f h (fun x ↦ ϕ' x ∘L ϕ x) x₀ =ᶠ[𝓝 x₀] fun x ↦
@@ -428,6 +429,7 @@ variable (I')
 
 variable [IsManifold J ∞ N]
 
+set_option backward.isDefEq.respectTransparency.types false in
 omit [IsManifold J' ∞ N'] in
 theorem ContMDiffAt.oneJet_comp {f1 : N' → M} (f2 : N' → M') {f3 : N' → N} {x₀ : N'}
     {h : ∀ x : N', OneJetSpace I' J (f2 x, f3 x)} {g : ∀ x : N', OneJetSpace I I' (f1 x, f2 x)}
@@ -602,6 +604,7 @@ theorem partialEquiv_eq_equiv {α β} {f : PartialEquiv α β} {e : α ≃ β} (
 
 @[inherit_doc] local notation "𝓜" => ModelProd (ModelProd H H') (E →L[𝕜] E')
 
+set_option backward.isDefEq.respectTransparency.types false in
 /-- In the `OneJetBundle` to the model space, the charts are just the canonical identification
 between a product type and a bundle total space type, a.k.a. `Bundle.TotalSpace.toProd`. -/
 @[simp, mfld_simps]
@@ -620,6 +623,7 @@ theorem oneJetBundle_model_space_chartAt (p : OneJetBundle I H I' H') :
       OpenPartialHomeomorph.refl_prod_refl]
     rfl
 
+set_option backward.isDefEq.respectTransparency.types false in
 @[simp, mfld_simps]
 theorem oneJetBundle_model_space_coe_chartAt (p : OneJetBundle I H I' H') :
     ⇑(chartAt 𝓜 p) = Bundle.TotalSpace.toProd (H × H') (E →L[𝕜] E') := by

SphereEversion/Global/OneJetSec.lean

@@ -110,6 +110,7 @@ theorem isHolonomicAt_iff {F : OneJetSec I M I' M'} {x : M} :
   simp_rw [IsHolonomicAt, oneJetExt, Bundle.TotalSpace.ext_iff, heq_iff_eq, F.fst_eq,
     oneJetBundle_mk_fst, true_and, oneJetBundle_mk_snd]
 
+set_option backward.isDefEq.respectTransparency.types false in
 theorem isHolonomicAt_congr {F F' : OneJetSec I M I' M'} {x : M} (h : F =ᶠ[𝓝 x] F') :
     F.IsHolonomicAt x ↔ F'.IsHolonomicAt x := by
   simp_rw [IsHolonomicAt]
@@ -133,7 +134,7 @@ end OneJetSec
 def IsHolonomicGerm {x : M} (φ : Germ (𝓝 x) (OneJetBundle I M I' M')) : Prop :=
   Quotient.liftOn' φ (fun F ↦ mfderiv% (fun x' ↦ (F x').1.2) x = (F x).2)
     (by
-      letI : Setoid (M → OneJetBundle I M I' M') := (𝓝 x).germSetoid (OneJetBundle I M I' M')
+      let : Setoid (M → OneJetBundle I M I' M') := (𝓝 x).germSetoid (OneJetBundle I M I' M')
       have key :
         ∀ f g,
           f ≈ g →

SphereEversion/Global/Relation.lean

@@ -177,7 +177,7 @@ def RelMfld.slice (R : RelMfld I M I' M') (σ : OneJetBundle I M I' M') (p : Dua
   {w : TM' σ.1.2 | OneJetBundle.mk σ.1.1 σ.1.2 (p.update σ.2 w) ∈ R}
 
 omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
-/-- For some reason `rw [mem_setOf_eq]` fails after unfolding `slice`,
+/-- For some reason `rw [mem_ofPred_eq]` fails after unfolding `slice`,
 but rewriting with this lemma works. -/
 theorem mem_slice {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'} {p : DualPair <| TM σ.1.1}
     {w : TM' σ.1.2} : w ∈ R.slice σ p ↔ OneJetBundle.mk σ.1.1 σ.1.2 (p.update σ.2 w) ∈ R :=
@@ -198,6 +198,7 @@ theorem slice_mk_update {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'}
 def RelMfld.Ample (R : RelMfld I M I' M') : Prop :=
   ∀ ⦃σ : OneJetBundle I M I' M'⦄ (p : DualPair <| TM σ.1.1), AmpleSet (R.slice σ p)
 
+set_option backward.isDefEq.respectTransparency.types false in
 omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 theorem RelMfld.ample_iff (R : RelMfld I M I' M') :
     R.Ample ↔
@@ -349,8 +350,7 @@ def RelMfld.SatisfiesHPrinciple (R : RelMfld I M IX X) (C : Set M) (ε : M → 
 theorem RelMfld.satisfiesHPrinciple_of_weak [FiniteDimensional ℝ E] [T2Space M]
     [SigmaCompactSpace M] {R : RelMfld I M IX X} {ε : M → ℝ} {C : Set M} (hC : IsClosed C)
     (h : ∀ A : Set M, IsClosed A → R.SatisfiesHPrincipleWeak A ε) : R.SatisfiesHPrinciple C ε := by
-  haveI := Manifold.metrizableSpace I M
-  letI : MetricSpace M := TopologicalSpace.metrizableSpaceMetric M
+  have := Manifold.metrizableSpace I M
   intro 𝓕₀ h𝓕₀
   obtain ⟨C', hCC', hC', h𝓕₀C'⟩ := h𝓕₀.closed_neighborhood hC
   obtain ⟨𝓕, h1, h2, h3, h4⟩ := h C' hC' 𝓕₀ h𝓕₀C'
@@ -480,6 +480,7 @@ theorem OpenSmoothEmbedding.smooth_transfer :
 theorem OneJetBundle.continuous_transfer : Continuous (φ.transfer ψ) :=
   (OpenSmoothEmbedding.smooth_transfer _ _).continuous
 
+set_option backward.isDefEq.respectTransparency.types false in
 omit [IsManifold IX ∞ X] [IsManifold IM ∞ M]
   [IsManifold IY ∞ Y] [IsManifold IN ∞ N] in
 theorem OpenSmoothEmbedding.range_transfer :
@@ -706,6 +707,7 @@ theorem Jupdate_bs (F : OneJetSec IM M IN N) (G : HtpyOneJetSec IX X IY Y) (t :
       if x ∈ range φ then _ else _
   split_ifs <;> rfl
 
+set_option backward.isDefEq.respectTransparency.types false in
 theorem Jupdate_localize {F : OneJetSec IM M IN N} {G : HtpyOneJetSec IX X IY Y} (hK : IsCompact K)
     (hFG : ∀ t, ∀ x ∉ K, F (φ x) = (OneJetBundle.embedding φ ψ) (G t x)) (t : ℝ)
     (rg : range ((φ.Jupdate ψ F G hK hFG t).bs ∘ φ) ⊆ range ψ) (x : X) :

SphereEversion/Global/TwistOneJetSec.lean

@@ -208,6 +208,7 @@ theorem FamilyOneJetEuclSec.contMDiff (s : FamilyOneJetEuclSec I M V J N) :
 
 variable {V'}
 
+set_option backward.isDefEq.respectTransparency.types false in
 def familyJoin {f : N × M → V} (hf : CMDiff ∞ f)
     (s : FamilyOneJetEuclSec I M V J N) : FamilyOneJetSec I M 𝓘(ℝ, V) V J N
     where

SphereEversion/Indexing.lean

@@ -64,7 +64,6 @@ theorem Set.countable_iff_exists_nonempty_indexType_equiv {α : Type*} {s : Set
   · refine ⟨fun hh ↦ ⟨0, ?_⟩, ?_⟩
     · simp only [indexType_zero]
       obtain ⟨_i⟩ := Set.countable_infinite_iff_nonempty_denumerable.mp ⟨hh, h⟩
-      haveI := _i
       exact ⟨(Denumerable.eqv s).symm⟩
     · rintro ⟨n, ⟨fn⟩⟩
       have hn : n = 0 := by

SphereEversion/InductiveConstructions.lean

@@ -93,6 +93,7 @@ theorem inductive_construction {X Y : Type*} [TopologicalSpace X] {N : ℕ} {U :
     convert (h₁f _ _ hn₀' x) using 1
     exact Germ.coe_eq.mpr hn₀.symm
 
+set_option backward.isDefEq.respectTransparency.types false in
 theorem inductive_construction_of_loc' {X Y : Type*} [EMetricSpace X] [LocallyCompactSpace X]
     [SecondCountableTopology X] (P₀ P₀' P₁ : ∀ x : X, Germ (𝓝 x) Y → Prop) {f₀ : X → Y}
     (hP₀f₀ : ∀ x, P₀ x f₀ ∧ P₀' x f₀)

SphereEversion/Local/AmpleRelation.lean

@@ -86,7 +86,7 @@ theorem slice_of_ker_eq_ker {θ : OneJet E F} {p p' : DualPair E} (hpp' : p.π =
     congr 2
     abel
   ext w
-  simp only [slice, mem_setOf_eq, map_sub, vadd_eq_add, mem_vadd_set_iff_neg_vadd_mem, key]
+  simp only [slice, mem_ofPred_eq, map_sub, vadd_eq_add, mem_vadd_set_iff_neg_vadd_mem, key]
   have : -(φ p.v - φ p'.v) + w + (φ p.v - φ p'.v) = w := by abel
   rw [this]
 

SphereEversion/Local/SphereEversion.lean

@@ -228,7 +228,7 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank 
   rw [injOn_iff_injective]
   let j := (ℝ ∙ x)ᗮ.subtypeL
   let p'' : DualPair (ℝ ∙ x)ᗮ := ⟨p.π.comp j, ⟨v', v'_in⟩, hπv'⟩
-  have eq : ((ℝ ∙ x)ᗮ : Set E).restrict (p'.update φ w) = p''.update (φ.comp j) w := by
+  have eq : ((ℝ ∙ x)ᗮ : Set E).domRestrict (p'.update φ w) = p''.update (φ.comp j) w := by
     ext z
     simp [p', j, DualPair.update, p'']
   have eq' : (p''.π.ker).map (φ.comp j : _ →ₛₗ[.id ℝ] F) =
@@ -244,7 +244,7 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank 
     erw [← this, map_comp]
   rw [eq, p''.injective_update_iff, mem_compl_iff, eq']
   · exact Iff.rfl
-  rw [← show ((ℝ ∙ x)ᗮ : Set E).restrict φ = φ.comp j by ext; rfl]
+  rw [← show ((ℝ ∙ x)ᗮ : Set E).domRestrict φ = φ.comp j by ext; rfl]
   exact hφ.injective
 
 end AssumeFiniteDimensional
@@ -415,7 +415,7 @@ theorem sphere_eversion_of_loc [Fact (dim E = 3)] :
   classical
   borelize E
   have rankE : (dim E = 3) := Fact.out
-  haveI : FiniteDimensional ℝ E := FiniteDimensional.of_finrank_eq_succ rankE
+  have : FiniteDimensional ℝ E := FiniteDimensional.of_finrank_eq_succ rankE
   let ω : Orientation ℝ E (Fin 3) :=
     ((stdOrthonormalBasis _ _).reindex <| finCongr rankE).toBasis.orientation
   have is_closed_pair : IsClosed ({0, 1} : Set ℝ) := (by simp : ({0, 1} : Set ℝ).Finite).isClosed

SphereEversion/Loops/Basic.lean

@@ -378,6 +378,7 @@ theorem ContDiff.partial_loop {γ : E → Loop F} {n : ℕ∞} (hγ_diff : 𝒞
 
 variable [FiniteDimensional ℝ F]
 
+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]

SphereEversion/Loops/DeltaMollifier.lean

@@ -125,7 +125,7 @@ theorem ContDiff.periodize {f : ℝ → E} {n : ℕ∞} (h : ContDiff ℝ n f) (
     refine (ProperlyDiscontinuousVAdd.finite_disjoint_inter_image
       (isCompact_Icc : IsCompact <| Icc (y - 1) (y + 1)) h').subset ?_
     intro i hi
-    rw [mem_setOf_eq]
+    rw [mem_ofPred_eq]
     apply Nonempty.mono _ hi
     gcongr
     · rw [show (e i : ℝ → ℝ) = VAdd.vadd i by ext x; exact add_comm x i]

SphereEversion/Loops/Exists.lean

@@ -155,7 +155,7 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op :
   let U₁ : Set ℝ := Iio (4⁻¹ : ℝ) ∪ Ioi (3 / 4)
   let U : Set (E × ℝ × ℝ) := (fun x ↦ x.2.1) ⁻¹' Iio (4⁻¹ : ℝ) ∪ (fun x ↦ fract x.2.2) ⁻¹' U₁
   have hUC : U ∈ 𝓝ˢ C := by
-    haveI hU : IsOpen U := by
+    have hU : IsOpen U := by
       refine (isOpen_Iio.preimage continuous_snd.fst).union ?_
       refine ((isOpen_Iio.union isOpen_Ioi).preimage_fract ?_).preimage continuous_snd.snd
       exact fun _ ↦ Or.inr (show (3 / 4 : ℝ) < 1 by norm_num)

SphereEversion/Loops/Surrounding.lean

@@ -153,10 +153,10 @@ 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₃⟩
-    haveI : Fintype b := (finite_set_of_fin_dim_affineIndependent ℝ h₁).fintype
+    have : Fintype b := (finite_set_of_fin_dim_affineIndependent ℝ h₁).fintype
     have hb : Fintype.card b = d + 1 := by
       rw [← h₁.affineSpan_eq_top_iff_card_eq_finrank_add_one, Subtype.range_coe_subtype,
-        setOf_mem_eq, h₂]
+        ofPred_mem_eq, h₂]
     let p := ((↑) : _ → F) ∘ (Fintype.equivFinOfCardEq hb).symm
     have hp : b = range p := by
       ext x
@@ -166,7 +166,7 @@ theorem surrounded_iff_mem_interior_convexHull_aff_basis [FiniteDimensional ℝ
     replace h₁ : AffineIndependent ℝ p :=
       h₁.comp_embedding (Fintype.equivFinOfCardEq hb).symm.toEmbedding
     let basis : AffineBasis ι ℝ F := ⟨_, h₁, h₂⟩
-    erw [basis.interior_convexHull, mem_setOf_eq] at h₃
+    erw [basis.interior_convexHull, mem_ofPred_eq] at h₃
     refine ⟨p, fun i ↦ basis.coord i f, ⟨h₁, h₃, ?_, ?_⟩, fun i ↦ h₀ (mem_range_self i)⟩
     · exact basis.sum_coord_apply_eq_one f
     · erw [← Finset.univ.affineCombination_eq_linear_combination p _
@@ -216,7 +216,7 @@ theorem smooth_surrounding [FiniteDimensional ℝ F] {x : F} {p : ι → F} {w :
   have hxp : W' (x, p) ∈ V := by simp [W', V, hp, h.coord_eq_w, h.w_pos]
   have hA : IsOpen A := by
     simp only [A, affineBases_findim ι ℝ F hι]
-    exact isOpen_univ.prod isOpen_setOf_affineIndependent
+    exact isOpen_univ.prod isOpen_setOfPred_affineIndependent
   have hU₂ : IsOpen U := hW'.isOpen_inter_preimage hA hV
   have hU₃ : U ∈ 𝓝 (x, p) :=
     mem_nhds_iff.mpr ⟨U, le_refl U, hU₂, Set.mem_inter (by simp [hp, A]) (mem_preimage.mpr hxp)⟩
@@ -238,7 +238,7 @@ theorem smooth_surroundingPts [FiniteDimensional ℝ F] {x : F} {p : ι → F} {
         SmoothAt' (uncurry W) yq ∧ SurroundingPts yq.1 yq.2 (W yq.1 yq.2) := by
   refine Exists.imp (fun W hW ↦ ?_) (smooth_surrounding h)
   rw [nhds_prod_eq] at hW ⊢
-  have := (IsOpen.eventually_mem isOpen_setOf_affineIndependent h.indep).prod_inr (𝓝 x)
+  have := (IsOpen.eventually_mem isOpen_setOfPred_affineIndependent h.indep).prod_inr (𝓝 x)
   filter_upwards [hW, this]; rintro ⟨y, q⟩ ⟨hW, h2W, h3W, hq⟩ h2q
   exact ⟨hW, h2q, h2W, h3W, hq⟩
 
@@ -283,7 +283,7 @@ theorem eventually_surroundingPts_of_tendsto_of_tendsto {l : Filter X} {m : Filt
   have hV' : V ∈ 𝓝 (W' (q, v)) := (isOpen_set_pi finite_univ fun _ _ ↦ isOpen_Ioi).mem_nhds hxp
   have hA : IsOpen A := by
     simp only [A, affineBases_findim ι ℝ F hι]
-    exact isOpen_univ.prod isOpen_setOf_affineIndependent
+    exact isOpen_univ.prod isOpen_setOfPred_affineIndependent
   have hW' : ContinuousAt W' (q, v) :=
     (smooth_barycentric ι ℝ F hι (n := 0)).continuousOn.continuousAt
       (mem_nhds_iff.mpr ⟨A, Subset.rfl, hA, hqv⟩)
@@ -937,7 +937,7 @@ def ContinuousGerm {x : E} (φ : Germ (𝓝 x) (ℝ → Loop F)) : Prop :=
       rw [nhds_prod_eq]
       apply mem_of_superset (Filter.prod_mem_prod h univ_mem)
       rintro ⟨x', p⟩ ⟨hx' : γ x' = γ' x', -⟩
-      simp only [mem_setOf_eq, hx'])
+      simp only [mem_ofPred_eq, hx'])
 
 variable (g b Ω)
 omit [NormedSpace ℝ E]