chore: fix focusing dots (#5708)

This PR is the result of running
```
find . -type f -name "*.lean" -exec sed -i -E 's/^( +)\. /\1· /' {} \;
find . -type f -name "*.lean" -exec sed -i -E 'N;s/^( +·)\n +(.*)$/\1 \2/;P;D' {} \;
```
which firstly replaces `.` focusing dots with `·` and secondly removes isolated instances of such dots, unifying them with the following line. A new rule is placed in the style linter to verify this.

Mathlib/Algebra/BigOperators/Basic.lean

@@ -2111,8 +2111,7 @@ theorem finset_sum_eq_sup_iff_disjoint {β : Type _} {i : Finset β} {f : β →
     i.sum f = i.sup f ↔
       ∀ (x) (_ : x ∈ i) (y) (_ : y ∈ i), x ≠ y → Multiset.Disjoint (f x) (f y) := by
   induction' i using Finset.cons_induction_on with z i hz hr
-  ·
-    simp only [Finset.not_mem_empty, IsEmpty.forall_iff, imp_true_iff, Finset.sum_empty,
+  · simp only [Finset.not_mem_empty, IsEmpty.forall_iff, imp_true_iff, Finset.sum_empty,
       Finset.sup_empty, bot_eq_zero, eq_self_iff_true]
   · simp_rw [Finset.sum_cons hz, Finset.sup_cons, Finset.mem_cons, Multiset.sup_eq_union,
       forall_eq_or_imp, Ne.def, IsEmpty.forall_iff, true_and_iff,

Mathlib/Algebra/Category/MonCat/Adjunctions.lean

@@ -62,8 +62,8 @@ def adjoinOneAdj : adjoinOne ⊣ forget₂ MonCat.{u} SemigroupCat.{u} :=
         simp only [Equiv.symm_symm, adjoinOne_map, coe_comp]
         simp_rw [WithOne.map]
         cases x
-        . rfl
-        . simp
+        · rfl
+        · simp
           rfl }
 #align adjoin_one_adj adjoinOneAdj
 #align adjoin_zero_adj adjoinZeroAdj

Mathlib/Algebra/Category/MonCat/Colimits.lean

@@ -227,17 +227,17 @@ def descFun (s : Cocone F) : ColimitType F → s.pt := by
   · intro x y r
     induction' r with _ _ _ _ h _ _ _ _ _ h₁ h₂ _ _ f x _ _ _ _ _ _ _ _ h _ _ _ _ h <;> try simp
     -- symm
-    . exact h.symm
+    · exact h.symm
     -- trans
-    . exact h₁.trans h₂
+    · exact h₁.trans h₂
     -- map
-    . exact s.w_apply f x
+    · exact s.w_apply f x
     -- mul_1
-    . rw [h]
+    · rw [h]
     -- mul_2
-    . rw [h]
+    · rw [h]
     -- mul_assoc
-    . rw [mul_assoc]
+    · rw [mul_assoc]
 set_option linter.uppercaseLean3 false in
 #align Mon.colimits.desc_fun MonCat.Colimits.descFun
 
@@ -261,12 +261,12 @@ def colimitIsColimit : IsColimit (colimitCocone F) where
     ext x
     induction' x using Quot.inductionOn with x
     induction' x with j x x y hx hy
-    . change _ = s.ι.app j _
+    · change _ = s.ι.app j _
       rw [← w j]
       rfl
-    . rw [quot_one, map_one]
+    · rw [quot_one, map_one]
       rfl
-    . rw [quot_mul, map_mul, hx, hy]
+    · rw [quot_mul, map_mul, hx, hy]
       dsimp [descMorphism, FunLike.coe, descFun]
       simp only [← quot_mul, descFunLift]
 set_option linter.uppercaseLean3 false in

Mathlib/Algebra/DirectLimit.lean

@@ -489,8 +489,7 @@ theorem of.zero_exact_aux2 {x : FreeCommRing (Σi, G i)} {s t} (hxs : IsSupporte
     f' j k hjk (lift (fun ix : s => f' ix.1.1 j (hj ix ix.2) ix.1.2) (restriction s x)) =
       lift (fun ix : t => f' ix.1.1 k (hk ix ix.2) ix.1.2) (restriction t x) := by
   refine' Subring.InClosure.recOn hxs _ _ _ _
-  ·
-    rw [(restriction _).map_one, (FreeCommRing.lift _).map_one, (f' j k hjk).map_one,
+  · rw [(restriction _).map_one, (FreeCommRing.lift _).map_one, (f' j k hjk).map_one,
       (restriction _).map_one, (FreeCommRing.lift _).map_one]
   · -- porting note: Lean 3 had `(FreeCommRing.lift _).map_neg` but I needed to replace it with
   -- `RingHom.map_neg` to get the rewrite to compile

Mathlib/Algebra/GCDMonoid/Finset.lean

@@ -168,8 +168,7 @@ theorem dvd_gcd {a : α} : (∀ b ∈ s, a ∣ f b) → a ∣ s.gcd f :=
 theorem gcd_insert [DecidableEq β] {b : β} :
     (insert b s : Finset β).gcd f = GCDMonoid.gcd (f b) (s.gcd f) := by
   by_cases h : b ∈ s
-  ·
-    rw [insert_eq_of_mem h,
+  · rw [insert_eq_of_mem h,
       (gcd_eq_right_iff (f b) (s.gcd f) (Multiset.normalize_gcd (s.1.map f))).2 (gcd_dvd h)]
   apply fold_insert h
 #align finset.gcd_insert Finset.gcd_insert

Mathlib/Algebra/GroupPower/Order.lean

@@ -403,10 +403,10 @@ theorem zero_pow_le_one : ∀ n : ℕ, (0 : R) ^ n ≤ 1
 theorem pow_add_pow_le (hx : 0 ≤ x) (hy : 0 ≤ y) (hn : n ≠ 0) : x ^ n + y ^ n ≤ (x + y) ^ n := by
   rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩
   induction' k with k ih;
-  . have eqn : Nat.succ Nat.zero = 1 := rfl
+  · have eqn : Nat.succ Nat.zero = 1 := rfl
     rw [eqn]
     simp only [pow_one, le_refl]
-  . let n := k.succ
+  · let n := k.succ
     have h1 := add_nonneg (mul_nonneg hx (pow_nonneg hy n)) (mul_nonneg hy (pow_nonneg hx n))
     have h2 := add_nonneg hx hy
     calc

Mathlib/Algebra/Homology/Additive.lean

@@ -359,12 +359,12 @@ def single₀MapHomologicalComplex (F : V ⥤ W) [F.Additive] :
               | _ + 1 => F.mapZeroObject.inv }
         hom_inv_id := by
           ext (_|_)
-          . simp
-          . exact IsZero.eq_of_src (IsZero.of_iso (isZero_zero _) F.mapZeroObject) _ _
+          · simp
+          · exact IsZero.eq_of_src (IsZero.of_iso (isZero_zero _) F.mapZeroObject) _ _
         inv_hom_id := by
           ext (_|_)
-          . simp
-          . exact IsZero.eq_of_src (isZero_zero _) _ _ })
+          · simp
+          · exact IsZero.eq_of_src (isZero_zero _) _ _ })
     fun f => by ext (_|_) <;> simp
 #align chain_complex.single₀_map_homological_complex ChainComplex.single₀MapHomologicalComplex
 
@@ -415,12 +415,12 @@ def single₀MapHomologicalComplex (F : V ⥤ W) [F.Additive] :
               | _ + 1 => F.mapZeroObject.inv }
         hom_inv_id := by
           ext (_|_)
-          . simp
-          . exact IsZero.eq_of_src (IsZero.of_iso (isZero_zero _) F.mapZeroObject) _ _
+          · simp
+          · exact IsZero.eq_of_src (IsZero.of_iso (isZero_zero _) F.mapZeroObject) _ _
         inv_hom_id := by
           ext (_|_)
-          . simp
-          . exact IsZero.eq_of_src (isZero_zero _) _ _ })
+          · simp
+          · exact IsZero.eq_of_src (isZero_zero _) _ _ })
     fun f => by ext (_|_) <;> simp
 #align cochain_complex.single₀_map_homological_complex CochainComplex.single₀MapHomologicalComplex
 

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -75,7 +75,7 @@ theorem d_comp_d (C : HomologicalComplex V c) (i j k : ι) : C.d i j ≫ C.d j k
   by_cases hij : c.Rel i j
   · by_cases hjk : c.Rel j k
     · exact C.d_comp_d' i j k hij hjk
-    . rw [C.shape j k hjk, comp_zero]
+    · rw [C.shape j k hjk, comp_zero]
   · rw [C.shape i j hij, zero_comp]
 #align homological_complex.d_comp_d HomologicalComplex.d_comp_d
 
@@ -91,8 +91,8 @@ theorem ext {C₁ C₂ : HomologicalComplex V c} (h_X : C₁.X = C₂.X)
   simp only [mk.injEq, heq_eq_eq, true_and]
   ext i j
   by_cases hij: c.Rel i j
-  . simpa only [comp_id, id_comp, eqToHom_refl] using h_d i j hij
-  . rw [s₁ i j hij, s₂ i j hij]
+  · simpa only [comp_id, id_comp, eqToHom_refl] using h_d i j hij
+  · rw [s₁ i j hij, s₂ i j hij]
 #align homological_complex.ext HomologicalComplex.ext
 
 end HomologicalComplex
@@ -188,7 +188,7 @@ theorem Hom.comm {A B : HomologicalComplex V c} (f : A.Hom B) (i j : ι) :
     f.f i ≫ B.d i j = A.d i j ≫ f.f j := by
   by_cases hij : c.Rel i j
   · exact f.comm' i j hij
-  . rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]
+  · rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]
 #align homological_complex.hom.comm HomologicalComplex.Hom.comm
 
 instance (A B : HomologicalComplex V c) : Inhabited (Hom A B) :=

Mathlib/Algebra/Homology/Homotopy.lean

@@ -122,7 +122,7 @@ theorem prevD_nat (C D : CochainComplex V ℕ) (i : ℕ) (f : ∀ i j, C.X i ⟶
   cases i
   · simp only [shape, CochainComplex.prev_nat_zero, ComplexShape.up_Rel, Nat.one_ne_zero,
       not_false_iff, comp_zero]
-  . congr <;> simp
+  · congr <;> simp
 #align prev_d_nat prevD_nat
 
 -- porting note: removed @[has_nonempty_instance]
@@ -555,16 +555,16 @@ def mkInductive : Homotopy e 0 where
     simp only [add_zero]
     refine' (mkInductiveAux₂ e zero comm_zero one comm_one succ i).2.2.trans _
     congr
-    . cases i
-      . dsimp [fromNext, mkInductiveAux₂]
+    · cases i
+      · dsimp [fromNext, mkInductiveAux₂]
         rw [dif_neg]
         simp only
-      . dsimp [fromNext]
+      · dsimp [fromNext]
         simp only [ChainComplex.next_nat_succ, dite_true]
         rw [mkInductiveAux₃ e zero comm_zero one comm_one succ]
         dsimp [xNextIso]
         rw [Category.id_comp]
-    . dsimp [toPrev]
+    · dsimp [toPrev]
       erw [dif_pos, Category.comp_id]
       simp only [ChainComplex.prev]
 #align homotopy.mk_inductive Homotopy.mkInductive
@@ -680,16 +680,16 @@ def mkCoinductive : Homotopy e 0 where
     rw [add_comm]
     refine' (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).2.2.trans _
     congr
-    . cases i
-      . dsimp [toPrev, mkCoinductiveAux₂]
+    · cases i
+      · dsimp [toPrev, mkCoinductiveAux₂]
         rw [dif_neg]
         simp only
-      . dsimp [toPrev]
+      · dsimp [toPrev]
         simp only [CochainComplex.prev_nat_succ, dite_true]
         rw [mkCoinductiveAux₃ e zero comm_zero one comm_one succ]
         dsimp [xPrevIso]
         rw [Category.comp_id]
-    . dsimp [fromNext]
+    · dsimp [fromNext]
       erw [dif_pos, Category.id_comp]
       simp only [CochainComplex.next]
 #align homotopy.mk_coinductive Homotopy.mkCoinductive

Mathlib/Algebra/Homology/Single.lean

@@ -136,12 +136,12 @@ def single₀ : V ⥤ ChainComplex V ℕ where
         | n + 1 => 0 }
   map_id X := by
     ext (_|_)
-    . rfl
-    . simp
+    · rfl
+    · simp
   map_comp f g := by
     ext (_|_)
-    . rfl
-    . simp
+    · rfl
+    · simp
 #align chain_complex.single₀ ChainComplex.single₀
 
 @[simp]
@@ -239,10 +239,10 @@ def toSingle₀Equiv (C : ChainComplex V ℕ) (X : V) :
         | n + 1 => 0
       comm' := fun i j h => by
         rcases i with (_|_|i) <;> cases j <;> simp only [single₀_obj_X_d, comp_zero]
-        . rw [C.shape, zero_comp]
+        · rw [C.shape, zero_comp]
           simp
-        . exact f.2.symm
-        . rw [C.shape, zero_comp]
+        · exact f.2.symm
+        · rw [C.shape, zero_comp]
           exact i.succ_succ_ne_one.symm }
   left_inv f := by
     ext i
@@ -297,9 +297,9 @@ def single₀IsoSingle : single₀ V ≅ single V _ 0 :=
         hom_inv_id := to_single₀_ext _ _ (by simp)
         inv_hom_id := by
           ext (_|_)
-          . dsimp
+          · dsimp
             simp
-          . dsimp
+          · dsimp
             rw [Category.comp_id] })
     fun f => by ext (_|_) <;> aesop_cat
 #align chain_complex.single₀_iso_single ChainComplex.single₀IsoSingle
@@ -333,12 +333,12 @@ def single₀ : V ⥤ CochainComplex V ℕ where
         | n + 1 => 0 }
   map_id X := by
     ext (_|_)
-    . rfl
-    . simp
+    · rfl
+    · simp
   map_comp f g := by
     ext (_|_)
-    . rfl
-    . simp
+    · rfl
+    · simp
 #align cochain_complex.single₀ CochainComplex.single₀
 
 @[simp]
@@ -436,10 +436,10 @@ def fromSingle₀Equiv (C : CochainComplex V ℕ) (X : V) :
       comm' := fun i j h => by
         rcases f with ⟨f, hf⟩
         rcases j with (_|_|j) <;> cases i <;> simp only [single₀_obj_X_d, zero_comp]
-        . rw [C.shape, comp_zero]
+        · rw [C.shape, comp_zero]
           simp
-        . exact hf
-        . rw [C.shape, comp_zero]
+        · exact hf
+        · rw [C.shape, comp_zero]
           simp
           exact j.succ_succ_ne_one.symm }
   left_inv f := by
@@ -470,9 +470,9 @@ def single₀IsoSingle : single₀ V ≅ single V _ 0 :=
       hom_inv_id := from_single₀_ext _ _ (by simp)
       inv_hom_id := by
         ext (_|_)
-        . dsimp
+        · dsimp
           simp
-        . dsimp
+        · dsimp
           rw [Category.id_comp]
           rfl }
 #align cochain_complex.single₀_iso_single CochainComplex.single₀IsoSingle

Mathlib/Algebra/IndicatorFunction.lean

@@ -464,11 +464,9 @@ theorem mulIndicator_mul_compl_eq_piecewise [DecidablePred (· ∈ s)] (f g : α
     s.mulIndicator f * sᶜ.mulIndicator g = s.piecewise f g := by
   ext x
   by_cases h : x ∈ s
-  ·
-    rw [piecewise_eq_of_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_mem h,
+  · rw [piecewise_eq_of_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_mem h,
       Set.mulIndicator_of_not_mem (Set.not_mem_compl_iff.2 h), mul_one]
-  ·
-    rw [piecewise_eq_of_not_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_not_mem h,
+  · rw [piecewise_eq_of_not_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_not_mem h,
       Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]
 #align set.mul_indicator_mul_compl_eq_piecewise Set.mulIndicator_mul_compl_eq_piecewise
 #align set.indicator_add_compl_eq_piecewise Set.indicator_add_compl_eq_piecewise

Mathlib/Algebra/Module/LinearMap.lean

@@ -373,8 +373,7 @@ theorem _root_.preimage_smul_setₛₗ [SemilinearMapClass F σ M M₃] {c : R}
   apply Set.Subset.antisymm
   · rintro x ⟨y, ys, hy⟩
     refine' ⟨(hc.unit.inv : R) • x, _, _⟩
-    ·
-      simp only [← hy, smul_smul, Set.mem_preimage, Units.inv_eq_val_inv, map_smulₛₗ h, ← map_mul,
+    · simp only [← hy, smul_smul, Set.mem_preimage, Units.inv_eq_val_inv, map_smulₛₗ h, ← map_mul,
         IsUnit.val_inv_mul, one_smul, map_one, ys]
     · simp only [smul_smul, IsUnit.mul_val_inv, one_smul, Units.inv_eq_val_inv]
   · rintro x ⟨y, hy, rfl⟩

Mathlib/Algebra/Order/Field/Basic.lean

@@ -237,8 +237,8 @@ theorem div_le_of_nonneg_of_le_mul (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c *
 /-- One direction of `div_le_iff` where `c` is allowed to be `0` (but `b` must be nonnegative) -/
 lemma mul_le_of_nonneg_of_le_div (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ b / c) : a * c ≤ b := by
   obtain rfl | hc := hc.eq_or_lt
-  . simpa using hb
-  . rwa [le_div_iff hc] at h
+  · simpa using hb
+  · rwa [le_div_iff hc] at h
 #align mul_le_of_nonneg_of_le_div mul_le_of_nonneg_of_le_div
 
 theorem div_le_one_of_le (h : a ≤ b) (hb : 0 ≤ b) : a / b ≤ 1 :=

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -273,7 +273,7 @@ theorem isAffineOpen_iff_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : Is
     dsimp [Opens.inclusion]
     rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk, Subtype.range_coe, Subtype.range_coe]
     rfl
-  . infer_instance
+  · infer_instance
 #align algebraic_geometry.is_affine_open_iff_of_is_open_immersion AlgebraicGeometry.isAffineOpen_iff_of_isOpenImmersion
 
 instance Scheme.quasi_compact_of_affine (X : Scheme) [IsAffine X] : CompactSpace X :=
@@ -349,7 +349,7 @@ theorem IsAffineOpen.basicOpenIsAffine {X : Scheme} {U : Opens X} (hU : IsAffine
     Scheme.Spec.map
       (CommRingCat.ofHom (algebraMap ((X.presheaf.obj <| op U)) (Localization.Away f))).op ≫
     hU.fromSpec
-  . exact PresheafedSpace.IsOpenImmersion.comp (hf := inferInstance) (hg := inferInstance)
+  · exact PresheafedSpace.IsOpenImmersion.comp (hf := inferInstance) (hg := inferInstance)
   convert
     rangeIsAffineOpenOfOpenImmersion
       (Scheme.Spec.map
@@ -406,7 +406,7 @@ theorem Scheme.map_PrimeSpectrum_basicOpen_of_affine (X : Scheme) [IsAffine X]
       ((Scheme.Spec.obj (op (Scheme.Γ.obj (op X)))).basicOpen
         ((inv (X.isoSpec.hom.1.c.app (op ((Opens.map (inv X.isoSpec.hom).val.base).obj ⊤))))
           ((X.presheaf.map (eqToHom <| by congr)) f)))
-  . congr
+  · congr
     · rw [← IsIso.inv_eq_inv, IsIso.inv_inv, IsIso.Iso.inv_inv, NatIso.app_hom]
       -- Porting note : added this `change` to prevent timeout
       change SpecΓIdentity.hom.app (X.presheaf.obj <| op ⊤) = _

Mathlib/AlgebraicGeometry/Limits.lean

@@ -106,7 +106,7 @@ instance (priority := 100) isIso_of_isEmpty {X Y : Scheme} (f : X ⟶ Y) [IsEmpt
     IsIso f := by
   haveI : IsEmpty X.carrier := ⟨fun x => isEmptyElim (show Y.carrier from f.1.base x)⟩
   have : Epi f.1.base
-  . rw [TopCat.epi_iff_surjective]; rintro (x : Y.carrier)
+  · rw [TopCat.epi_iff_surjective]; rintro (x : Y.carrier)
     exact isEmptyElim x
   apply IsOpenImmersion.to_iso
 #align algebraic_geometry.is_iso_of_is_empty AlgebraicGeometry.isIso_of_isEmpty

Mathlib/AlgebraicGeometry/LocallyRingedSpace/HasColimits.lean

@@ -299,7 +299,7 @@ noncomputable def coequalizerCoforkIsColimit : IsColimit (coequalizerCofork f g)
     set h := _
     change IsLocalRingHom h
     suffices : IsLocalRingHom ((PresheafedSpace.stalkMap (coequalizerCofork f g).π.1 _).comp h)
-    . apply isLocalRingHom_of_comp _ (PresheafedSpace.stalkMap (coequalizerCofork f g).π.1 _)
+    · apply isLocalRingHom_of_comp _ (PresheafedSpace.stalkMap (coequalizerCofork f g).π.1 _)
     change IsLocalRingHom (_ ≫ PresheafedSpace.stalkMap (coequalizerCofork f g).π.val y)
     erw [← PresheafedSpace.stalkMap.comp]
     apply isLocalRingHom_stalkMap_congr _ _ (coequalizer.π_desc s.π.1 e).symm y
@@ -331,7 +331,7 @@ noncomputable instance preservesCoequalizer :
     -- of colimit is provided later
     suffices : PreservesColimit (parallelPair (F.map WalkingParallelPairHom.left)
       (F.map WalkingParallelPairHom.right)) forgetToSheafedSpace
-    . apply preservesColimitOfIsoDiagram _ (diagramIsoParallelPair F).symm
+    · apply preservesColimitOfIsoDiagram _ (diagramIsoParallelPair F).symm
     apply preservesColimitOfPreservesColimitCocone (coequalizerCoforkIsColimit _ _)
     apply (isColimitMapCoconeCoforkEquiv _ _).symm _
     dsimp only [forgetToSheafedSpace]