chore: remove unnecessary cdots (#12417)

These `·` are scoping when there is a single active goal.

These were found using a modification of the linter at #12339.

Mathlib/Algebra/BigOperators/Associated.lean

@@ -91,15 +91,15 @@ theorem Multiset.prod_primes_dvd [CancelCommMonoidWithZero α]
     apply mul_dvd_mul_left a
     refine induct _ (fun a ha => h a (Multiset.mem_cons_of_mem ha)) (fun b b_in_s => ?_)
       fun a => (Multiset.countP_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)
-    · have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
-      have a_prime := h a (Multiset.mem_cons_self a s)
-      have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
-      refine' (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => _
-      have assoc := b_prime.associated_of_dvd a_prime b_div_a
-      have := uniq a
-      rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
-        Multiset.countP_pos] at this
-      exact this ⟨b, b_in_s, assoc.symm⟩
+    have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
+    have a_prime := h a (Multiset.mem_cons_self a s)
+    have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
+    refine' (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => _
+    have assoc := b_prime.associated_of_dvd a_prime b_div_a
+    have := uniq a
+    rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
+      Multiset.countP_pos] at this
+    exact this ⟨b, b_in_s, assoc.symm⟩
 #align multiset.prod_primes_dvd Multiset.prod_primes_dvd
 
 theorem Finset.prod_primes_dvd [CancelCommMonoidWithZero α] [Unique αˣ] {s : Finset α} (n : α)

Mathlib/Algebra/BigOperators/Basic.lean

@@ -2075,8 +2075,8 @@ theorem mem_sum {f : α → Multiset β} (s : Finset α) (b : β) :
     (b ∈ ∑ x in s, f x) ↔ ∃ a ∈ s, b ∈ f a := by
   classical
     refine' s.induction_on (by simp) _
-    · intro a t hi ih
-      simp [sum_insert hi, ih, or_and_right, exists_or]
+    intro a t hi ih
+    simp [sum_insert hi, ih, or_and_right, exists_or]
 #align finset.mem_sum Finset.mem_sum
 
 section ProdEqZero

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -295,7 +295,7 @@ lemma prod_range_diag_flip (n : ℕ) (f : ℕ → ℕ → M) :
       Nat.lt_succ_iff, le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, imp_self,
       implies_true, Sigma.forall, forall_const, add_tsub_cancel_of_le, Sigma.mk.inj_iff,
       add_tsub_cancel_left, heq_eq_eq]
-  · exact fun a b han hba ↦ lt_of_le_of_lt hba han
+  exact fun a b han hba ↦ lt_of_le_of_lt hba han
 #align sum_range_diag_flip Finset.sum_range_diag_flip
 
 end Generic

Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean

@@ -94,7 +94,7 @@ theorem mul_mem_cancel_left {c d e : C} {f : c ⟶ d} {g : d ⟶ e} (hf : f ∈
   · rintro h
     suffices Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e by
       simpa only [inv_eq_inv, IsIso.inv_hom_id_assoc] using this
-    · apply S.mul (S.inv hf) h
+    apply S.mul (S.inv hf) h
   · apply S.mul hf
 #align category_theory.subgroupoid.mul_mem_cancel_left CategoryTheory.Subgroupoid.mul_mem_cancel_left
 
@@ -104,7 +104,7 @@ theorem mul_mem_cancel_right {c d e : C} {f : c ⟶ d} {g : d ⟶ e} (hg : g ∈
   · rintro h
     suffices (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d by
       simpa only [inv_eq_inv, IsIso.hom_inv_id, Category.comp_id, Category.assoc] using this
-    · apply S.mul h (S.inv hg)
+    apply S.mul h (S.inv hg)
   · exact fun hf => S.mul hf hg
 #align category_theory.subgroupoid.mul_mem_cancel_right CategoryTheory.Subgroupoid.mul_mem_cancel_right
 
@@ -590,7 +590,7 @@ theorem isNormal_map (hφ : Function.Injective φ.obj) (hφ' : im φ hφ = ⊤)
       simp only [eqToHom_refl, Category.comp_id, Category.id_comp, inv_eq_inv]
       suffices Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (φ.map <| Groupoid.inv f ≫ γ ≫ f) by
         simp only [inv_eq_inv, Functor.map_comp, Functor.map_inv] at this; exact this
-      · constructor; apply Sn.conj f γS }
+      constructor; apply Sn.conj f γS }
 #align category_theory.subgroupoid.is_normal_map CategoryTheory.Subgroupoid.isNormal_map
 
 end Hom

Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

@@ -271,8 +271,8 @@ def preservesLimitsOfShapeOfEquiv {J' : Type w₂} [Category.{w₂'} J'] (e : J
         have := (isLimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
         apply ((IsLimit.postcomposeHomEquiv equ _).symm this).ofIsoLimit
         refine' Cones.ext (Iso.refl _) fun j => _
-        · dsimp
-          simp [equ, ← Functor.map_comp] }
+        dsimp
+        simp [equ, ← Functor.map_comp] }
 #align category_theory.limits.preserves_limits_of_shape_of_equiv CategoryTheory.Limits.preservesLimitsOfShapeOfEquiv
 
 /-- A functor preserving larger limits also preserves smaller limits. -/
@@ -340,8 +340,8 @@ def preservesColimitsOfShapeOfEquiv {J' : Type w₂} [Category.{w₂'} J'] (e :
         have := (isColimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
         apply ((IsColimit.precomposeInvEquiv equ _).symm this).ofIsoColimit
         refine' Cocones.ext (Iso.refl _) fun j => _
-        · dsimp
-          simp [equ, ← Functor.map_comp] }
+        dsimp
+        simp [equ, ← Functor.map_comp] }
 #align category_theory.limits.preserves_colimits_of_shape_of_equiv CategoryTheory.Limits.preservesColimitsOfShapeOfEquiv
 
 /-- A functor preserving larger colimits also preserves smaller colimits. -/

Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

@@ -1441,13 +1441,13 @@ def Over.coprod [HasBinaryCoproducts C] {A : C} : Over A ⥤ Over A ⥤ Over A w
         dsimp; rw [coprod.map_desc, Category.id_comp, Over.w k])
       naturality := fun f g k => by
         ext;
-          · dsimp; simp }
+        dsimp; simp }
   map_id X := by
     ext
-    · dsimp; simp
+    dsimp; simp
   map_comp f g := by
     ext
-    · dsimp; simp
+    dsimp; simp
 #align category_theory.over.coprod CategoryTheory.Over.coprod
 
 end CategoryTheory

Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean

@@ -146,7 +146,7 @@ instance instFintypeWalkingParallelPairHom (j j' : WalkingParallelPair) :
       (WalkingParallelPair.recOn j' ∅ [WalkingParallelPairHom.id one].toFinset)
   complete := by
     rintro (_|_) <;> simp
-    · cases j <;> simp
+    cases j <;> simp
 end
 
 instance : FinCategory WalkingParallelPair where

Mathlib/CategoryTheory/Limits/Shapes/Images.lean

@@ -110,8 +110,8 @@ theorem ext {F F' : MonoFactorisation f} (hI : F.I = F'.I)
   cases' hI
   simp? at hm says simp only [eqToHom_refl, Category.id_comp] at hm
   congr
-  · apply (cancel_mono Fm).1
-    rw [Ffac, hm, Ffac']
+  apply (cancel_mono Fm).1
+  rw [Ffac, hm, Ffac']
 #align category_theory.limits.mono_factorisation.ext CategoryTheory.Limits.MonoFactorisation.ext
 
 /-- Any mono factorisation of `f` gives a mono factorisation of `f ≫ g` when `g` is a mono. -/

Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean

@@ -241,7 +241,7 @@ def wideSpan (B : C) (objs : J → C) (arrows : ∀ j : J, B ⟶ objs j) : WideP
     cases f
     · simp only [Eq.ndrec, hom_id, eq_rec_constant, Category.id_comp]; congr
     · cases g
-      · simp only [Eq.ndrec, hom_id, eq_rec_constant, Category.comp_id]; congr
+      simp only [Eq.ndrec, hom_id, eq_rec_constant, Category.comp_id]; congr
 #align category_theory.limits.wide_pushout_shape.wide_span CategoryTheory.Limits.WidePushoutShape.wideSpan
 
 /-- Every diagram is naturally isomorphic (actually, equal) to a `wideSpan` -/

Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

@@ -1938,9 +1938,9 @@ abbrev toDeleteEdge (e : Sym2 V) (p : G.Walk v w) (hp : e ∉ p.edges) :
 theorem map_toDeleteEdges_eq (s : Set (Sym2 V)) {p : G.Walk v w} (hp) :
     Walk.map (Hom.mapSpanningSubgraphs (G.deleteEdges_le s)) (p.toDeleteEdges s hp) = p := by
   rw [← transfer_eq_map_of_le, transfer_transfer, transfer_self]
-  · intros e
-    rw [edges_transfer]
-    apply edges_subset_edgeSet p
+  intros e
+  rw [edges_transfer]
+  apply edges_subset_edgeSet p
 #align simple_graph.walk.map_to_delete_edges_eq SimpleGraph.Walk.map_toDeleteEdges_eq
 
 protected theorem IsPath.toDeleteEdges (s : Set (Sym2 V))

Mathlib/Computability/Halting.lean

@@ -252,11 +252,11 @@ theorem computable_iff_re_compl_re {p : α → Prop} [DecidablePred p] :
           simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop,
             and_true, exists_const] at hx hy
           cases hy.1 hx.1)
-      · refine' Partrec.of_eq pk fun n => Part.eq_some_iff.2 _
-        rw [hk]
-        simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true,
-          true_eq_decide_iff, and_self, exists_const, false_eq_decide_iff]
-        apply Decidable.em⟩⟩
+      refine' Partrec.of_eq pk fun n => Part.eq_some_iff.2 _
+      rw [hk]
+      simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true,
+        true_eq_decide_iff, and_self, exists_const, false_eq_decide_iff]
+      apply Decidable.em⟩⟩
 #align computable_pred.computable_iff_re_compl_re ComputablePred.computable_iff_re_compl_re
 
 theorem computable_iff_re_compl_re' {p : α → Prop} :

Mathlib/Computability/Partrec.lean

@@ -835,10 +835,10 @@ theorem fix_aux {α σ} (f : α →. Sum σ α) (a : α) (b : σ) :
         exact Or.inr ⟨_, hk, h₂⟩
       · rwa [le_antisymm (Nat.le_of_lt_succ mk) km]
     · rcases IH _ am₃ k.succ (by simp [F]; exact ⟨_, hk, am₃⟩) with ⟨n, hn₁, hn₂⟩
-      · refine' ⟨n, hn₁, fun m mn km => _⟩
-        cases' km.lt_or_eq_dec with km km
-        · exact hn₂ _ mn km
-        · exact km ▸ ⟨_, hk⟩
+      refine' ⟨n, hn₁, fun m mn km => _⟩
+      cases' km.lt_or_eq_dec with km km
+      · exact hn₂ _ mn km
+      · exact km ▸ ⟨_, hk⟩
 #align partrec.fix_aux Partrec.fix_aux
 
 theorem fix {f : α →. Sum σ α} (hf : Partrec f) : Partrec (PFun.fix f) := by

Mathlib/Computability/TMToPartrec.lean

@@ -666,10 +666,10 @@ theorem cont_eval_fix {f k v} (fok : Code.Ok f) :
         obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
           IH (stepRet (k₀.then (Cont.fix f k)) v₀) (by rw [stepRet, if_neg he, e₁]; rfl)
             v'.tail _ stepRet_then (by apply ReflTransGen.single; rw [e₀]; rfl)
-        · refine' ⟨_, PFun.mem_fix_iff.2 _, h₃⟩
-          simp only [Part.eq_some_iff.2 hv₁, Part.map_some, Part.mem_some_iff]
-          split_ifs at hv₂ ⊢ <;> [exact Or.inl (congr_arg Sum.inl (Part.mem_some_iff.1 hv₂));
-            exact Or.inr ⟨_, rfl, hv₂⟩]
+        refine' ⟨_, PFun.mem_fix_iff.2 _, h₃⟩
+        simp only [Part.eq_some_iff.2 hv₁, Part.map_some, Part.mem_some_iff]
+        split_ifs at hv₂ ⊢ <;> [exact Or.inl (congr_arg Sum.inl (Part.mem_some_iff.1 hv₂));
+          exact Or.inr ⟨_, rfl, hv₂⟩]
     · exact IH _ rfl _ _ stepRet_then (ReflTransGen.tail hr rfl)
   · rintro ⟨v', he, hr⟩
     rw [reaches_eval] at hr
@@ -1340,8 +1340,8 @@ theorem move_ok {p k₁ k₂ q s L₁ o L₂} {S : K' → List Γ'} (h₁ : k₁
     simp only [splitAtPred, Option.elim, List.head?, List.tail_cons, Option.iget_some] at e ⊢
     revert e; cases p a <;> intro e <;>
       simp only [cond_false, cond_true, Prod.mk.injEq, true_and, false_and] at e ⊢
-    · simp only [e]
-      rfl
+    simp only [e]
+    rfl
   · refine' TransGen.head rfl _
     simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim, ne_eq, List.reverseAux_cons]
     cases' e₁ : S k₁ with a' Sk <;> rw [e₁, splitAtPred] at e
@@ -1398,8 +1398,8 @@ theorem clear_ok {p k q s L₁ o L₂} {S : K' → List Γ'} (e : splitAtPred p
     simp only [splitAtPred, Option.elim, List.head?, List.tail_cons] at e ⊢
     revert e; cases p a <;> intro e <;>
       simp only [cond_false, cond_true, Prod.mk.injEq, true_and, false_and] at e ⊢
-    · rcases e with ⟨e₁, e₂⟩
-      rw [e₁, e₂]
+    rcases e with ⟨e₁, e₂⟩
+    rw [e₁, e₂]
   · refine' TransGen.head rfl _
     simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
     cases' e₁ : S k with a' Sk <;> rw [e₁, splitAtPred] at e

Mathlib/Data/FP/Basic.lean

@@ -155,7 +155,7 @@ unsafe def ofPosRatDn (n : ℕ+) (d : ℕ+) : Float × Bool := by
   let r := mkRat n₂ d₂
   let m := r.floor
   refine' (Float.finite Bool.false e₃ (Int.toNat m) _, r.den = 1)
-  · exact lcProof
+  exact lcProof
 #align fp.of_pos_rat_dn FP.ofPosRatDn
 
 -- Porting note: remove this line when you dropped 'lcProof'

Mathlib/Data/Finset/Lattice.lean

@@ -1768,7 +1768,7 @@ theorem min_erase_ne_self {s : Finset α} : (s.erase x).min ≠ x := by
   convert @max_erase_ne_self αᵒᵈ _ (toDual x) (s.map toDual.toEmbedding) using 1
   apply congr_arg -- Porting note: forces unfolding to see `Finset.min` is `Finset.max`
   congr!
-  · ext; simp only [mem_map_equiv]; exact Iff.rfl
+  ext; simp only [mem_map_equiv]; exact Iff.rfl
 #align finset.min_erase_ne_self Finset.min_erase_ne_self
 
 theorem exists_next_right {x : α} {s : Finset α} (h : ∃ y ∈ s, x < y) :

Mathlib/Data/Finset/NatAntidiagonal.lean

@@ -72,7 +72,7 @@ theorem antidiagonal_succ (n : ℕ) :
         (by simp) := by
   apply eq_of_veq
   rw [cons_val, map_val]
-  · apply Multiset.Nat.antidiagonal_succ
+  apply Multiset.Nat.antidiagonal_succ
 #align finset.nat.antidiagonal_succ Finset.Nat.antidiagonal_succ
 
 theorem antidiagonal_succ' (n : ℕ) :

Mathlib/Data/Finset/Powerset.lean

@@ -320,9 +320,9 @@ theorem powersetCard_sup [DecidableEq α] (u : Finset α) (n : ℕ) (hn : n < u.
     simp only [mem_biUnion, exists_prop, id]
     obtain ⟨t, ht⟩ : ∃ t, t ∈ powersetCard n (u.erase x) := powersetCard_nonempty.2
       (le_trans (Nat.le_sub_one_of_lt hn) pred_card_le_card_erase)
-    · refine' ⟨insert x t, _, mem_insert_self _ _⟩
-      rw [← insert_erase hx, powersetCard_succ_insert (not_mem_erase _ _)]
-      exact mem_union_right _ (mem_image_of_mem _ ht)
+    refine' ⟨insert x t, _, mem_insert_self _ _⟩
+    rw [← insert_erase hx, powersetCard_succ_insert (not_mem_erase _ _)]
+    exact mem_union_right _ (mem_image_of_mem _ ht)
 #align finset.powerset_len_sup Finset.powersetCard_sup
 
 theorem powersetCard_map {β : Type*} (f : α ↪ β) (n : ℕ) (s : Finset α) :

Mathlib/Data/Finsupp/AList.lean

@@ -127,10 +127,10 @@ theorem _root_.Finsupp.toAList_lookupFinsupp (f : α →₀ M) : f.toAList.looku
   classical
     by_cases h : f a = 0
     · suffices f.toAList.lookup a = none by simp [h, this]
-      · simp [lookup_eq_none, h]
+      simp [lookup_eq_none, h]
     · suffices f.toAList.lookup a = some (f a) by simp [h, this]
-      · apply mem_lookup_iff.2
-        simpa using h
+      apply mem_lookup_iff.2
+      simpa using h
 #align finsupp.to_alist_lookup_finsupp Finsupp.toAList_lookupFinsupp
 
 theorem lookupFinsupp_surjective : Function.Surjective (@lookupFinsupp α M _) := fun f =>

Mathlib/Data/Finsupp/Basic.lean

@@ -481,7 +481,7 @@ theorem mapDomain_comp {f : α → β} {g : β → γ} :
   · intro
     exact single_add _
   refine' sum_congr fun _ _ => sum_single_index _
-  · exact single_zero _
+  exact single_zero _
 #align finsupp.map_domain_comp Finsupp.mapDomain_comp
 
 @[simp]

Mathlib/Data/Finsupp/BigOperators.lean

@@ -88,12 +88,12 @@ theorem List.support_sum_eq [AddMonoid M] (l : List (ι →₀ M))
     rw [Finsupp.support_add_eq, IH hl.right, Finset.sup_eq_union]
     suffices _root_.Disjoint hd.support (tl.foldr (fun x y ↦ (Finsupp.support x ⊔ y)) ∅) by
       exact Finset.disjoint_of_subset_right (List.support_sum_subset _) this
-    · rw [← List.foldr_map, ← Finset.bot_eq_empty, List.foldr_sup_eq_sup_toFinset,
-        Finset.disjoint_sup_right]
-      intro f hf
-      simp only [List.mem_toFinset, List.mem_map] at hf
-      obtain ⟨f, hf, rfl⟩ := hf
-      exact hl.left _ hf
+    rw [← List.foldr_map, ← Finset.bot_eq_empty, List.foldr_sup_eq_sup_toFinset,
+      Finset.disjoint_sup_right]
+    intro f hf
+    simp only [List.mem_toFinset, List.mem_map] at hf
+    obtain ⟨f, hf, rfl⟩ := hf
+    exact hl.left _ hf
 #align list.support_sum_eq List.support_sum_eq
 
 theorem Multiset.support_sum_eq [AddCommMonoid M] (s : Multiset (ι →₀ M))

Mathlib/Data/Fintype/Card.lean

@@ -1251,13 +1251,13 @@ theorem List.exists_pw_disjoint_with_card {α : Type*} [Fintype α]
     exact ranges_nodup hu
   · -- pairwise disjoint
     refine Pairwise.map _ (fun s t ↦ disjoint_map (Equiv.injective _)) ?_
-    · -- List.Pairwise List.disjoint l
-      apply Pairwise.pmap (List.ranges_disjoint c)
-      intro u hu v hv huv
-      apply disjoint_pmap
-      · intro a a' ha ha' h
-        simpa only [klift, Fin.mk_eq_mk] using h
-      exact huv
+    -- List.Pairwise List.disjoint l
+    apply Pairwise.pmap (List.ranges_disjoint c)
+    intro u hu v hv huv
+    apply disjoint_pmap
+    · intro a a' ha ha' h
+      simpa only [klift, Fin.mk_eq_mk] using h
+    exact huv
 
 end Ranges
 

Mathlib/Data/Fintype/Option.lean

@@ -101,7 +101,7 @@ theorem induction_empty_option {P : ∀ (α : Type u) [Fintype α], Prop}
       convert h_option α (Pα _)
     @truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _))
       f_empty h_option α _ (Classical.decEq α)
-  · exact p _
+  exact p _
   -- ·
 #align fintype.induction_empty_option Fintype.induction_empty_option
 

Mathlib/Data/Fintype/Pi.lean

@@ -125,7 +125,7 @@ theorem Fintype.piFinset_univ {α : Type*} {β : α → Type*} [DecidableEq α]
 -- but those don't work with subsingletons in lean4 as-is so we cannot do this here.
 noncomputable instance _root_.Function.Embedding.fintype {α β} [Fintype α] [Fintype β] :
   Fintype (α ↪ β) :=
-  by classical. exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β)
+  by classical exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β)
 #align function.embedding.fintype Function.Embedding.fintype
 
 @[simp]

Mathlib/Data/LazyList/Basic.lean

@@ -84,7 +84,7 @@ instance : LawfulTraversable LazyList := by
     · simp only [List.traverse, map_pure]; rfl
     · replace ih : tl.get.traverse f = ofList <$> tl.get.toList.traverse f := ih
       simp only [traverse._eq_2, ih, Functor.map_map, seq_map_assoc, toList, List.traverse, map_seq]
-      · rfl
+      rfl
     · apply ih
 
 /-- `init xs`, if `xs` non-empty, drops the last element of the list.

Mathlib/Data/List/NodupEquivFin.lean

@@ -220,7 +220,7 @@ theorem duplicate_iff_exists_distinct_get {l : List α} {x : α} :
     · rintro ⟨f, hf⟩
       refine' ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩,
         f.lt_iff_lt.2 (show (0 : ℕ) < 1 from zero_lt_one), _⟩
-      · rw [← hf, ← hf]; simp
+      rw [← hf, ← hf]; simp
     · rintro ⟨n, m, hnm, h, h'⟩
       refine' ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) _, _⟩
       · rintro ⟨⟨_ | i⟩, hi⟩ ⟨⟨_ | j⟩, hj⟩

Mathlib/Data/Nat/Digits.lean

@@ -244,8 +244,8 @@ theorem digits_ofDigits (b : ℕ) (h : 1 < b) (L : List ℕ) (w₁ : ∀ l ∈ L
         apply w₁
         exact List.mem_cons_of_mem _ m
       · intro h
-        · rw [List.getLast_cons h] at w₂
-          convert w₂
+        rw [List.getLast_cons h] at w₂
+        convert w₂
     · exact w₁ d (List.mem_cons_self _ _)
     · by_cases h' : L = []
       · rcases h' with rfl
@@ -366,8 +366,8 @@ theorem getLast_digit_ne_zero (b : ℕ) {m : ℕ} (hm : m ≠ 0) :
   · simpa only [digits_of_lt (b + 2) n hn hnb]
   · rw [digits_getLast n (le_add_left 2 b)]
     refine' IH _ (Nat.div_lt_self hn.bot_lt (one_lt_succ_succ b)) _
-    · rw [← pos_iff_ne_zero]
-      exact Nat.div_pos (le_of_not_lt hnb) (zero_lt_succ (succ b))
+    rw [← pos_iff_ne_zero]
+    exact Nat.div_pos (le_of_not_lt hnb) (zero_lt_succ (succ b))
 #align nat.last_digit_ne_zero Nat.getLast_digit_ne_zero
 
 /-- The digits in the base b+2 expansion of n are all less than b+2 -/

Mathlib/Data/Nat/Interval.lean

@@ -259,10 +259,10 @@ theorem Ico_image_const_sub_eq_Ico (hac : a ≤ c) :
     rw [lt_tsub_iff_left, Nat.lt_succ_iff] at ha
     have hx : x ≤ c := (Nat.le_add_left _ _).trans ha
     refine' ⟨c - x, _, tsub_tsub_cancel_of_le hx⟩
-    · rw [mem_Ico]
-      exact
-        ⟨le_tsub_of_add_le_right ha,
-          (tsub_lt_iff_left hx).2 <| succ_le_iff.1 <| tsub_le_iff_right.1 hb⟩
+    rw [mem_Ico]
+    exact
+      ⟨le_tsub_of_add_le_right ha,
+        (tsub_lt_iff_left hx).2 <| succ_le_iff.1 <| tsub_le_iff_right.1 hb⟩
 #align nat.Ico_image_const_sub_eq_Ico Nat.Ico_image_const_sub_eq_Ico
 
 theorem Ico_succ_left_eq_erase_Ico : Ico a.succ b = erase (Ico a b) a := by