bump to nightly-2023-12-03-06

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/AlgebraicGeometry/OpenImmersion/Scheme.lean

@@ -291,7 +291,7 @@ theorem affineBasisCover_is_basis (X : Scheme) :
       {x : Set X.carrier |
         ∃ a : X.affineBasisCover.J, x = Set.range (X.affineBasisCover.map a).1.base} :=
   by
-  apply TopologicalSpace.isTopologicalBasis_of_open_of_nhds
+  apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
   · rintro _ ⟨a, rfl⟩
     exact is_open_immersion.open_range (X.affine_basis_cover.map a)
   · rintro a U haU hU

Mathbin/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -1017,7 +1017,7 @@ theorem isTopologicalBasis_basic_opens :
     TopologicalSpace.IsTopologicalBasis
       (Set.range fun r : R => (basicOpen r : Set (PrimeSpectrum R))) :=
   by
-  apply TopologicalSpace.isTopologicalBasis_of_open_of_nhds
+  apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
   · rintro _ ⟨r, rfl⟩
     exact is_open_basic_open
   · rintro p U hp ⟨s, hs⟩

Mathbin/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean

@@ -585,7 +585,7 @@ theorem isTopologicalBasis_basic_opens :
     TopologicalSpace.IsTopologicalBasis
       (Set.range fun r : A => (basicOpen 𝒜 r : Set (ProjectiveSpectrum 𝒜))) :=
   by
-  apply TopologicalSpace.isTopologicalBasis_of_open_of_nhds
+  apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
   · rintro _ ⟨r, rfl⟩
     exact is_open_basic_open 𝒜
   · rintro p U hp ⟨s, hs⟩

Mathbin/Analysis/Calculus/ContDiff.lean

@@ -2738,17 +2738,17 @@ theorem contDiffOn_succ_iff_derivWithin {n : ℕ} (hs : UniqueDiffOn 𝕜 s₂)
 -/
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `congrm #[[expr «expr ∧ »(_, _)]] -/
-#print contDiffOn_succ_iff_deriv_of_open /-
+#print contDiffOn_succ_iff_deriv_of_isOpen /-
 /-- A function is `C^(n + 1)` on an open domain if and only if it is
 differentiable there, and its derivative (formulated with `deriv`) is `C^n`. -/
-theorem contDiffOn_succ_iff_deriv_of_open {n : ℕ} (hs : IsOpen s₂) :
+theorem contDiffOn_succ_iff_deriv_of_isOpen {n : ℕ} (hs : IsOpen s₂) :
     ContDiffOn 𝕜 (n + 1 : ℕ) f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 n (deriv f₂) s₂ :=
   by
   rw [contDiffOn_succ_iff_derivWithin hs.unique_diff_on]
   trace
     "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `congrm #[[expr «expr ∧ »(_, _)]]"
-  exact contDiffOn_congr fun _ => derivWithin_of_open hs
-#align cont_diff_on_succ_iff_deriv_of_open contDiffOn_succ_iff_deriv_of_open
+  exact contDiffOn_congr fun _ => derivWithin_of_isOpen hs
+#align cont_diff_on_succ_iff_deriv_of_open contDiffOn_succ_iff_deriv_of_isOpen
 -/
 
 #print contDiffOn_top_iff_derivWithin /-
@@ -2771,17 +2771,17 @@ theorem contDiffOn_top_iff_derivWithin (hs : UniqueDiffOn 𝕜 s₂) :
 -/
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `congrm #[[expr «expr ∧ »(_, _)]] -/
-#print contDiffOn_top_iff_deriv_of_open /-
+#print contDiffOn_top_iff_deriv_of_isOpen /-
 /-- A function is `C^∞` on an open domain if and only if it is differentiable
 there, and its derivative (formulated with `deriv`) is `C^∞`. -/
-theorem contDiffOn_top_iff_deriv_of_open (hs : IsOpen s₂) :
+theorem contDiffOn_top_iff_deriv_of_isOpen (hs : IsOpen s₂) :
     ContDiffOn 𝕜 ∞ f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 ∞ (deriv f₂) s₂ :=
   by
   rw [contDiffOn_top_iff_derivWithin hs.unique_diff_on]
   trace
     "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `congrm #[[expr «expr ∧ »(_, _)]]"
-  exact contDiffOn_congr fun _ => derivWithin_of_open hs
-#align cont_diff_on_top_iff_deriv_of_open contDiffOn_top_iff_deriv_of_open
+  exact contDiffOn_congr fun _ => derivWithin_of_isOpen hs
+#align cont_diff_on_top_iff_deriv_of_open contDiffOn_top_iff_deriv_of_isOpen
 -/
 
 #print ContDiffOn.derivWithin /-
@@ -2798,11 +2798,11 @@ theorem ContDiffOn.derivWithin (hf : ContDiffOn 𝕜 n f₂ s₂) (hs : UniqueDi
 #align cont_diff_on.deriv_within ContDiffOn.derivWithin
 -/
 
-#print ContDiffOn.deriv_of_open /-
-theorem ContDiffOn.deriv_of_open (hf : ContDiffOn 𝕜 n f₂ s₂) (hs : IsOpen s₂) (hmn : m + 1 ≤ n) :
+#print ContDiffOn.deriv_of_isOpen /-
+theorem ContDiffOn.deriv_of_isOpen (hf : ContDiffOn 𝕜 n f₂ s₂) (hs : IsOpen s₂) (hmn : m + 1 ≤ n) :
     ContDiffOn 𝕜 m (deriv f₂) s₂ :=
-  (hf.derivWithin hs.UniqueDiffOn hmn).congr fun x hx => (derivWithin_of_open hs hx).symm
-#align cont_diff_on.deriv_of_open ContDiffOn.deriv_of_open
+  (hf.derivWithin hs.UniqueDiffOn hmn).congr fun x hx => (derivWithin_of_isOpen hs hx).symm
+#align cont_diff_on.deriv_of_open ContDiffOn.deriv_of_isOpen
 -/
 
 #print ContDiffOn.continuousOn_derivWithin /-
@@ -2812,19 +2812,19 @@ theorem ContDiffOn.continuousOn_derivWithin (h : ContDiffOn 𝕜 n f₂ s₂) (h
 #align cont_diff_on.continuous_on_deriv_within ContDiffOn.continuousOn_derivWithin
 -/
 
-#print ContDiffOn.continuousOn_deriv_of_open /-
-theorem ContDiffOn.continuousOn_deriv_of_open (h : ContDiffOn 𝕜 n f₂ s₂) (hs : IsOpen s₂)
+#print ContDiffOn.continuousOn_deriv_of_isOpen /-
+theorem ContDiffOn.continuousOn_deriv_of_isOpen (h : ContDiffOn 𝕜 n f₂ s₂) (hs : IsOpen s₂)
     (hn : 1 ≤ n) : ContinuousOn (deriv f₂) s₂ :=
-  ((contDiffOn_succ_iff_deriv_of_open hs).1 (h.of_le hn)).2.ContinuousOn
-#align cont_diff_on.continuous_on_deriv_of_open ContDiffOn.continuousOn_deriv_of_open
+  ((contDiffOn_succ_iff_deriv_of_isOpen hs).1 (h.of_le hn)).2.ContinuousOn
+#align cont_diff_on.continuous_on_deriv_of_open ContDiffOn.continuousOn_deriv_of_isOpen
 -/
 
 #print contDiff_succ_iff_deriv /-
 /-- A function is `C^(n + 1)` if and only if it is differentiable,
   and its derivative (formulated in terms of `deriv`) is `C^n`. -/
 theorem contDiff_succ_iff_deriv {n : ℕ} :
     ContDiff 𝕜 (n + 1 : ℕ) f₂ ↔ Differentiable 𝕜 f₂ ∧ ContDiff 𝕜 n (deriv f₂) := by
-  simp only [← contDiffOn_univ, contDiffOn_succ_iff_deriv_of_open, isOpen_univ,
+  simp only [← contDiffOn_univ, contDiffOn_succ_iff_deriv_of_isOpen, isOpen_univ,
     differentiableOn_univ]
 #align cont_diff_succ_iff_deriv contDiff_succ_iff_deriv
 -/

Mathbin/Analysis/Calculus/ContDiffDef.lean

@@ -1393,10 +1393,10 @@ theorem contDiffOn_succ_iff_has_fderiv_within {n : ℕ} (hs : UniqueDiffOn 𝕜
 -/
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `congrm #[[expr «expr ∧ »(_, _)]] -/
-#print contDiffOn_succ_iff_fderiv_of_open /-
+#print contDiffOn_succ_iff_fderiv_of_isOpen /-
 /-- A function is `C^(n + 1)` on an open domain if and only if it is
 differentiable there, and its derivative (expressed with `fderiv`) is `C^n`. -/
-theorem contDiffOn_succ_iff_fderiv_of_open {n : ℕ} (hs : IsOpen s) :
+theorem contDiffOn_succ_iff_fderiv_of_isOpen {n : ℕ} (hs : IsOpen s) :
     ContDiffOn 𝕜 (n + 1 : ℕ) f s ↔
       DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 n (fun y => fderiv 𝕜 f y) s :=
   by
@@ -1406,7 +1406,7 @@ theorem contDiffOn_succ_iff_fderiv_of_open {n : ℕ} (hs : IsOpen s) :
   apply contDiffOn_congr
   intro x hx
   exact fderivWithin_of_isOpen hs hx
-#align cont_diff_on_succ_iff_fderiv_of_open contDiffOn_succ_iff_fderiv_of_open
+#align cont_diff_on_succ_iff_fderiv_of_open contDiffOn_succ_iff_fderiv_of_isOpen
 -/
 
 #print contDiffOn_top_iff_fderivWithin /-
@@ -1430,10 +1430,10 @@ theorem contDiffOn_top_iff_fderivWithin (hs : UniqueDiffOn 𝕜 s) :
 -/
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `congrm #[[expr «expr ∧ »(_, _)]] -/
-#print contDiffOn_top_iff_fderiv_of_open /-
+#print contDiffOn_top_iff_fderiv_of_isOpen /-
 /-- A function is `C^∞` on an open domain if and only if it is differentiable there, and its
 derivative (expressed with `fderiv`) is `C^∞`. -/
-theorem contDiffOn_top_iff_fderiv_of_open (hs : IsOpen s) :
+theorem contDiffOn_top_iff_fderiv_of_isOpen (hs : IsOpen s) :
     ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (fun y => fderiv 𝕜 f y) s :=
   by
   rw [contDiffOn_top_iff_fderivWithin hs.unique_diff_on]
@@ -1442,7 +1442,7 @@ theorem contDiffOn_top_iff_fderiv_of_open (hs : IsOpen s) :
   apply contDiffOn_congr
   intro x hx
   exact fderivWithin_of_isOpen hs hx
-#align cont_diff_on_top_iff_fderiv_of_open contDiffOn_top_iff_fderiv_of_open
+#align cont_diff_on_top_iff_fderiv_of_open contDiffOn_top_iff_fderiv_of_isOpen
 -/
 
 #print ContDiffOn.fderivWithin /-
@@ -1459,11 +1459,11 @@ theorem ContDiffOn.fderivWithin (hf : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn
 #align cont_diff_on.fderiv_within ContDiffOn.fderivWithin
 -/
 
-#print ContDiffOn.fderiv_of_open /-
-theorem ContDiffOn.fderiv_of_open (hf : ContDiffOn 𝕜 n f s) (hs : IsOpen s) (hmn : m + 1 ≤ n) :
+#print ContDiffOn.fderiv_of_isOpen /-
+theorem ContDiffOn.fderiv_of_isOpen (hf : ContDiffOn 𝕜 n f s) (hs : IsOpen s) (hmn : m + 1 ≤ n) :
     ContDiffOn 𝕜 m (fun y => fderiv 𝕜 f y) s :=
   (hf.fderivWithin hs.UniqueDiffOn hmn).congr fun x hx => (fderivWithin_of_isOpen hs hx).symm
-#align cont_diff_on.fderiv_of_open ContDiffOn.fderiv_of_open
+#align cont_diff_on.fderiv_of_open ContDiffOn.fderiv_of_isOpen
 -/
 
 #print ContDiffOn.continuousOn_fderivWithin /-
@@ -1473,11 +1473,11 @@ theorem ContDiffOn.continuousOn_fderivWithin (h : ContDiffOn 𝕜 n f s) (hs : U
 #align cont_diff_on.continuous_on_fderiv_within ContDiffOn.continuousOn_fderivWithin
 -/
 
-#print ContDiffOn.continuousOn_fderiv_of_open /-
-theorem ContDiffOn.continuousOn_fderiv_of_open (h : ContDiffOn 𝕜 n f s) (hs : IsOpen s)
+#print ContDiffOn.continuousOn_fderiv_of_isOpen /-
+theorem ContDiffOn.continuousOn_fderiv_of_isOpen (h : ContDiffOn 𝕜 n f s) (hs : IsOpen s)
     (hn : 1 ≤ n) : ContinuousOn (fun x => fderiv 𝕜 f x) s :=
-  ((contDiffOn_succ_iff_fderiv_of_open hs).1 (h.of_le hn)).2.ContinuousOn
-#align cont_diff_on.continuous_on_fderiv_of_open ContDiffOn.continuousOn_fderiv_of_open
+  ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 (h.of_le hn)).2.ContinuousOn
+#align cont_diff_on.continuous_on_fderiv_of_open ContDiffOn.continuousOn_fderiv_of_isOpen
 -/
 
 /-! ### Functions with a Taylor series on the whole space -/

Mathbin/Analysis/Calculus/Deriv/Basic.lean

@@ -659,10 +659,10 @@ theorem derivWithin_inter (ht : t ∈ 𝓝 x) : derivWithin f (s ∩ t) x = deri
 #align deriv_within_inter derivWithin_inter
 -/
 
-#print derivWithin_of_open /-
-theorem derivWithin_of_open (hs : IsOpen s) (hx : x ∈ s) : derivWithin f s x = deriv f x := by
+#print derivWithin_of_isOpen /-
+theorem derivWithin_of_isOpen (hs : IsOpen s) (hx : x ∈ s) : derivWithin f s x = deriv f x := by
   unfold derivWithin; rw [fderivWithin_of_isOpen hs hx]; rfl
-#align deriv_within_of_open derivWithin_of_open
+#align deriv_within_of_open derivWithin_of_isOpen
 -/
 
 #print deriv_mem_iff /-

Mathbin/Analysis/Convex/Gauge.lean

@@ -420,25 +420,26 @@ theorem interior_subset_gauge_lt_one (s : Set E) : interior s ⊆ {x | gauge s x
 #align interior_subset_gauge_lt_one interior_subset_gauge_lt_one
 -/
 
-#print gauge_lt_one_eq_self_of_open /-
-theorem gauge_lt_one_eq_self_of_open (hs₁ : Convex ℝ s) (hs₀ : (0 : E) ∈ s) (hs₂ : IsOpen s) :
+#print gauge_lt_one_eq_self_of_isOpen /-
+theorem gauge_lt_one_eq_self_of_isOpen (hs₁ : Convex ℝ s) (hs₀ : (0 : E) ∈ s) (hs₂ : IsOpen s) :
     {x | gauge s x < 1} = s :=
   by
   refine' (gauge_lt_one_subset_self hs₁ ‹_› <| absorbent_nhds_zero <| hs₂.mem_nhds hs₀).antisymm _
   convert interior_subset_gauge_lt_one s
   exact hs₂.interior_eq.symm
-#align gauge_lt_one_eq_self_of_open gauge_lt_one_eq_self_of_open
+#align gauge_lt_one_eq_self_of_open gauge_lt_one_eq_self_of_isOpen
 -/
 
-theorem gauge_lt_one_of_mem_of_open (hs₁ : Convex ℝ s) (hs₀ : (0 : E) ∈ s) (hs₂ : IsOpen s) {x : E}
-    (hx : x ∈ s) : gauge s x < 1 := by rwa [← gauge_lt_one_eq_self_of_open hs₁ hs₀ hs₂] at hx 
-#align gauge_lt_one_of_mem_of_open gauge_lt_one_of_mem_of_openₓ
+theorem gauge_lt_one_of_mem_of_isOpen (hs₁ : Convex ℝ s) (hs₀ : (0 : E) ∈ s) (hs₂ : IsOpen s)
+    {x : E} (hx : x ∈ s) : gauge s x < 1 := by
+  rwa [← gauge_lt_one_eq_self_of_isOpen hs₁ hs₀ hs₂] at hx 
+#align gauge_lt_one_of_mem_of_open gauge_lt_one_of_mem_of_isOpenₓ
 
 theorem gauge_lt_of_mem_smul (x : E) (ε : ℝ) (hε : 0 < ε) (hs₀ : (0 : E) ∈ s) (hs₁ : Convex ℝ s)
     (hs₂ : IsOpen s) (hx : x ∈ ε • s) : gauge s x < ε :=
   by
   have : ε⁻¹ • x ∈ s := by rwa [← mem_smul_set_iff_inv_smul_mem₀ hε.ne']
-  have h_gauge_lt := gauge_lt_one_of_mem_of_open hs₁ hs₀ hs₂ this
+  have h_gauge_lt := gauge_lt_one_of_mem_of_isOpen hs₁ hs₀ hs₂ this
   rwa [gauge_smul_of_nonneg (inv_nonneg.2 hε.le), smul_eq_mul, inv_mul_lt_iff hε, mul_one] at
     h_gauge_lt 
   infer_instance
@@ -481,18 +482,18 @@ def gaugeSeminorm (hs₀ : Balanced 𝕜 s) (hs₁ : Convex ℝ s) (hs₂ : Abso
 variable {hs₀ : Balanced 𝕜 s} {hs₁ : Convex ℝ s} {hs₂ : Absorbent ℝ s} [TopologicalSpace E]
   [ContinuousSMul ℝ E]
 
-#print gaugeSeminorm_lt_one_of_open /-
-theorem gaugeSeminorm_lt_one_of_open (hs : IsOpen s) {x : E} (hx : x ∈ s) :
+#print gaugeSeminorm_lt_one_of_isOpen /-
+theorem gaugeSeminorm_lt_one_of_isOpen (hs : IsOpen s) {x : E} (hx : x ∈ s) :
     gaugeSeminorm hs₀ hs₁ hs₂ x < 1 :=
-  gauge_lt_one_of_mem_of_open hs₁ hs₂.zero_mem hs hx
-#align gauge_seminorm_lt_one_of_open gaugeSeminorm_lt_one_of_open
+  gauge_lt_one_of_mem_of_isOpen hs₁ hs₂.zero_mem hs hx
+#align gauge_seminorm_lt_one_of_open gaugeSeminorm_lt_one_of_isOpen
 -/
 
 #print gaugeSeminorm_ball_one /-
 theorem gaugeSeminorm_ball_one (hs : IsOpen s) : (gaugeSeminorm hs₀ hs₁ hs₂).ball 0 1 = s :=
   by
   rw [Seminorm.ball_zero_eq]
-  exact gauge_lt_one_eq_self_of_open hs₁ hs₂.zero_mem hs
+  exact gauge_lt_one_eq_self_of_isOpen hs₁ hs₂.zero_mem hs
 #align gauge_seminorm_ball_one gaugeSeminorm_ball_one
 -/
 

Mathbin/Analysis/Convex/Strict.lean

@@ -132,16 +132,17 @@ protected theorem StrictConvex.convex (hs : StrictConvex 𝕜 s) : Convex 𝕜 s
 #align strict_convex.convex StrictConvex.convex
 -/
 
-#print Convex.strictConvex_of_open /-
+#print Convex.strictConvex_of_isOpen /-
 /-- An open convex set is strictly convex. -/
-protected theorem Convex.strictConvex_of_open (h : IsOpen s) (hs : Convex 𝕜 s) : StrictConvex 𝕜 s :=
-  fun x hx y hy _ a b ha hb hab => h.interior_eq.symm ▸ hs hx hy ha.le hb.le hab
-#align convex.strict_convex_of_open Convex.strictConvex_of_open
+protected theorem Convex.strictConvex_of_isOpen (h : IsOpen s) (hs : Convex 𝕜 s) :
+    StrictConvex 𝕜 s := fun x hx y hy _ a b ha hb hab =>
+  h.interior_eq.symm ▸ hs hx hy ha.le hb.le hab
+#align convex.strict_convex_of_open Convex.strictConvex_of_isOpen
 -/
 
 #print IsOpen.strictConvex_iff /-
 theorem IsOpen.strictConvex_iff (h : IsOpen s) : StrictConvex 𝕜 s ↔ Convex 𝕜 s :=
-  ⟨StrictConvex.convex, Convex.strictConvex_of_open h⟩
+  ⟨StrictConvex.convex, Convex.strictConvex_of_isOpen h⟩
 #align is_open.strict_convex_iff IsOpen.strictConvex_iff
 -/
 

Mathbin/Analysis/Convolution.lean

@@ -1722,7 +1722,7 @@ theorem contDiffOn_convolution_right_with_param_aux {G : Type uP} {E' : Type uP}
       ∀ q₀ : P × G,
         q₀.1 ∈ s → HasFDerivAt (fun q : P × G => (f ⋆[L, μ] g q.1) q.2) (f' q₀.1 q₀.2) q₀ :=
       hasFDerivAt_convolution_right_with_param L hs hk hgs hf hg.one_of_succ
-    rw [contDiffOn_succ_iff_fderiv_of_open (hs.prod (@isOpen_univ G _))] at hg ⊢
+    rw [contDiffOn_succ_iff_fderiv_of_isOpen (hs.prod (@isOpen_univ G _))] at hg ⊢
     constructor
     · rintro ⟨p, x⟩ ⟨hp, hx⟩
       exact (A (p, x) hp).DifferentiableAt.DifferentiableWithinAt

Mathbin/Analysis/LocallyConvex/AbsConvex.lean

@@ -180,7 +180,7 @@ theorem gaugeSeminormFamily_ball (s : AbsConvexOpenSets 𝕜 E) :
   dsimp only [gaugeSeminormFamily]
   rw [Seminorm.ball_zero_eq]
   simp_rw [gaugeSeminorm_to_fun]
-  exact gauge_lt_one_eq_self_of_open s.coe_convex s.coe_zero_mem s.coe_is_open
+  exact gauge_lt_one_eq_self_of_isOpen s.coe_convex s.coe_zero_mem s.coe_is_open
 #align gauge_seminorm_family_ball gaugeSeminormFamily_ball
 -/
 

Mathbin/Analysis/NormedSpace/Basic.lean

@@ -215,7 +215,7 @@ instance {E : Type _} [NormedAddCommGroup E] [NormedSpace ℚ E] (e : E) :
   by
   rcases eq_or_ne e 0 with (rfl | he)
   · rw [AddSubgroup.zmultiples_zero_eq_bot]; infer_instance
-  · rw [discreteTopology_iff_open_singleton_zero, isOpen_induced_iff]
+  · rw [discreteTopology_iff_isOpen_singleton_zero, isOpen_induced_iff]
     refine' ⟨Metric.ball 0 ‖e‖, Metric.isOpen_ball, _⟩
     ext ⟨x, hx⟩
     obtain ⟨k, rfl⟩ := add_subgroup.mem_zmultiples_iff.mp hx

Mathbin/Analysis/NormedSpace/HahnBanach/Separation.lean

@@ -60,7 +60,7 @@ theorem separate_convex_open_set [TopologicalSpace E] [AddCommGroup E] [Topologi
     rw [← Submodule.coe_mk x₀ (Submodule.mem_span_singleton_self _), hφ₁,
       LinearPMap.mkSpanSingleton'_apply_self]
   have hφ₄ : ∀ x ∈ s, φ x < 1 := fun x hx =>
-    (hφ₂ x).trans_lt (gauge_lt_one_of_mem_of_open hs₁ hs₀ hs₂ hx)
+    (hφ₂ x).trans_lt (gauge_lt_one_of_mem_of_isOpen hs₁ hs₀ hs₂ hx)
   · refine' ⟨⟨φ, _⟩, hφ₃, hφ₄⟩
     refine'
       φ.continuous_of_nonzero_on_open _ (hs₂.vadd (-x₀)) (nonempty.vadd_set ⟨0, hs₀⟩)