chore: tidy various files (#7081)

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -47,11 +47,11 @@ This notation works for functions `f : p → M`, where `p : Prop`, so the follow
 
 ## Implementation notes
 
-`Finsum` and `Finprod` is "yet another way of doing finite sums and products in Lean". However
+`finsum` and `finprod` is "yet another way of doing finite sums and products in Lean". However
 experiments in the wild (e.g. with matroids) indicate that it is a helpful approach in settings
 where the user is not interested in computability and wants to do reasoning without running into
 typeclass diamonds caused by the constructive finiteness used in definitions such as `Finset` and
-`Fintype`. By sticking solely to `Set.finite` we avoid these problems. We are aware that there are
+`Fintype`. By sticking solely to `Set.Finite` we avoid these problems. We are aware that there are
 other solutions but for beginner mathematicians this approach is easier in practice.
 
 Another application is the construction of a partition of unity from a collection of “bump”
@@ -171,29 +171,29 @@ notation3"∏ᶠ "(...)", "r:67:(scoped f => finprod f) => r
 --          (finprod (α := $t) fun $h => $p))))
 
 @[to_additive]
-theorem finprod_eq_prod_pLift_of_mulSupport_toFinset_subset {f : α → M}
+theorem finprod_eq_prod_plift_of_mulSupport_toFinset_subset {f : α → M}
     (hf : (mulSupport (f ∘ PLift.down)).Finite) {s : Finset (PLift α)} (hs : hf.toFinset ⊆ s) :
     ∏ᶠ i, f i = ∏ i in s, f i.down := by
   rw [finprod, dif_pos]
   refine' Finset.prod_subset hs fun x _ hxf => _
   rwa [hf.mem_toFinset, nmem_mulSupport] at hxf
-#align finprod_eq_prod_plift_of_mul_support_to_finset_subset finprod_eq_prod_pLift_of_mulSupport_toFinset_subset
-#align finsum_eq_sum_plift_of_support_to_finset_subset finsum_eq_sum_pLift_of_support_toFinset_subset
+#align finprod_eq_prod_plift_of_mul_support_to_finset_subset finprod_eq_prod_plift_of_mulSupport_toFinset_subset
+#align finsum_eq_sum_plift_of_support_to_finset_subset finsum_eq_sum_plift_of_support_toFinset_subset
 
 @[to_additive]
-theorem finprod_eq_prod_pLift_of_mulSupport_subset {f : α → M} {s : Finset (PLift α)}
+theorem finprod_eq_prod_plift_of_mulSupport_subset {f : α → M} {s : Finset (PLift α)}
     (hs : mulSupport (f ∘ PLift.down) ⊆ s) : ∏ᶠ i, f i = ∏ i in s, f i.down :=
-  finprod_eq_prod_pLift_of_mulSupport_toFinset_subset (s.finite_toSet.subset hs) fun x hx => by
+  finprod_eq_prod_plift_of_mulSupport_toFinset_subset (s.finite_toSet.subset hs) fun x hx => by
     rw [Finite.mem_toFinset] at hx
     exact hs hx
-#align finprod_eq_prod_plift_of_mul_support_subset finprod_eq_prod_pLift_of_mulSupport_subset
-#align finsum_eq_sum_plift_of_support_subset finsum_eq_sum_pLift_of_support_subset
+#align finprod_eq_prod_plift_of_mul_support_subset finprod_eq_prod_plift_of_mulSupport_subset
+#align finsum_eq_sum_plift_of_support_subset finsum_eq_sum_plift_of_support_subset
 
 @[to_additive (attr := simp)]
 theorem finprod_one : (∏ᶠ _ : α, (1 : M)) = 1 := by
   have : (mulSupport fun x : PLift α => (fun _ => 1 : α → M) x.down) ⊆ (∅ : Finset (PLift α)) :=
     fun x h => by simp at h
-  rw [finprod_eq_prod_pLift_of_mulSupport_subset this, Finset.prod_empty]
+  rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_empty]
 #align finprod_one finprod_one
 #align finsum_zero finsum_zero
 
@@ -212,13 +212,13 @@ theorem finprod_false (f : False → M) : ∏ᶠ i, f i = 1 :=
 #align finsum_false finsum_false
 
 @[to_additive]
-theorem finprod_eq_single (f : α → M) (a : α) (ha : ∀ (x) (_ : x ≠ a), f x = 1) :
+theorem finprod_eq_single (f : α → M) (a : α) (ha : ∀ x, x ≠ a → f x = 1) :
     ∏ᶠ x, f x = f a := by
   have : mulSupport (f ∘ PLift.down) ⊆ ({PLift.up a} : Finset (PLift α)) := by
     intro x
     contrapose
     simpa [PLift.eq_up_iff_down_eq] using ha x.down
-  rw [finprod_eq_prod_pLift_of_mulSupport_subset this, Finset.prod_singleton]
+  rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_singleton]
 #align finprod_eq_single finprod_eq_single
 #align finsum_eq_single finsum_eq_single
 
@@ -291,26 +291,26 @@ theorem one_le_finprod' {M : Type*} [OrderedCommMonoid M] {f : α → M} (hf : 
 #align finsum_nonneg finsum_nonneg
 
 @[to_additive]
-theorem MonoidHom.map_finprod_pLift (f : M →* N) (g : α → M)
+theorem MonoidHom.map_finprod_plift (f : M →* N) (g : α → M)
     (h : (mulSupport <| g ∘ PLift.down).Finite) : f (∏ᶠ x, g x) = ∏ᶠ x, f (g x) := by
-  rw [finprod_eq_prod_pLift_of_mulSupport_subset h.coe_toFinset.ge,
-    finprod_eq_prod_pLift_of_mulSupport_subset, f.map_prod]
+  rw [finprod_eq_prod_plift_of_mulSupport_subset h.coe_toFinset.ge,
+    finprod_eq_prod_plift_of_mulSupport_subset, f.map_prod]
   rw [h.coe_toFinset]
   exact mulSupport_comp_subset f.map_one (g ∘ PLift.down)
-#align monoid_hom.map_finprod_plift MonoidHom.map_finprod_pLift
-#align add_monoid_hom.map_finsum_plift AddMonoidHom.map_finsum_pLift
+#align monoid_hom.map_finprod_plift MonoidHom.map_finprod_plift
+#align add_monoid_hom.map_finsum_plift AddMonoidHom.map_finsum_plift
 
 @[to_additive]
 theorem MonoidHom.map_finprod_Prop {p : Prop} (f : M →* N) (g : p → M) :
     f (∏ᶠ x, g x) = ∏ᶠ x, f (g x) :=
-  f.map_finprod_pLift g (Set.toFinite _)
+  f.map_finprod_plift g (Set.toFinite _)
 #align monoid_hom.map_finprod_Prop MonoidHom.map_finprod_Prop
 #align add_monoid_hom.map_finsum_Prop AddMonoidHom.map_finsum_Prop
 
 @[to_additive]
 theorem MonoidHom.map_finprod_of_preimage_one (f : M →* N) (hf : ∀ x, f x = 1 → x = 1) (g : α → M) :
     f (∏ᶠ i, g i) = ∏ᶠ i, f (g i) := by
-  by_cases hg : (mulSupport <| g ∘ PLift.down).Finite; · exact f.map_finprod_pLift g hg
+  by_cases hg : (mulSupport <| g ∘ PLift.down).Finite; · exact f.map_finprod_plift g hg
   rw [finprod, dif_neg, f.map_one, finprod, dif_neg]
   exacts [Infinite.mono (fun x hx => mt (hf (g x.down)) hx) hg, hg]
 #align monoid_hom.map_finprod_of_preimage_one MonoidHom.map_finprod_of_preimage_one
@@ -333,16 +333,18 @@ theorem MulEquiv.map_finprod (g : M ≃* N) (f : α → M) : g (∏ᶠ i, f i) =
 infinite. For a more usual version assuming `(support f).Finite` instead, see `finsum_smul'`. -/
 theorem finsum_smul {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
     (f : ι → R) (x : M) : (∑ᶠ i, f i) • x = ∑ᶠ i, f i • x := by
-  rcases eq_or_ne x 0 with (rfl | hx); · simp
-  exact ((smulAddHom R M).flip x).map_finsum_of_injective (smul_left_injective R hx) _
+  rcases eq_or_ne x 0 with (rfl | hx)
+  · simp
+  · exact ((smulAddHom R M).flip x).map_finsum_of_injective (smul_left_injective R hx) _
 #align finsum_smul finsum_smul
 
 /-- The `NoZeroSMulDivisors` makes sure that the result holds even when the support of `f` is
 infinite. For a more usual version assuming `(support f).Finite` instead, see `smul_finsum'`. -/
 theorem smul_finsum {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
     (c : R) (f : ι → M) : (c • ∑ᶠ i, f i) = ∑ᶠ i, c • f i := by
-  rcases eq_or_ne c 0 with (rfl | hc); · simp
-  exact (smulAddHom R M c).map_finsum_of_injective (smul_right_injective M hc) _
+  rcases eq_or_ne c 0 with (rfl | hc)
+  · simp
+  · exact (smulAddHom R M c).map_finsum_of_injective (smul_right_injective M hc) _
 #align smul_finsum smul_finsum
 
 @[to_additive]
@@ -388,7 +390,7 @@ theorem finprod_eq_prod_of_mulSupport_subset (f : α → M) {s : Finset α} (h :
   have : mulSupport (f ∘ PLift.down) ⊆ s.map Equiv.plift.symm.toEmbedding := by
     rw [A, Finset.coe_map]
     exact image_subset _ h
-  rw [finprod_eq_prod_pLift_of_mulSupport_subset this]
+  rw [finprod_eq_prod_plift_of_mulSupport_subset this]
   simp only [Finset.prod_map, Equiv.coe_toEmbedding]
   congr
 #align finprod_eq_prod_of_mul_support_subset finprod_eq_prod_of_mulSupport_subset
@@ -619,7 +621,7 @@ theorem finprod_mul_distrib (hf : (mulSupport f).Finite) (hg : (mulSupport g).Fi
       mem_union, mem_mulSupport]
     intro x
     contrapose!
-    rintro ⟨hf,hg⟩
+    rintro ⟨hf, hg⟩
     simp [hf, hg]
 #align finprod_mul_distrib finprod_mul_distrib
 #align finsum_add_distrib finsum_add_distrib
@@ -689,7 +691,7 @@ theorem finprod_mem_mul_distrib (hs : s.Finite) :
 @[to_additive]
 theorem MonoidHom.map_finprod {f : α → M} (g : M →* N) (hf : (mulSupport f).Finite) :
     g (∏ᶠ i, f i) = ∏ᶠ i, g (f i) :=
-  g.map_finprod_pLift f <| hf.preimage <| Equiv.plift.injective.injOn _
+  g.map_finprod_plift f <| hf.preimage <| Equiv.plift.injective.injOn _
 #align monoid_hom.map_finprod MonoidHom.map_finprod
 #align add_monoid_hom.map_finsum AddMonoidHom.map_finsum
 

Mathlib/Analysis/Convex/Combination.lean

@@ -192,7 +192,7 @@ theorem Convex.finsum_mem {ι : Sort*} {w : ι → R} {z : ι → E} {s : Set E}
     exact zero_ne_one h₁
   have hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ hfin_w.toFinset :=
     (support_smul_subset_left _ _).trans hfin_w.coe_toFinset.ge
-  rw [finsum_eq_sum_pLift_of_support_subset hsub]
+  rw [finsum_eq_sum_plift_of_support_subset hsub]
   refine' hs.sum_mem (fun _ _ => h₀ _) _ fun i hi => hz _ _
   · rwa [finsum, dif_pos hfin_w] at h₁
   · rwa [hfin_w.mem_toFinset] at hi

Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

@@ -504,15 +504,12 @@ theorem cos_eq_sqrt_one_sub_sin_sq {x : ℝ} (hl : -(π / 2) ≤ x) (hu : x ≤
 #align real.cos_eq_sqrt_one_sub_sin_sq Real.cos_eq_sqrt_one_sub_sin_sq
 
 theorem sin_eq_zero_iff_of_lt_of_lt {x : ℝ} (hx₁ : -π < x) (hx₂ : x < π) : sin x = 0 ↔ x = 0 :=
-  ⟨fun h => le_antisymm (le_of_not_gt fun h0 => lt_irrefl (0 : ℝ) <|
-    calc
-      0 < sin x := sin_pos_of_pos_of_lt_pi h0 hx₂
-      _ = 0 := h)
-    (le_of_not_gt fun h0 => lt_irrefl (0 : ℝ) <|
-      calc
-        0 = sin x := h.symm
-        _ < 0 := sin_neg_of_neg_of_neg_pi_lt h0 hx₁),
-    fun h => by simp [h]⟩
+  ⟨fun h => by
+    contrapose! h
+    cases h.lt_or_lt with
+    | inl h0 => exact (sin_neg_of_neg_of_neg_pi_lt h0 hx₁).ne
+    | inr h0 => exact (sin_pos_of_pos_of_lt_pi h0 hx₂).ne',
+  fun h => by simp [h]⟩
 #align real.sin_eq_zero_iff_of_lt_of_lt Real.sin_eq_zero_iff_of_lt_of_lt
 
 theorem sin_eq_zero_iff {x : ℝ} : sin x = 0 ↔ ∃ n : ℤ, (n : ℝ) * π = x :=
@@ -736,24 +733,23 @@ theorem cos_pi_over_two_pow : ∀ n : ℕ, cos (π / 2 ^ (n + 1)) = sqrtTwoAddSe
   | 0 => by simp
   | n + 1 => by
     have : (2 : ℝ) ≠ 0 := two_ne_zero
-    symm; rw [div_eq_iff_mul_eq this]; symm
-    rw [sqrtTwoAddSeries, sqrt_eq_iff_sq_eq, mul_pow, cos_sq, ← mul_div_assoc, Nat.add_succ,
-      pow_succ, mul_div_mul_left _ _ this, cos_pi_over_two_pow _, add_mul]
-    congr; · norm_num
-    rw [mul_comm, sq, mul_assoc, ← mul_div_assoc, mul_div_cancel_left, ← mul_div_assoc,
-        mul_div_cancel_left] <;>
-      try exact this
-    apply add_nonneg; norm_num; apply sqrtTwoAddSeries_zero_nonneg; norm_num
-    apply le_of_lt; apply cos_pos_of_mem_Ioo ⟨_, _⟩
+    rw [eq_div_iff_mul_eq this, eq_comm, sqrtTwoAddSeries, sqrt_eq_iff_sq_eq, mul_pow, cos_sq,
+      ← mul_div_assoc, pow_succ, mul_div_mul_left _ _ this, cos_pi_over_two_pow _, add_mul]
+    · congr
+      · norm_num
+      · rw [mul_comm, sq, mul_assoc, ← mul_div_assoc, mul_div_cancel_left _ this, ← mul_div_assoc,
+          mul_div_cancel_left _ this]
+    · exact add_nonneg two_pos.le (sqrtTwoAddSeries_zero_nonneg _)
+    refine le_of_lt <| mul_pos (cos_pos_of_mem_Ioo ⟨?_, ?_⟩) two_pos
     · trans (0 : ℝ)
-      rw [neg_lt_zero]
-      apply pi_div_two_pos
-      apply div_pos pi_pos
-      apply pow_pos
-      norm_num
-    apply div_lt_div' (le_refl π) _ pi_pos _
+      · rw [neg_lt_zero]
+        exact pi_div_two_pos
+      · exact div_pos pi_pos <| pow_pos two_pos _
+    apply div_lt_div' (le_refl π) _ pi_pos two_pos
     refine' lt_of_le_of_lt (le_of_eq (pow_one _).symm) _
-    apply pow_lt_pow; norm_num; apply Nat.succ_lt_succ; apply Nat.succ_pos; all_goals norm_num
+    apply pow_lt_pow
+    · norm_num
+    · exact Nat.succ_lt_succ n.succ_pos
 #align real.cos_pi_over_two_pow Real.cos_pi_over_two_pow
 
 theorem sin_sq_pi_over_two_pow (n : ℕ) :
@@ -764,90 +760,92 @@ theorem sin_sq_pi_over_two_pow (n : ℕ) :
 theorem sin_sq_pi_over_two_pow_succ (n : ℕ) :
     sin (π / 2 ^ (n + 2)) ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4 := by
   rw [sin_sq_pi_over_two_pow, sqrtTwoAddSeries, div_pow, sq_sqrt, add_div, ← sub_sub]
-  congr; norm_num; norm_num; apply add_nonneg; norm_num; apply sqrtTwoAddSeries_zero_nonneg
+  congr
+  · norm_num
+  · norm_num
+  · exact add_nonneg two_pos.le (sqrtTwoAddSeries_zero_nonneg _)
 #align real.sin_sq_pi_over_two_pow_succ Real.sin_sq_pi_over_two_pow_succ
 
 @[simp]
 theorem sin_pi_over_two_pow_succ (n : ℕ) :
     sin (π / 2 ^ (n + 2)) = sqrt (2 - sqrtTwoAddSeries 0 n) / 2 := by
-  symm; rw [div_eq_iff_mul_eq]; symm
-  rw [sqrt_eq_iff_sq_eq, mul_pow, sin_sq_pi_over_two_pow_succ, sub_mul]
+  rw [eq_div_iff_mul_eq two_ne_zero, eq_comm, sqrt_eq_iff_sq_eq, mul_pow,
+    sin_sq_pi_over_two_pow_succ, sub_mul]
   · congr <;> norm_num
   · rw [sub_nonneg]
-    apply le_of_lt
-    apply sqrtTwoAddSeries_lt_two
-  apply le_of_lt; apply mul_pos; apply sin_pos_of_pos_of_lt_pi
-  · apply div_pos pi_pos
-    apply pow_pos
-    norm_num
-  refine' lt_of_lt_of_le _ (le_of_eq (div_one _)); rw [div_lt_div_left]
+    exact (sqrtTwoAddSeries_lt_two _).le
+  refine le_of_lt <| mul_pos (sin_pos_of_pos_of_lt_pi ?_ ?_) two_pos
+  · exact div_pos pi_pos <| pow_pos two_pos _
+  refine' lt_of_lt_of_le _ (le_of_eq (div_one _))
+  rw [div_lt_div_left pi_pos (pow_pos two_pos _) one_pos]
   refine' lt_of_le_of_lt (le_of_eq (pow_zero 2).symm) _
-  apply pow_lt_pow; norm_num; apply Nat.succ_pos; apply pi_pos
-  apply pow_pos; all_goals norm_num
+  apply pow_lt_pow
+  · norm_num
+  · apply Nat.succ_pos
 #align real.sin_pi_over_two_pow_succ Real.sin_pi_over_two_pow_succ
 
 @[simp]
 theorem cos_pi_div_four : cos (π / 4) = sqrt 2 / 2 := by
   trans cos (π / 2 ^ 2)
-  congr
-  norm_num
-  simp
+  · congr
+    norm_num
+  · simp
 #align real.cos_pi_div_four Real.cos_pi_div_four
 
 @[simp]
 theorem sin_pi_div_four : sin (π / 4) = sqrt 2 / 2 := by
   trans sin (π / 2 ^ 2)
-  congr
-  norm_num
-  simp
+  · congr
+    norm_num
+  · simp
 #align real.sin_pi_div_four Real.sin_pi_div_four
 
 @[simp]
 theorem cos_pi_div_eight : cos (π / 8) = sqrt (2 + sqrt 2) / 2 := by
   trans cos (π / 2 ^ 3)
-  congr
-  norm_num
-  simp
+  · congr
+    norm_num
+  · simp
 #align real.cos_pi_div_eight Real.cos_pi_div_eight
 
 @[simp]
 theorem sin_pi_div_eight : sin (π / 8) = sqrt (2 - sqrt 2) / 2 := by
   trans sin (π / 2 ^ 3)
-  congr
-  norm_num
-  simp
+  · congr
+    norm_num
+  · simp
 #align real.sin_pi_div_eight Real.sin_pi_div_eight
 
 @[simp]
 theorem cos_pi_div_sixteen : cos (π / 16) = sqrt (2 + sqrt (2 + sqrt 2)) / 2 := by
   trans cos (π / 2 ^ 4)
-  congr
-  norm_num
-  simp
+  · congr
+    norm_num
+  · simp
 #align real.cos_pi_div_sixteen Real.cos_pi_div_sixteen
 
 @[simp]
 theorem sin_pi_div_sixteen : sin (π / 16) = sqrt (2 - sqrt (2 + sqrt 2)) / 2 := by
   trans sin (π / 2 ^ 4)
-  congr
-  norm_num
-  simp
+  · congr
+    norm_num
+  · simp
 #align real.sin_pi_div_sixteen Real.sin_pi_div_sixteen
 
 @[simp]
 theorem cos_pi_div_thirty_two : cos (π / 32) = sqrt (2 + sqrt (2 + sqrt (2 + sqrt 2))) / 2 := by
   trans cos (π / 2 ^ 5)
-  congr
-  norm_num
-  simp
+  · congr
+    norm_num
+  · simp
 #align real.cos_pi_div_thirty_two Real.cos_pi_div_thirty_two
 
 @[simp]
 theorem sin_pi_div_thirty_two : sin (π / 32) = sqrt (2 - sqrt (2 + sqrt (2 + sqrt 2))) / 2 := by
   trans sin (π / 2 ^ 5)
-  congr
-  norm_num
-  simp
+  · congr
+    norm_num
+  · simp
 #align real.sin_pi_div_thirty_two Real.sin_pi_div_thirty_two
 
 -- This section is also a convenient location for other explicit values of `sin` and `cos`.
@@ -862,7 +860,7 @@ theorem cos_pi_div_three : cos (π / 3) = 1 / 2 := by
   cases' mul_eq_zero.mp h₁ with h h
   · linarith [pow_eq_zero h]
   · have : cos π < cos (π / 3) := by
-      refine' cos_lt_cos_of_nonneg_of_le_pi _ rfl.ge _ <;> linarith [pi_pos]
+      refine' cos_lt_cos_of_nonneg_of_le_pi _ le_rfl _ <;> linarith [pi_pos]
     linarith [cos_pi]
 #align real.cos_pi_div_three Real.cos_pi_div_three
 
@@ -882,8 +880,7 @@ theorem sq_cos_pi_div_six : cos (π / 6) ^ 2 = 3 / 4 := by
 @[simp]
 theorem cos_pi_div_six : cos (π / 6) = sqrt 3 / 2 := by
   suffices sqrt 3 = cos (π / 6) * 2 by
-    field_simp [(by norm_num : 0 ≠ 2)]
-    exact this.symm
+    field_simp [(by norm_num : 0 ≠ 2), ← this]
   rw [sqrt_eq_iff_sq_eq]
   · have h1 := (mul_right_inj' (by norm_num : (4 : ℝ) ≠ 0)).mpr sq_cos_pi_div_six
     rw [← sub_eq_zero] at h1 ⊢

Mathlib/Geometry/Manifold/BumpFunction.lean

@@ -204,7 +204,7 @@ theorem nhdsWithin_range_basis :
     (𝓝[range I] extChartAt I c c).HasBasis (fun _ : SmoothBumpFunction I c => True) fun f =>
       closedBall (extChartAt I c c) f.rOut ∩ range I := by
   refine' ((nhdsWithin_hasBasis nhds_basis_closedBall _).restrict_subset
-    (extChartAt_target_mem_nhdsWithin _ _)).to_has_basis' _ _
+    (extChartAt_target_mem_nhdsWithin _ _)).to_hasBasis' _ _
   · rintro R ⟨hR0, hsub⟩
     exact ⟨⟨⟨R / 2, R, half_pos hR0, half_lt_self hR0⟩, hsub⟩, trivial, Subset.rfl⟩
   · exact fun f _ => inter_mem (mem_nhdsWithin_of_mem_nhds <| closedBall_mem_nhds _ f.rOut_pos)
@@ -293,7 +293,7 @@ theorem nhds_basis_tsupport :
       (extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I) := by
     rw [← map_extChartAt_symm_nhdsWithin_range I c]
     exact nhdsWithin_range_basis.map _
-  refine' this.to_has_basis' (fun f _ => ⟨f, trivial, f.tsupport_subset_symm_image_closedBall⟩)
+  refine' this.to_hasBasis' (fun f _ => ⟨f, trivial, f.tsupport_subset_symm_image_closedBall⟩)
     fun f _ => f.tsupport_mem_nhds
 #align smooth_bump_function.nhds_basis_tsupport SmoothBumpFunction.nhds_basis_tsupport
 
@@ -305,7 +305,7 @@ neighborhood of `c` and each neighborhood of `c` includes `support f` for some
 `f : SmoothBumpFunction I c` such that `tsupport f ⊆ s`. -/
 theorem nhds_basis_support {s : Set M} (hs : s ∈ 𝓝 c) :
     (𝓝 c).HasBasis (fun f : SmoothBumpFunction I c => tsupport f ⊆ s) fun f => support f :=
-  ((nhds_basis_tsupport I c).restrict_subset hs).to_has_basis'
+  ((nhds_basis_tsupport I c).restrict_subset hs).to_hasBasis'
     (fun f hf => ⟨f, hf.2, subset_closure⟩) fun f _ => f.support_mem_nhds
 #align smooth_bump_function.nhds_basis_support SmoothBumpFunction.nhds_basis_support