chore: tidy various files (#3530)

Author: Ruben-VandeVelde

Mathlib/Algebra/Algebra/Bilinear.lean

@@ -22,9 +22,7 @@ in order to avoid importing `LinearAlgebra.BilinearMap` and
 -/
 
 
-open TensorProduct
-
-open Module
+open TensorProduct Module
 
 namespace LinearMap
 
@@ -63,14 +61,14 @@ def mulLeftRight (ab : A × A) : A →ₗ[R] A :=
 #align linear_map.mul_left_right LinearMap.mulLeftRight
 
 @[simp]
-theorem mulLeft_toAddMonoid_hom (a : A) : (mulLeft R a : A →+ A) = AddMonoidHom.mulLeft a :=
+theorem mulLeft_toAddMonoidHom (a : A) : (mulLeft R a : A →+ A) = AddMonoidHom.mulLeft a :=
   rfl
-#align linear_map.mul_left_to_add_monoid_hom LinearMap.mulLeft_toAddMonoid_hom
+#align linear_map.mul_left_to_add_monoid_hom LinearMap.mulLeft_toAddMonoidHom
 
 @[simp]
-theorem mulRight_toAddMonoid_hom (a : A) : (mulRight R a : A →+ A) = AddMonoidHom.mulRight a :=
+theorem mulRight_toAddMonoidHom (a : A) : (mulRight R a : A →+ A) = AddMonoidHom.mulRight a :=
   rfl
-#align linear_map.mul_right_to_add_monoid_hom LinearMap.mulRight_toAddMonoid_hom
+#align linear_map.mul_right_to_add_monoid_hom LinearMap.mulRight_toAddMonoidHom
 
 variable {R}
 
@@ -165,8 +163,7 @@ the algebra.
 
 A weaker version of this for non-unital algebras exists as `NonUnitalAlgHom.mul`. -/
 def Algebra.lmul : A →ₐ[R] End R A :=
-  { LinearMap.mul R
-      A with
+  { LinearMap.mul R A with
     map_one' := by
       ext a
       exact one_mul a

Mathlib/Algebra/Algebra/Operations.lean

@@ -175,7 +175,7 @@ theorem mul_le : M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P :=
 theorem mul_toAddSubmonoid (M N : Submodule R A) :
     (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid := by
   dsimp [HMul.hMul, Mul.mul]  --porting note: added `hMul`
-  simp_rw [← LinearMap.mulLeft_toAddMonoid_hom R, LinearMap.mulLeft, ← map_toAddSubmonoid _ N,
+  simp_rw [← LinearMap.mulLeft_toAddMonoidHom R, LinearMap.mulLeft, ← map_toAddSubmonoid _ N,
     map₂]
   rw [supᵢ_toAddSubmonoid]
   rfl

Mathlib/Algebra/Algebra/Pi.lean

@@ -15,7 +15,7 @@ import Mathlib.Algebra.Algebra.Equiv
 
 The R-algebra structure on `∀ i : I, A i` when each `A i` is an R-algebra.
 
-## Main defintions
+## Main definitions
 
 * `Pi.algebra`
 * `Pi.evalAlgHom`
@@ -27,25 +27,22 @@ universe u v w
 
 namespace Pi
 
+-- The indexing type
 variable {I : Type u}
 
--- The indexing type
+-- The scalar type
 variable {R : Type _}
 
--- The scalar type
+-- The family of types already equipped with instances
 variable {f : I → Type v}
 
--- The family of types already equipped with instances
 variable (x y : ∀ i, f i) (i : I)
 
 variable (I f)
 
 instance algebra {r : CommSemiring R} [s : ∀ i, Semiring (f i)] [∀ i, Algebra R (f i)] :
     Algebra R (∀ i : I, f i) :=
-  {
-    (Pi.ringHom fun i => algebraMap R (f i) :
-      R →+* ∀ i : I,
-          f i) with
+  { (Pi.ringHom fun i => algebraMap R (f i) : R →+* ∀ i : I, f i) with
     commutes' := fun a f => by ext; simp [Algebra.commutes]
     smul_def' := fun a f => by ext; simp [Algebra.smul_def] }
 #align pi.algebra Pi.algebra
@@ -77,7 +74,7 @@ def evalAlgHom {_ : CommSemiring R} [∀ i, Semiring (f i)] [∀ i, Algebra R (f
 
 variable (A B : Type _) [CommSemiring R] [Semiring B] [Algebra R B]
 
-/-- `Function.const` as an `AlgHom`. The name matches `Pi.constRingHhom`, `Pi.constMonoidHom`,
+/-- `Function.const` as an `AlgHom`. The name matches `Pi.constRingHom`, `Pi.constMonoidHom`,
 etc. -/
 @[simps]
 def constAlgHom : B →ₐ[R] A → B :=
@@ -133,16 +130,14 @@ namespace AlgEquiv
 /-- A family of algebra equivalences `∀ i, (A₁ i ≃ₐ A₂ i)` generates a
 multiplicative equivalence between `∀ i, A₁ i` and `∀ i, A₂ i`.
 
-This is the `AlgEquiv` version of `Equiv.Pi_congrRight`, and the dependent version of
+This is the `AlgEquiv` version of `Equiv.piCongrRight`, and the dependent version of
 `AlgEquiv.arrowCongr`.
 -/
 @[simps apply]
 def piCongrRight {R ι : Type _} {A₁ A₂ : ι → Type _} [CommSemiring R] [∀ i, Semiring (A₁ i)]
     [∀ i, Semiring (A₂ i)] [∀ i, Algebra R (A₁ i)] [∀ i, Algebra R (A₂ i)]
     (e : ∀ i, A₁ i ≃ₐ[R] A₂ i) : (∀ i, A₁ i) ≃ₐ[R] ∀ i, A₂ i :=
-  {
-    @RingEquiv.piCongrRight ι A₁ A₂ _ _ fun i =>
-      (e i).toRingEquiv with
+  { @RingEquiv.piCongrRight ι A₁ A₂ _ _ fun i => (e i).toRingEquiv with
     toFun := fun x j => e j (x j)
     invFun := fun x j => (e j).symm (x j)
     commutes' := fun r => by

Mathlib/Algebra/Algebra/Tower.lean

@@ -131,8 +131,8 @@ theorem coe_toAlgHom : ↑(toAlgHom R S A) = algebraMap S A :=
 #align is_scalar_tower.coe_to_alg_hom IsScalarTower.coe_toAlgHom
 
 @[simp]
-theorem coe_to_alg_hom' : (toAlgHom R S A : S → A) = algebraMap S A := rfl
-#align is_scalar_tower.coe_to_alg_hom' IsScalarTower.coe_to_alg_hom'
+theorem coe_toAlgHom' : (toAlgHom R S A : S → A) = algebraMap S A := rfl
+#align is_scalar_tower.coe_to_alg_hom' IsScalarTower.coe_toAlgHom'
 
 variable {R S A B}
 
@@ -198,8 +198,8 @@ theorem coe_restrictScalars (f : A →ₐ[S] B) : (f.restrictScalars R : A →+*
 #align alg_hom.coe_restrict_scalars AlgHom.coe_restrictScalars
 
 @[simp]
-theorem coe_restrict_scalars' (f : A →ₐ[S] B) : (restrictScalars R f : A → B) = f := rfl
-#align alg_hom.coe_restrict_scalars' AlgHom.coe_restrict_scalars'
+theorem coe_restrictScalars' (f : A →ₐ[S] B) : (restrictScalars R f : A → B) = f := rfl
+#align alg_hom.coe_restrict_scalars' AlgHom.coe_restrictScalars'
 
 theorem restrictScalars_injective :
     Function.Injective (restrictScalars R : (A →ₐ[S] B) → A →ₐ[R] B) := fun _ _ h =>
@@ -226,8 +226,8 @@ theorem coe_restrictScalars (f : A ≃ₐ[S] B) : (f.restrictScalars R : A ≃+*
 #align alg_equiv.coe_restrict_scalars AlgEquiv.coe_restrictScalars
 
 @[simp]
-theorem coe_restrict_scalars' (f : A ≃ₐ[S] B) : (restrictScalars R f : A → B) = f := rfl
-#align alg_equiv.coe_restrict_scalars' AlgEquiv.coe_restrict_scalars'
+theorem coe_restrictScalars' (f : A ≃ₐ[S] B) : (restrictScalars R f : A → B) = f := rfl
+#align alg_equiv.coe_restrict_scalars' AlgEquiv.coe_restrictScalars'
 
 theorem restrictScalars_injective :
     Function.Injective (restrictScalars R : (A ≃ₐ[S] B) → A ≃ₐ[R] B) := fun _ _ h =>

Mathlib/Algebra/Module/Submodule/Basic.lean

@@ -409,9 +409,9 @@ variable {α β : Type _}
 instance [VAdd M α] : VAdd p α :=
   p.toAddSubmonoid.vadd
 
-instance vAddCommClass [VAdd M β] [VAdd α β] [VAddCommClass M α β] : VAddCommClass p α β :=
+instance vaddCommClass [VAdd M β] [VAdd α β] [VAddCommClass M α β] : VAddCommClass p α β :=
   ⟨fun a => (vadd_comm (a : M) : _)⟩
-#align submodule.vadd_comm_class Submodule.vAddCommClass
+#align submodule.vadd_comm_class Submodule.vaddCommClass
 
 instance [VAdd M α] [FaithfulVAdd M α] : FaithfulVAdd p α :=
   ⟨fun h => Subtype.ext <| eq_of_vadd_eq_vadd h⟩

Mathlib/AlgebraicTopology/SimplexCategory.lean

@@ -94,14 +94,14 @@ protected def rec {F : ∀ _ : SimplexCategory, Sort _} (h : ∀ n : ℕ, F [n])
 #align simplex_category.rec SimplexCategory.rec
 
 -- porting note: removed @[nolint has_nonempty_instance]
-/-- Morphisms in the simplex_category. -/
+/-- Morphisms in the `SimplexCategory`. -/
 protected def Hom (a b : SimplexCategory) :=
   Fin (a.len + 1) →o Fin (b.len + 1)
 #align simplex_category.hom SimplexCategory.Hom
 
 namespace Hom
 
-/-- Make a moprhism in `SimplexCategory` from a monotone map of fin's. -/
+/-- Make a moprhism in `SimplexCategory` from a monotone map of `Fin`'s. -/
 def mk {a b : SimplexCategory} (f : Fin (a.len + 1) →o Fin (b.len + 1)) : SimplexCategory.Hom a b :=
   f
 #align simplex_category.hom.mk SimplexCategory.Hom.mk
@@ -640,7 +640,7 @@ theorem eq_σ_comp_of_not_injective {n : ℕ} {Δ' : SimplexCategory} (θ : mk (
   -- and then, `θ x = θ (x+1)`
   have hθ₂ : ∃ x y : Fin (n + 2), (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y := by
     rcases hθ with ⟨x, y, ⟨h₁, h₂⟩⟩
-    by_cases x < y
+    by_cases h : x < y
     · exact ⟨x, y, ⟨h₁, h⟩⟩
     · refine' ⟨y, x, ⟨h₁.symm, _⟩⟩
       cases' lt_or_eq_of_le (not_lt.mp h) with h' h'

Mathlib/Analysis/BoxIntegral/Box/Basic.lean

@@ -202,30 +202,30 @@ protected def Icc : Box ι ↪o Set (ι → ℝ) :=
   OrderEmbedding.ofMapLEIff (fun I : Box ι ↦ Icc I.lower I.upper) fun I J ↦ (le_TFAE I J).out 2 0
 #align box_integral.box.Icc BoxIntegral.Box.Icc
 
-theorem icc_def : Box.Icc I = Icc I.lower I.upper := rfl
-#align box_integral.box.Icc_def BoxIntegral.Box.icc_def
+theorem Icc_def : Box.Icc I = Icc I.lower I.upper := rfl
+#align box_integral.box.Icc_def BoxIntegral.Box.Icc_def
 
 @[simp]
-theorem upper_mem_icc (I : Box ι) : I.upper ∈ Box.Icc I :=
+theorem upper_mem_Icc (I : Box ι) : I.upper ∈ Box.Icc I :=
   right_mem_Icc.2 I.lower_le_upper
-#align box_integral.box.upper_mem_Icc BoxIntegral.Box.upper_mem_icc
+#align box_integral.box.upper_mem_Icc BoxIntegral.Box.upper_mem_Icc
 
 @[simp]
-theorem lower_mem_icc (I : Box ι) : I.lower ∈ Box.Icc I :=
+theorem lower_mem_Icc (I : Box ι) : I.lower ∈ Box.Icc I :=
   left_mem_Icc.2 I.lower_le_upper
-#align box_integral.box.lower_mem_Icc BoxIntegral.Box.lower_mem_icc
+#align box_integral.box.lower_mem_Icc BoxIntegral.Box.lower_mem_Icc
 
-protected theorem isCompact_icc (I : Box ι) : IsCompact (Box.Icc I) :=
+protected theorem isCompact_Icc (I : Box ι) : IsCompact (Box.Icc I) :=
   isCompact_Icc
-#align box_integral.box.is_compact_Icc BoxIntegral.Box.isCompact_icc
+#align box_integral.box.is_compact_Icc BoxIntegral.Box.isCompact_Icc
 
-theorem icc_eq_pi : Box.Icc I = pi univ fun i ↦ Icc (I.lower i) (I.upper i) :=
+theorem Icc_eq_pi : Box.Icc I = pi univ fun i ↦ Icc (I.lower i) (I.upper i) :=
   (pi_univ_Icc _ _).symm
-#align box_integral.box.Icc_eq_pi BoxIntegral.Box.icc_eq_pi
+#align box_integral.box.Icc_eq_pi BoxIntegral.Box.Icc_eq_pi
 
-theorem le_iff_icc : I ≤ J ↔ Box.Icc I ⊆ Box.Icc J :=
+theorem le_iff_Icc : I ≤ J ↔ Box.Icc I ⊆ Box.Icc J :=
   (le_TFAE I J).out 0 2
-#align box_integral.box.le_iff_Icc BoxIntegral.Box.le_iff_icc
+#align box_integral.box.le_iff_Icc BoxIntegral.Box.le_iff_Icc
 
 theorem antitone_lower : Antitone fun I : Box ι ↦ I.lower :=
   fun _ _ H ↦ (le_iff_bounds.1 H).1
@@ -235,9 +235,9 @@ theorem monotone_upper : Monotone fun I : Box ι ↦ I.upper :=
   fun _ _ H ↦ (le_iff_bounds.1 H).2
 #align box_integral.box.monotone_upper BoxIntegral.Box.monotone_upper
 
-theorem coe_subset_icc : ↑I ⊆ Box.Icc I :=
+theorem coe_subset_Icc : ↑I ⊆ Box.Icc I :=
   fun _ hx ↦ ⟨fun i ↦ (hx i).1.le, fun i ↦ (hx i).2⟩
-#align box_integral.box.coe_subset_Icc BoxIntegral.Box.coe_subset_icc
+#align box_integral.box.coe_subset_Icc BoxIntegral.Box.coe_subset_Icc
 
 /-!
 ### Supremum of two boxes
@@ -290,10 +290,10 @@ theorem isSome_iff : ∀ {I : WithBot (Box ι)}, I.isSome ↔ (I : Set (ι → 
     simp [I.nonempty_coe]
 #align box_integral.box.is_some_iff BoxIntegral.Box.isSome_iff
 
-theorem bUnion_coe_eq_coe (I : WithBot (Box ι)) :
+theorem bunionᵢ_coe_eq_coe (I : WithBot (Box ι)) :
     (⋃ (J : Box ι) (_hJ : ↑J = I), (J : Set (ι → ℝ))) = I := by
   induction I using WithBot.recBotCoe <;> simp [WithBot.coe_eq_coe]
-#align box_integral.box.bUnion_coe_eq_coe BoxIntegral.Box.bUnion_coe_eq_coe
+#align box_integral.box.bUnion_coe_eq_coe BoxIntegral.Box.bunionᵢ_coe_eq_coe
 
 @[simp, norm_cast]
 theorem withBotCoe_subset_iff {I J : WithBot (Box ι)} : (I : Set (ι → ℝ)) ⊆ J ↔ I ≤ J := by
@@ -345,10 +345,10 @@ instance WithBot.inf : Inf (WithBot (Box ι)) :=
 
 @[simp]
 theorem coe_inf (I J : WithBot (Box ι)) : (↑(I ⊓ J) : Set (ι → ℝ)) = (I : Set _) ∩ J := by
-  induction I using WithBot.recBotCoe;
+  induction I using WithBot.recBotCoe
   · change ∅ = _
     simp
-  induction J using WithBot.recBotCoe;
+  induction J using WithBot.recBotCoe
   · change ∅ = _
     simp
   change ((mk' _ _ : WithBot (Box ι)) : Set (ι → ℝ)) = _
@@ -427,12 +427,12 @@ theorem mapsTo_insertNth_face {n} (I : Box (Fin (n + 1))) {i : Fin (n + 1)} {x :
   exact ⟨hx, hy⟩
 #align box_integral.box.maps_to_insert_nth_face BoxIntegral.Box.mapsTo_insertNth_face
 
-theorem continuousOn_face_icc {X} [TopologicalSpace X] {n} {f : (Fin (n + 1) → ℝ) → X}
+theorem continuousOn_face_Icc {X} [TopologicalSpace X] {n} {f : (Fin (n + 1) → ℝ) → X}
     {I : Box (Fin (n + 1))} (h : ContinuousOn f (Box.Icc I)) {i : Fin (n + 1)} {x : ℝ}
     (hx : x ∈ Icc (I.lower i) (I.upper i)) :
     ContinuousOn (f ∘ i.insertNth x) (Box.Icc (I.face i)) :=
   h.comp (continuousOn_const.fin_insertNth i continuousOn_id) (I.mapsTo_insertNth_face_Icc hx)
-#align box_integral.box.continuous_on_face_Icc BoxIntegral.Box.continuousOn_face_icc
+#align box_integral.box.continuous_on_face_Icc BoxIntegral.Box.continuousOn_face_Icc
 
 /-!
 ### Covering of the interior of a box by a monotone sequence of smaller boxes
@@ -446,15 +446,15 @@ protected def Ioo : Box ι →o Set (ι → ℝ) where
     pi_mono fun i _ ↦ Ioo_subset_Ioo ((le_iff_bounds.1 h).1 i) ((le_iff_bounds.1 h).2 i)
 #align box_integral.box.Ioo BoxIntegral.Box.Ioo
 
-theorem ioo_subset_coe (I : Box ι) : Box.Ioo I ⊆ I :=
+theorem Ioo_subset_coe (I : Box ι) : Box.Ioo I ⊆ I :=
   fun _ hx i ↦ Ioo_subset_Ioc_self (hx i trivial)
-#align box_integral.box.Ioo_subset_coe BoxIntegral.Box.ioo_subset_coe
+#align box_integral.box.Ioo_subset_coe BoxIntegral.Box.Ioo_subset_coe
 
-protected theorem ioo_subset_icc (I : Box ι) : Box.Ioo I ⊆ Box.Icc I :=
-  I.ioo_subset_coe.trans coe_subset_icc
-#align box_integral.box.Ioo_subset_Icc BoxIntegral.Box.ioo_subset_icc
+protected theorem Ioo_subset_Icc (I : Box ι) : Box.Ioo I ⊆ Box.Icc I :=
+  I.Ioo_subset_coe.trans coe_subset_Icc
+#align box_integral.box.Ioo_subset_Icc BoxIntegral.Box.Ioo_subset_Icc
 
-theorem unionᵢ_ioo_of_tendsto [Finite ι] {I : Box ι} {J : ℕ → Box ι} (hJ : Monotone J)
+theorem unionᵢ_Ioo_of_tendsto [Finite ι] {I : Box ι} {J : ℕ → Box ι} (hJ : Monotone J)
     (hl : Tendsto (lower ∘ J) atTop (𝓝 I.lower)) (hu : Tendsto (upper ∘ J) atTop (𝓝 I.upper)) :
     (⋃ n, Box.Ioo (J n)) = Box.Ioo I :=
   have hl' : ∀ i, Antitone fun n ↦ (J n).lower i :=
@@ -469,7 +469,7 @@ theorem unionᵢ_ioo_of_tendsto [Finite ι] {I : Box ι} {J : ℕ → Box ι} (h
         unionᵢ_Ioo_of_mono_of_isGLB_of_isLUB (hl' i) (hu' i)
           (isGLB_of_tendsto_atTop (hl' i) (tendsto_pi_nhds.1 hl _))
           (isLUB_of_tendsto_atTop (hu' i) (tendsto_pi_nhds.1 hu _))
-#align box_integral.box.Union_Ioo_of_tendsto BoxIntegral.Box.unionᵢ_ioo_of_tendsto
+#align box_integral.box.Union_Ioo_of_tendsto BoxIntegral.Box.unionᵢ_Ioo_of_tendsto
 
 theorem exists_seq_mono_tendsto (I : Box ι) :
     ∃ J : ℕ →o Box ι,
@@ -527,7 +527,7 @@ theorem dist_le_distortion_mul (I : Box ι) (i : ι) :
     neg_sub] using I.nndist_le_distortion_mul i
 #align box_integral.box.dist_le_distortion_mul BoxIntegral.Box.dist_le_distortion_mul
 
-theorem diam_icc_le_of_distortion_le (I : Box ι) (i : ι) {c : ℝ≥0} (h : I.distortion ≤ c) :
+theorem diam_Icc_le_of_distortion_le (I : Box ι) (i : ι) {c : ℝ≥0} (h : I.distortion ≤ c) :
     diam (Box.Icc I) ≤ c * (I.upper i - I.lower i) :=
   have : (0 : ℝ) ≤ c * (I.upper i - I.lower i) :=
     mul_nonneg c.coe_nonneg (sub_nonneg.2 <| I.lower_le_upper _)
@@ -537,7 +537,7 @@ theorem diam_icc_le_of_distortion_le (I : Box ι) (i : ι) {c : ℝ≥0} (h : I.
       _ ≤ I.distortion * (I.upper i - I.lower i) := (I.dist_le_distortion_mul i)
       _ ≤ c * (I.upper i - I.lower i) :=
         mul_le_mul_of_nonneg_right h (sub_nonneg.2 (I.lower_le_upper i))
-#align box_integral.box.diam_Icc_le_of_distortion_le BoxIntegral.Box.diam_icc_le_of_distortion_le
+#align box_integral.box.diam_Icc_le_of_distortion_le BoxIntegral.Box.diam_Icc_le_of_distortion_le
 
 end Distortion
 

Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean

@@ -32,9 +32,7 @@ rectangular box, induction
 -/
 
 
-open Set Finset Function Filter Metric
-
-open Classical Topology Filter ENNReal
+open Set Finset Function Filter Metric Classical Topology Filter ENNReal
 
 noncomputable section
 
@@ -157,8 +155,8 @@ theorem subbox_induction_on' {p : Box ι → Prop} (I : Box ι)
   have hzJ : ∀ m, z ∈ Box.Icc (J m) :=
     mem_interᵢ.1 (csupᵢ_mem_Inter_Icc_of_antitone_Icc
       ((@Box.Icc ι).monotone.comp_antitone hJmono) fun m ↦ (J m).lower_le_upper)
-  have hJl_mem : ∀ m, (J m).lower ∈ Box.Icc I := fun m ↦ le_iff_icc.1 (hJle m) (J m).lower_mem_icc
-  have hJu_mem : ∀ m, (J m).upper ∈ Box.Icc I := fun m ↦ le_iff_icc.1 (hJle m) (J m).upper_mem_icc
+  have hJl_mem : ∀ m, (J m).lower ∈ Box.Icc I := fun m ↦ le_iff_Icc.1 (hJle m) (J m).lower_mem_Icc
+  have hJu_mem : ∀ m, (J m).upper ∈ Box.Icc I := fun m ↦ le_iff_Icc.1 (hJle m) (J m).upper_mem_Icc
   have hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝 z) :=
     tendsto_atTop_csupᵢ (antitone_lower.comp hJmono) ⟨I.upper, fun x ⟨m, hm⟩ ↦ hm ▸ (hJl_mem m).2⟩
   have hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝 z) := by
@@ -167,11 +165,11 @@ theorem subbox_induction_on' {p : Box ι → Prop} (I : Box ι)
     simpa [hJsub] using
       tendsto_const_nhds.div_atTop (tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)
   replace hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z)
-  exact
-    tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hJlz (eventually_of_forall hJl_mem)
+  · exact
+      tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hJlz (eventually_of_forall hJl_mem)
   replace hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝[Icc I.lower I.upper] z)
-  exact
-    tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hJuz (eventually_of_forall hJu_mem)
+  · exact
+      tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hJuz (eventually_of_forall hJu_mem)
   rcases H_nhds z (h0 ▸ hzJ 0) with ⟨U, hUz, hU⟩
   rcases(tendsto_lift'.1 (hJlz.Icc hJuz) U hUz).exists with ⟨m, hUm⟩
   exact hJp m (hU (J m) (hJle m) m (hzJ m) hUm (hJsub m))

Mathlib/Analysis/NormedSpace/ContinuousLinearMap.lean

@@ -61,7 +61,7 @@ def LinearMap.mkContinuous (C : ℝ) (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) : E
 
 /-- Reinterpret a linear map `𝕜 →ₗ[𝕜] E` as a continuous linear map. This construction
 is generalized to the case of any finite dimensional domain
-in `linear_map.to_continuous_linear_map`. -/
+in `LinearMap.toContinuousLinearMap`. -/
 def LinearMap.toContinuousLinearMap₁ (f : 𝕜 →ₗ[𝕜] E) : 𝕜 →L[𝕜] E :=
   f.mkContinuous ‖f 1‖ fun x =>
     le_of_eq <| by
@@ -71,7 +71,7 @@ def LinearMap.toContinuousLinearMap₁ (f : 𝕜 →ₗ[𝕜] E) : 𝕜 →L[
 
 /-- Construct a continuous linear map from a linear map and the existence of a bound on this linear
 map. If you have an explicit bound, use `LinearMap.mkContinuous` instead, as a norm estimate will
-follow automatically in `linear_map.mk_continuous_norm_le`. -/
+follow automatically in `LinearMap.mkContinuous_norm_le`. -/
 def LinearMap.mkContinuousOfExistsBound (h : ∃ C, ∀ x, ‖f x‖ ≤ C * ‖x‖) : E →SL[σ] F :=
   ⟨f,
     let ⟨C, hC⟩ := h