chore: uncdot up to and including CategoryTheory (#12521)

A portion of #12422 containing all the changes in `Mathlib/[A-C]` up to and including `CategoryTheory`.

Mathlib/Algebra/DirectLimit.lean

@@ -768,11 +768,11 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
       ⟨k, s ∪ t, this,
         isSupported_add (isSupported_upwards hxs <| Set.subset_union_left s t)
           (isSupported_upwards hyt <| Set.subset_union_right s t), fun [_] => _⟩
-    · -- Porting note: was `(restriction _).map_add`
-      classical rw [RingHom.map_add, (FreeCommRing.lift _).map_add, ←
-        of.zero_exact_aux2 G f' hxs hi this hik (Set.subset_union_left s t), ←
-        of.zero_exact_aux2 G f' hyt hj this hjk (Set.subset_union_right s t), ihs,
-        (f' i k hik).map_zero, iht, (f' j k hjk).map_zero, zero_add]
+    -- Porting note: was `(restriction _).map_add`
+    classical rw [RingHom.map_add, (FreeCommRing.lift _).map_add, ←
+      of.zero_exact_aux2 G f' hxs hi this hik (Set.subset_union_left s t), ←
+      of.zero_exact_aux2 G f' hyt hj this hjk (Set.subset_union_right s t), ihs,
+      (f' i k hik).map_zero, iht, (f' j k hjk).map_zero, zero_add]
   · rintro x y ⟨j, t, hj, hyt, iht⟩
     rw [smul_eq_mul]
     rcases exists_finset_support x with ⟨s, hxs⟩

Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean

@@ -182,10 +182,10 @@ lemma mappingConeCompTriangleh_distinguished :
   refine' ⟨_, _, (CochainComplex.mappingConeCompTriangle f g).mor₁, ⟨_⟩⟩
   refine' Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (isoOfHomotopyEquiv
     (CochainComplex.mappingConeCompHomotopyEquiv f g)) (by aesop_cat) (by simp) _
-  · dsimp [CochainComplex.mappingConeCompTriangleh]
-    rw [CategoryTheory.Functor.map_id, comp_id, ← Functor.map_comp_assoc]
-    congr 2
-    exact (CochainComplex.mappingConeCompHomotopyEquiv_comm₂ f g).symm
+  dsimp [CochainComplex.mappingConeCompTriangleh]
+  rw [CategoryTheory.Functor.map_id, comp_id, ← Functor.map_comp_assoc]
+  congr 2
+  exact (CochainComplex.mappingConeCompHomotopyEquiv_comm₂ f g).symm
 
 noncomputable instance : IsTriangulated (HomotopyCategory C (ComplexShape.up ℤ)) :=
   IsTriangulated.mk' (by

Mathlib/Algebra/Homology/TotalComplex.lean

@@ -223,12 +223,12 @@ lemma D₂_D₁ (i₁₂ i₁₂' i₁₂'' : I₁₂) :
             ComplexShape.ε₂_ε₁ c₁₂ h₃ h₄, neg_mul, Units.neg_smul]
         · simp only [K.d₂_eq_zero c₁₂ _ _ _ h₄, zero_comp, comp_zero, smul_zero, neg_zero]
       · rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, zero_comp, neg_zero]
-        · by_cases h₄ : c₂.Rel i₂ (c₂.next i₂)
-          · rw [totalAux.d₂_eq K c₁₂ i₁ h₄ i₁₂']; swap
-            · rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← c₁₂.next_eq' h₁, h]
-            simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₁]
-            rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, comp_zero, smul_zero]
-          · rw [K.d₂_eq_zero c₁₂ _ _ _ h₄, zero_comp]
+        by_cases h₄ : c₂.Rel i₂ (c₂.next i₂)
+        · rw [totalAux.d₂_eq K c₁₂ i₁ h₄ i₁₂']; swap
+          · rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← c₁₂.next_eq' h₁, h]
+          simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₁]
+          rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, comp_zero, smul_zero]
+        · rw [K.d₂_eq_zero c₁₂ _ _ _ h₄, zero_comp]
     · rw [K.D₁_shape c₁₂ _ _ h₂, K.D₂_shape c₁₂ _ _ h₂, comp_zero, comp_zero, neg_zero]
   · rw [K.D₁_shape c₁₂ _ _ h₁, K.D₂_shape c₁₂ _ _ h₁, zero_comp, zero_comp, neg_zero]
 

Mathlib/Algebra/Module/DedekindDomain.lean

@@ -53,10 +53,10 @@ theorem isInternal_prime_power_torsion_of_is_torsion_by_ideal {I : Ideal R} (hI
   · intro p hp q hq pq; dsimp
     rw [irreducible_pow_sup]
     · suffices (normalizedFactors _).count p = 0 by rw [this, zero_min, pow_zero, Ideal.one_eq_top]
-      · rw [Multiset.count_eq_zero,
-          normalizedFactors_of_irreducible_pow (prime_of_mem q hq).irreducible,
-          Multiset.mem_replicate]
-        exact fun H => pq <| H.2.trans <| normalize_eq q
+      rw [Multiset.count_eq_zero,
+        normalizedFactors_of_irreducible_pow (prime_of_mem q hq).irreducible,
+        Multiset.mem_replicate]
+      exact fun H => pq <| H.2.trans <| normalize_eq q
     · rw [← Ideal.zero_eq_bot]; apply pow_ne_zero; exact (prime_of_mem q hq).ne_zero
     · exact (prime_of_mem p hp).irreducible
 #align submodule.is_internal_prime_power_torsion_of_is_torsion_by_ideal Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal

Mathlib/Algebra/Order/CompleteField.lean

@@ -151,9 +151,9 @@ theorem cutMap_add (a b : α) : cutMap β (a + b) = cutMap β a + cutMap β b :=
   · rw [mem_setOf_eq, ← sub_lt_iff_lt_add] at hq
     obtain ⟨q₁, hq₁q, hq₁ab⟩ := exists_rat_btwn hq
     refine ⟨q₁, by rwa [coe_mem_cutMap_iff], q - q₁, ?_, add_sub_cancel _ _⟩
-    · norm_cast
-      rw [coe_mem_cutMap_iff]
-      exact mod_cast sub_lt_comm.mp hq₁q
+    norm_cast
+    rw [coe_mem_cutMap_iff]
+    exact mod_cast sub_lt_comm.mp hq₁q
   · rintro _ ⟨_, ⟨qa, ha, rfl⟩, _, ⟨qb, hb, rfl⟩, rfl⟩
     -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction.
     refine' ⟨qa + qb, _, by beta_reduce; norm_cast⟩

Mathlib/Algebra/Polynomial/Degree/Definitions.lean

@@ -970,10 +970,10 @@ theorem coeff_mul_degree_add_degree (p q : R[X]) :
               rw [coeff_eq_zero_of_degree_lt
                   (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),
                 mul_zero]
-            · by_contra! H'
-              exact
-                ne_of_lt (Nat.lt_of_lt_of_le (Nat.add_lt_add_right H j) (Nat.add_le_add_left H' _))
-                  h₁
+            by_contra! H'
+            exact
+              ne_of_lt (Nat.lt_of_lt_of_le (Nat.add_lt_add_right H j) (Nat.add_le_add_left H' _))
+                h₁
       · intro H
         exfalso
         apply H

Mathlib/Algebra/Polynomial/PartialFractions.lean

@@ -109,28 +109,28 @@ theorem div_eq_quo_add_sum_rem_div (f : R[X]) {ι : Type*} {g : ι → R[X]} {s
       (IsCoprime.prod_right fun i hi =>
         hcop (Finset.mem_coe.2 (b.mem_insert_self a))
           (Finset.mem_coe.2 (Finset.mem_insert_of_mem hi)) (by rintro rfl; exact hab hi))
-  · obtain ⟨q, r, hrdeg, IH⟩ :=
-      Hind _ (fun i hi => hg i (Finset.mem_insert_of_mem hi))
-        (Set.Pairwise.mono (Finset.coe_subset.2 fun i hi => Finset.mem_insert_of_mem hi) hcop)
-    refine ⟨q₀ + q, fun i => if i = a then r₁ else r i, ?_, ?_⟩
-    · intro i
-      dsimp only
-      split_ifs with h1
-      · cases h1
-        intro
-        exact hdeg₁
-      · intro hi
-        exact hrdeg i (Finset.mem_of_mem_insert_of_ne hi h1)
-    norm_cast at hf IH ⊢
-    rw [Finset.prod_insert hab, hf, IH, Finset.sum_insert hab, if_pos rfl]
-    trans (↑(q₀ + q : R[X]) : K) + (↑r₁ / ↑(g a) + ∑ i : ι in b, (r i : K) / (g i : K))
-    · push_cast
-      ring
-    congr 2
-    refine' Finset.sum_congr rfl fun x hxb => _
-    rw [if_neg]
-    rintro rfl
-    exact hab hxb
+  obtain ⟨q, r, hrdeg, IH⟩ :=
+    Hind _ (fun i hi => hg i (Finset.mem_insert_of_mem hi))
+      (Set.Pairwise.mono (Finset.coe_subset.2 fun i hi => Finset.mem_insert_of_mem hi) hcop)
+  refine ⟨q₀ + q, fun i => if i = a then r₁ else r i, ?_, ?_⟩
+  · intro i
+    dsimp only
+    split_ifs with h1
+    · cases h1
+      intro
+      exact hdeg₁
+    · intro hi
+      exact hrdeg i (Finset.mem_of_mem_insert_of_ne hi h1)
+  norm_cast at hf IH ⊢
+  rw [Finset.prod_insert hab, hf, IH, Finset.sum_insert hab, if_pos rfl]
+  trans (↑(q₀ + q : R[X]) : K) + (↑r₁ / ↑(g a) + ∑ i : ι in b, (r i : K) / (g i : K))
+  · push_cast
+    ring
+  congr 2
+  refine' Finset.sum_congr rfl fun x hxb => _
+  rw [if_neg]
+  rintro rfl
+  exact hab hxb
 #align div_eq_quo_add_sum_rem_div div_eq_quo_add_sum_rem_div
 
 end NDenominators

Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean

@@ -832,7 +832,7 @@ lemma map_slope {F : Type u} [Field F] (W : Affine F) {K : Type v} [Field K] (φ
   by_cases hx : x₁ = x₂
   · by_cases hy : y₁ = W.negY x₂ y₂
     · rw [slope_of_Yeq hx hy, slope_of_Yeq <| congr_arg _ hx, map_zero]
-      · rw [hy, map_negY]
+      rw [hy, map_negY]
     · rw [slope_of_Yne hx hy, slope_of_Yne <| congr_arg _ hx]
       · simp only [negY]
         map_simp
@@ -925,7 +925,7 @@ def map : W⟮F⟯ →+ W⟮K⟯ where
     · by_cases hy : y₁ = (W.baseChange F).toAffine.negY x₂ y₂
       · simp only [some_add_some_of_Yeq hx hy, mapFun]
         rw [some_add_some_of_Yeq <| congr_arg _ hx]
-        · rw [hy, baseChange_negY]
+        rw [hy, baseChange_negY]
       · simp only [some_add_some_of_Yne hx hy, mapFun]
         rw [some_add_some_of_Yne <| congr_arg _ hx]
         · simp only [some.injEq, ← baseChange_addX, ← baseChange_addY, ← baseChange_slope]

Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

@@ -551,7 +551,7 @@ theorem AffineTargetMorphismProperty.diagonalOfTargetAffineLocally
   specialize H g₁
   rw [← affine_cancel_left_isIso hP.1 (pullbackDiagonalMapIso f _ f₁ f₂).hom]
   convert H
-  · apply pullback.hom_ext <;>
+  apply pullback.hom_ext <;>
     simp only [Category.assoc, pullback.lift_fst, pullback.lift_snd, pullback.lift_fst_assoc,
       pullback.lift_snd_assoc, Category.comp_id, pullbackDiagonalMapIso_hom_fst,
       pullbackDiagonalMapIso_hom_snd]

Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

@@ -261,12 +261,12 @@ instance quasiSeparatedSpace_of_isAffine (X : Scheme) [IsAffine X] :
   rw [e, e', Set.iUnion₂_inter]
   simp_rw [Set.inter_iUnion₂]
   apply hs.isCompact_biUnion
-  · intro i _
-    apply hs'.isCompact_biUnion
-    intro i' _
-    change IsCompact (X.basicOpen i ⊓ X.basicOpen i').1
-    rw [← Scheme.basicOpen_mul]
-    exact ((topIsAffineOpen _).basicOpenIsAffine _).isCompact
+  intro i _
+  apply hs'.isCompact_biUnion
+  intro i' _
+  change IsCompact (X.basicOpen i ⊓ X.basicOpen i').1
+  rw [← Scheme.basicOpen_mul]
+  exact ((topIsAffineOpen _).basicOpenIsAffine _).isCompact
 #align algebraic_geometry.quasi_separated_space_of_is_affine AlgebraicGeometry.quasiSeparatedSpace_of_isAffine
 
 theorem IsAffineOpen.isQuasiSeparated {X : Scheme} {U : Opens X.carrier} (hU : IsAffineOpen U) :

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -230,7 +230,7 @@ lemma carrier_eq_span :
     erw [mem_carrier_iff, HomogeneousLocalization.val_mk'']
     erw [show (Localization.mk s ⟨f ^ l, ⟨_, rfl⟩⟩ : Localization.Away f) =
       (Localization.mk 1 ⟨f^l, ⟨_, rfl⟩⟩ : Localization.Away f) * Localization.mk s 1 by
-      · rw [Localization.mk_mul, mul_one, one_mul]]
+      rw [Localization.mk_mul, mul_one, one_mul]]
     exact Ideal.mul_mem_left _ _ <| Ideal.subset_span ⟨s, hs, rfl⟩
 
 theorem disjoint :
@@ -644,9 +644,9 @@ lemma toSpec_fromSpec {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (x :
   · erw [ToSpec.mem_carrier_iff]
     obtain ⟨k, (k_spec : f^k = z.den)⟩ := z.den_mem
     rw [show z.val = (Localization.mk z.num ⟨f^k, ⟨k, rfl⟩⟩ : Away f) by
-        · rw [z.eq_num_div_den]; congr; exact k_spec.symm,
+        rw [z.eq_num_div_den]; congr; exact k_spec.symm,
       show (mk z.num ⟨f^k, ⟨k, rfl⟩⟩ : Away f) = mk z.num 1 * (mk 1 ⟨f^k, ⟨k, rfl⟩⟩ : Away f) by
-        · rw [mk_mul, mul_one, one_mul]]
+        rw [mk_mul, mul_one, one_mul]]
     refine Ideal.mul_mem_right _ _ <| Ideal.subset_span ⟨z.num, ?_, rfl⟩
 
     intro j
@@ -703,7 +703,7 @@ lemma fromSpec_toSpec {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (x :
     dsimp only [GradedAlgebra.proj_apply]
     rw [show (mk (decompose 𝒜 z i ^ m) ⟨f^i, ⟨i, rfl⟩⟩ : Away f) =
       (decompose 𝒜 z i ^ m : A) • (mk 1 ⟨f^i, ⟨i, rfl⟩⟩ : Away f) by
-      · rw [smul_mk, smul_eq_mul, mul_one], Algebra.smul_def]
+      rw [smul_mk, smul_eq_mul, mul_one], Algebra.smul_def]
     exact Ideal.mul_mem_right _ _ <|
       Ideal.subset_span ⟨_, ⟨Ideal.pow_mem_of_mem _ (x.1.asHomogeneousIdeal.2 i hz) _ hm, rfl⟩⟩
 

Mathlib/AlgebraicTopology/SplitSimplicialObject.lean

@@ -135,9 +135,9 @@ theorem eqId_iff_eq : A.EqId ↔ A.1 = Δ := by
     simp only at h
     subst h
     refine' ext _ _ rfl _
-    · haveI := hf
-      simp only [eqToHom_refl, comp_id]
-      exact eq_id_of_epi f
+    haveI := hf
+    simp only [eqToHom_refl, comp_id]
+    exact eq_id_of_epi f
 #align simplicial_object.splitting.index_set.eq_id_iff_eq SimplicialObject.Splitting.IndexSet.eqId_iff_eq
 
 theorem eqId_iff_len_eq : A.EqId ↔ A.1.unop.len = Δ.unop.len := by

Mathlib/Analysis/Analytic/Composition.lean

@@ -1120,7 +1120,7 @@ def sigmaEquivSigmaPi (n : ℕ) :
       have A : length (gather a b) = List.length (splitWrtComposition a.blocks b) := by
         simp only [length, gather, length_map, length_splitWrtComposition]
       congr! 2
-      · exact (Fin.heq_fun_iff A (α := List ℕ)).2 fun i => rfl
+      exact (Fin.heq_fun_iff A (α := List ℕ)).2 fun i => rfl
     · have B : Composition.length (Composition.gather a b) = List.length b.blocks :=
         Composition.length_gather _ _
       conv_rhs => rw [← ofFn_get b.blocks]

Mathlib/Analysis/Analytic/IsolatedZeros.lean

@@ -77,7 +77,7 @@ theorem has_fpower_series_dslope_fslope (hp : HasFPowerSeriesAt f p z₀) :
   · have hxx : ∀ n : ℕ, x⁻¹ * x ^ (n + 1) = x ^ n := fun n => by field_simp [h, _root_.pow_succ]
     suffices HasSum (fun n => x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀)) by
       simpa [dslope, slope, h, smul_smul, hxx] using this
-    · simpa [hp0] using ((hasSum_nat_add_iff' 1).mpr hx).const_smul x⁻¹
+    simpa [hp0] using ((hasSum_nat_add_iff' 1).mpr hx).const_smul x⁻¹
 #align has_fpower_series_at.has_fpower_series_dslope_fslope HasFPowerSeriesAt.has_fpower_series_dslope_fslope
 
 theorem has_fpower_series_iterate_dslope_fslope (n : ℕ) (hp : HasFPowerSeriesAt f p z₀) :

Mathlib/Analysis/Complex/AbsMax.lean

@@ -133,8 +133,8 @@ theorem norm_max_aux₁ [CompleteSpace F] {f : ℂ → F} {z w : ℂ}
     rw [le_div_iff hr, norm_smul, norm_inv, norm_eq_abs, hζ, mul_comm, mul_inv_cancel_left₀ hr.ne']
     exact hz (hsub hζ)
   show ‖(w - z)⁻¹ • f w‖ < ‖f z‖ / r
-  · rw [norm_smul, norm_inv, norm_eq_abs, ← div_eq_inv_mul]
-    exact (div_lt_div_right hr).2 hw_lt
+  rw [norm_smul, norm_inv, norm_eq_abs, ← div_eq_inv_mul]
+  exact (div_lt_div_right hr).2 hw_lt
 #align complex.norm_max_aux₁ Complex.norm_max_aux₁
 
 /-!

Mathlib/Analysis/Convex/Independent.lean

@@ -192,7 +192,7 @@ theorem convexIndependent_iff_finset {p : ι → E} :
   suffices x ∈ t.preimage p (hp.injOn _) by rwa [mem_preimage, ← mem_coe] at this
   refine' h _ x _
   rwa [t.image_preimage p (hp.injOn _), filter_true_of_mem]
-  · exact fun y hy => s.image_subset_range p (ht <| mem_coe.2 hy)
+  exact fun y hy => s.image_subset_range p (ht <| mem_coe.2 hy)
 #align convex_independent_iff_finset convexIndependent_iff_finset
 
 /-! ### Extreme points -/

Mathlib/Analysis/Convolution.lean

@@ -991,12 +991,12 @@ theorem convolution_assoc (hL : ∀ (x : E) (y : E') (z : E''), L₂ (L x y) z =
     (L₃ (f t)).integrable_comp <| ht.ofNorm L₄ hg hk, _⟩
   refine' (hfgk.const_mul (‖L₃‖ * ‖L₄‖)).mono' h2_meas
     (((quasiMeasurePreserving_sub_left_of_right_invariant ν x₀).ae hgk).mono fun t ht => _)
-  · simp_rw [convolution_def, mul_apply', mul_mul_mul_comm ‖L₃‖ ‖L₄‖, ← integral_mul_left]
-    rw [Real.norm_of_nonneg (by positivity)]
-    refine' integral_mono_of_nonneg (eventually_of_forall fun t => norm_nonneg _)
-      ((ht.const_mul _).const_mul _) (eventually_of_forall fun s => _)
-    simp only [← mul_assoc ‖L₄‖]
-    apply_rules [ContinuousLinearMap.le_of_opNorm₂_le_of_le, le_rfl]
+  simp_rw [convolution_def, mul_apply', mul_mul_mul_comm ‖L₃‖ ‖L₄‖, ← integral_mul_left]
+  rw [Real.norm_of_nonneg (by positivity)]
+  refine' integral_mono_of_nonneg (eventually_of_forall fun t => norm_nonneg _)
+    ((ht.const_mul _).const_mul _) (eventually_of_forall fun s => _)
+  simp only [← mul_assoc ‖L₄‖]
+  apply_rules [ContinuousLinearMap.le_of_opNorm₂_le_of_le, le_rfl]
 #align convolution_assoc MeasureTheory.convolution_assoc
 
 end Assoc

Mathlib/Analysis/InnerProductSpace/PiL2.lean

@@ -827,7 +827,7 @@ theorem Orthonormal.exists_orthonormalBasis_extension_of_card_eq {ι : Type*} [F
   obtain ⟨g, hg⟩ := hvsY.exists_equiv_extend_of_card_eq hιY hsv'
   use b₀.reindex g.symm
   intro i hi
-  · simp [hb₀, hg i hi]
+  simp [hb₀, hg i hi]
 #align orthonormal.exists_orthonormal_basis_extension_of_card_eq Orthonormal.exists_orthonormalBasis_extension_of_card_eq
 
 variable (𝕜 E)

Mathlib/Analysis/InnerProductSpace/Projection.lean

@@ -631,7 +631,7 @@ theorem orthogonalProjection_singleton {v : E} (w : E) :
     (orthogonalProjection (𝕜 ∙ v) w : E) = (⟪v, w⟫ / ((‖v‖ ^ 2 : ℝ) : 𝕜)) • v := by
   by_cases hv : v = 0
   · rw [hv, eq_orthogonalProjection_of_eq_submodule (Submodule.span_zero_singleton 𝕜)]
-    · simp
+    simp
   have hv' : ‖v‖ ≠ 0 := ne_of_gt (norm_pos_iff.mpr hv)
   have key :
     (((‖v‖ ^ 2 : ℝ) : 𝕜)⁻¹ * ((‖v‖ ^ 2 : ℝ) : 𝕜)) • ((orthogonalProjection (𝕜 ∙ v) w) : E) =

Mathlib/Analysis/InnerProductSpace/Symmetric.lean

@@ -171,9 +171,9 @@ theorem IsSymmetric.inner_map_polarization {T : E →ₗ[𝕜] E} (hT : T.IsSymm
     suffices (re ⟪T y, x⟫ : 𝕜) = ⟪T y, x⟫ by
       rw [conj_eq_iff_re.mpr this]
       ring
-    · rw [← re_add_im ⟪T y, x⟫]
-      simp_rw [h, mul_zero, add_zero]
-      norm_cast
+    rw [← re_add_im ⟪T y, x⟫]
+    simp_rw [h, mul_zero, add_zero]
+    norm_cast
   · simp_rw [map_add, map_sub, inner_add_left, inner_add_right, inner_sub_left, inner_sub_right,
       LinearMap.map_smul, inner_smul_left, inner_smul_right, RCLike.conj_I, mul_add, mul_sub,
       sub_sub, ← mul_assoc, mul_neg, h, neg_neg, one_mul, neg_one_mul]

Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean

@@ -51,12 +51,12 @@ theorem exists_extension_norm_eq (p : Subspace ℝ E) (f : p →L[ℝ] ℝ) :
       fun x => le_trans (le_abs_self _) (f.le_opNorm _) with ⟨g, g_eq, g_le⟩
   set g' :=
     g.mkContinuous ‖f‖ fun x => abs_le.2 ⟨neg_le.1 <| g.map_neg x ▸ norm_neg x ▸ g_le (-x), g_le x⟩
-  · refine' ⟨g', g_eq, _⟩
-    · apply le_antisymm (g.mkContinuous_norm_le (norm_nonneg f) _)
-      refine' f.opNorm_le_bound (norm_nonneg _) fun x => _
-      dsimp at g_eq
-      rw [← g_eq]
-      apply g'.le_opNorm
+  refine' ⟨g', g_eq, _⟩
+  apply le_antisymm (g.mkContinuous_norm_le (norm_nonneg f) _)
+  refine' f.opNorm_le_bound (norm_nonneg _) fun x => _
+  dsimp at g_eq
+  rw [← g_eq]
+  apply g'.le_opNorm
 #align real.exists_extension_norm_eq Real.exists_extension_norm_eq
 
 end Real

Mathlib/Analysis/NormedSpace/MStructure.lean

@@ -141,7 +141,7 @@ theorem commute [FaithfulSMul M X] {P Q : M} (h₁ : IsLprojection X P) (h₂ :
         _ = P * (1 - Q) - (Q * P - Q * P * Q) := by noncomm_ring
     rwa [eq_sub_iff_add_eq, add_right_eq_self, sub_eq_zero] at e1
   show P * Q = Q * P
-  · rw [QP_eq_QPQ, PR_eq_RPR Q h₂]
+  rw [QP_eq_QPQ, PR_eq_RPR Q h₂]
 #align is_Lprojection.commute IsLprojection.commute
 
 theorem mul [FaithfulSMul M X] {P Q : M} (h₁ : IsLprojection X P) (h₂ : IsLprojection X Q) :