diff --git a/Archive/Imo/Imo2006Q5.lean b/Archive/Imo/Imo2006Q5.lean
index e0314a7549364..7e47fb00973b6 100644
--- a/Archive/Imo/Imo2006Q5.lean
+++ b/Archive/Imo/Imo2006Q5.lean
@@ -173,21 +173,21 @@ theorem imo2006_q5' {P : Polynomial ℤ} (hP : 1 < P.natDegree) :
     suffices H' : (P.comp P - X).roots.toFinset ⊆ (P + (X : ℤ[X]) - a - b).roots.toFinset from
       (Finset.card_le_card H').trans
         ((Multiset.toFinset_card_le _).trans <| (card_roots' _).trans_eq hPab)
-    · -- Let t be a root of P(P(t)) - t, define u = P(t).
-      intro t ht
-      replace ht := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ht)
-      rw [IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero] at ht
-      simp only [mem_roots hPab', sub_eq_iff_eq_add, Multiset.mem_toFinset, IsRoot.def,
-        eval_sub, eval_add, eval_X, eval_C, eval_intCast, Int.cast_id, zero_add]
-      -- An auxiliary lemma proved earlier implies we only need to show |t - a| = |u - b| and
-      -- |t - b| = |u - a|. We prove this by establishing that each side of either equation divides
-      -- the other.
-      apply (Int.add_eq_add_of_natAbs_eq_of_natAbs_eq hab _ _).symm <;>
-          apply Int.natAbs_eq_of_dvd_dvd <;> set u := P.eval t
-      · rw [← ha, ← ht]; apply sub_dvd_eval_sub
-      · apply sub_dvd_eval_sub
-      · rw [← ht]; apply sub_dvd_eval_sub
-      · rw [← ha]; apply sub_dvd_eval_sub
+    -- Let t be a root of P(P(t)) - t, define u = P(t).
+    intro t ht
+    replace ht := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ht)
+    rw [IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero] at ht
+    simp only [mem_roots hPab', sub_eq_iff_eq_add, Multiset.mem_toFinset, IsRoot.def,
+      eval_sub, eval_add, eval_X, eval_C, eval_intCast, Int.cast_id, zero_add]
+    -- An auxiliary lemma proved earlier implies we only need to show |t - a| = |u - b| and
+    -- |t - b| = |u - a|. We prove this by establishing that each side of either equation divides
+    -- the other.
+    apply (Int.add_eq_add_of_natAbs_eq_of_natAbs_eq hab _ _).symm <;>
+        apply Int.natAbs_eq_of_dvd_dvd <;> set u := P.eval t
+    · rw [← ha, ← ht]; apply sub_dvd_eval_sub
+    · apply sub_dvd_eval_sub
+    · rw [← ht]; apply sub_dvd_eval_sub
+    · rw [← ha]; apply sub_dvd_eval_sub
 #align imo2006_q5.imo2006_q5' Imo2006Q5.imo2006_q5'
 
 end Imo2006Q5
diff --git a/Archive/Imo/Imo2021Q1.lean b/Archive/Imo/Imo2021Q1.lean
index 9946ba7529c00..95f3c944ecbdd 100644
--- a/Archive/Imo/Imo2021Q1.lean
+++ b/Archive/Imo/Imo2021Q1.lean
@@ -89,9 +89,9 @@ theorem exists_finset_3_le_card_with_pairs_summing_to_squares (n : ℕ) (hn : 10
     suffices a ∉ {b, c} ∧ b ∉ {c} by
       rw [Finset.card_insert_of_not_mem this.1, Finset.card_insert_of_not_mem this.2,
         Finset.card_singleton]
-    · rw [Finset.mem_insert, Finset.mem_singleton, Finset.mem_singleton]
-      push_neg
-      exact ⟨⟨hab.ne, (hab.trans hbc).ne⟩, hbc.ne⟩
+    rw [Finset.mem_insert, Finset.mem_singleton, Finset.mem_singleton]
+    push_neg
+    exact ⟨⟨hab.ne, (hab.trans hbc).ne⟩, hbc.ne⟩
   · intro x hx y hy hxy
     simp only [Finset.mem_insert, Finset.mem_singleton] at hx hy
     rcases hx with (rfl | rfl | rfl) <;> rcases hy with (rfl | rfl | rfl)
diff --git a/Archive/Wiedijk100Theorems/BallotProblem.lean b/Archive/Wiedijk100Theorems/BallotProblem.lean
index d4717924c25a0..9f62677722000 100644
--- a/Archive/Wiedijk100Theorems/BallotProblem.lean
+++ b/Archive/Wiedijk100Theorems/BallotProblem.lean
@@ -201,8 +201,8 @@ theorem count_countedSequence : ∀ p q : ℕ, count (countedSequence p q) = (p
     rw [counted_succ_succ, measure_union (disjoint_bits _ _) list_int_measurableSet,
       count_injective_image List.cons_injective, count_countedSequence _ _,
       count_injective_image List.cons_injective, count_countedSequence _ _]
-    · norm_cast
-      rw [add_assoc, add_comm 1 q, ← Nat.choose_succ_succ, Nat.succ_eq_add_one, add_right_comm]
+    norm_cast
+    rw [add_assoc, add_comm 1 q, ← Nat.choose_succ_succ, Nat.succ_eq_add_one, add_right_comm]
 #align ballot.count_counted_sequence Ballot.count_countedSequence
 
 theorem first_vote_pos :
@@ -237,12 +237,11 @@ theorem first_vote_pos :
       rw [(condCount_eq_zero_iff <| (countedSequence_finite _ _).image _).2 this, condCount,
         cond_apply _ list_int_measurableSet, hint, count_injective_image List.cons_injective,
         count_countedSequence, count_countedSequence, one_mul, zero_mul, add_zero,
-        Nat.cast_add, Nat.cast_one]
-      · rw [mul_comm, ← div_eq_mul_inv, ENNReal.div_eq_div_iff]
-        · norm_cast
-          rw [mul_comm _ (p + 1), ← Nat.succ_eq_add_one p, Nat.succ_add, Nat.succ_mul_choose_eq,
-            mul_comm]
-        all_goals simp [(Nat.choose_pos <| (le_add_iff_nonneg_right _).2 zero_le').ne.symm]
+        Nat.cast_add, Nat.cast_one, mul_comm, ← div_eq_mul_inv, ENNReal.div_eq_div_iff]
+      · norm_cast
+        rw [mul_comm _ (p + 1), ← Nat.succ_eq_add_one p, Nat.succ_add, Nat.succ_mul_choose_eq,
+          mul_comm]
+      all_goals simp [(Nat.choose_pos <| (le_add_iff_nonneg_right _).2 zero_le').ne.symm]
     · simp
 #align ballot.first_vote_pos Ballot.first_vote_pos
 
@@ -394,11 +393,11 @@ theorem ballot_problem :
       ENNReal.toReal_sub_of_le, ENNReal.toReal_nat, ENNReal.toReal_nat]
     exacts [Nat.cast_le.2 qp.le, ENNReal.natCast_ne_top _]
   rwa [ENNReal.toReal_eq_toReal (measure_lt_top _ _).ne] at this
-  · simp only [Ne, ENNReal.div_eq_top, tsub_eq_zero_iff_le, Nat.cast_le, not_le,
-      add_eq_zero_iff, Nat.cast_eq_zero, ENNReal.add_eq_top, ENNReal.natCast_ne_top, or_self_iff,
-      not_false_iff, and_true_iff]
-    push_neg
-    exact ⟨fun _ _ => by linarith, (tsub_le_self.trans_lt (ENNReal.natCast_ne_top p).lt_top).ne⟩
+  simp only [Ne, ENNReal.div_eq_top, tsub_eq_zero_iff_le, Nat.cast_le, not_le,
+    add_eq_zero_iff, Nat.cast_eq_zero, ENNReal.add_eq_top, ENNReal.natCast_ne_top, or_self_iff,
+    not_false_iff, and_true_iff]
+  push_neg
+  exact ⟨fun _ _ => by linarith, (tsub_le_self.trans_lt (ENNReal.natCast_ne_top p).lt_top).ne⟩
 #align ballot.ballot_problem Ballot.ballot_problem
 
 end Ballot
diff --git a/Archive/Wiedijk100Theorems/FriendshipGraphs.lean b/Archive/Wiedijk100Theorems/FriendshipGraphs.lean
index 796e551654f30..396fc49722ff7 100644
--- a/Archive/Wiedijk100Theorems/FriendshipGraphs.lean
+++ b/Archive/Wiedijk100Theorems/FriendshipGraphs.lean
@@ -317,7 +317,7 @@ theorem existsPolitician_of_degree_le_two (hd : G.IsRegularOfDegree d) (h : d 
     ExistsPolitician G := by
   interval_cases d
   iterate 2 apply existsPolitician_of_degree_le_one hG hd; norm_num
-  · exact existsPolitician_of_degree_eq_two hG hd
+  exact existsPolitician_of_degree_eq_two hG hd
 #align theorems_100.friendship.exists_politician_of_degree_le_two Theorems100.Friendship.existsPolitician_of_degree_le_two
 
 end Friendship