[Merged by Bors] - chore: adapt to multiple goal linter 1

Mathlib/Algebra/GroupPower/Order.lean

@@ -436,7 +436,7 @@ protected lemma Even.add_pow_le (hn : ∃ k, 2 * k = n) :
         rw [Commute.mul_pow]; simp [Commute, SemiconjBy, two_mul, mul_two]
     _ ≤ 2 ^ n * (2 ^ (n - 1) * ((a ^ 2) ^ n + (b ^ 2) ^ n)) := mul_le_mul_of_nonneg_left
           (add_pow_le (sq_nonneg _) (sq_nonneg _) _) $ pow_nonneg (zero_le_two (α := R)) _
-    _ = _ := by simp only [← mul_assoc, ← pow_add, ← pow_mul]; cases n; rfl; simp [Nat.two_mul]
+    _ = _ := by simp only [← mul_assoc, ← pow_add, ← pow_mul]; cases n; (· rfl); simp [Nat.two_mul]
 
 end LinearOrderedSemiring
 

Mathlib/Algebra/Order/Group/Abs.lean

@@ -342,7 +342,7 @@ variable [LinearOrderedCommGroup α] {a b : α}
   obtain ha | ha := le_or_lt 1 a <;> obtain hb | hb := le_or_lt 1 b
   · simp [ha, hb, mabs_of_one_le, one_le_mul ha hb]
   · exact (lt_irrefl (1 : α) <| ha.trans_lt <| hab.trans_lt hb).elim
-  any_goals simp [ha.le, hb.le, mabs_of_le_one, mul_le_one', mul_comm]
+  on_goal 2 => simp [ha.le, hb.le, mabs_of_le_one, mul_le_one', mul_comm]
   have : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔
     (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1) := by
     simp [ha.le, ha.not_le, hb, mabs_of_le_one, mabs_of_one_le]

Mathlib/Algebra/Order/Group/Int.lean

@@ -411,8 +411,8 @@ theorem toNat_le_toNat {a b : ℤ} (h : a ≤ b) : toNat a ≤ toNat b := by
 #align int.to_nat_le_to_nat Int.toNat_le_toNat
 
 theorem toNat_lt_toNat {a b : ℤ} (hb : 0 < b) : toNat a < toNat b ↔ a < b :=
-  ⟨fun h => by cases a; exact lt_toNat.1 h; exact lt_trans (neg_of_sign_eq_neg_one rfl) hb,
-   fun h => by rw [lt_toNat]; cases a; exact h; exact hb⟩
+  ⟨fun h => by cases a; exacts [lt_toNat.1 h, lt_trans (neg_of_sign_eq_neg_one rfl) hb],
+   fun h => by rw [lt_toNat]; cases a; exacts [h, hb]⟩
 #align int.to_nat_lt_to_nat Int.toNat_lt_toNat
 
 theorem lt_of_toNat_lt {a b : ℤ} (h : toNat a < toNat b) : a < b :=

Mathlib/Algebra/Order/Group/MinMax.lean

@@ -85,10 +85,10 @@ variable {α : Type*} [LinearOrderedAddCommGroup α] {a b c : α}
 
 theorem max_sub_max_le_max (a b c d : α) : max a b - max c d ≤ max (a - c) (b - d) := by
   simp only [sub_le_iff_le_add, max_le_iff]; constructor
-  calc
+  · calc
     a = a - c + c := (sub_add_cancel a c).symm
     _ ≤ max (a - c) (b - d) + max c d := add_le_add (le_max_left _ _) (le_max_left _ _)
-  calc
+  · calc
     b = b - d + d := (sub_add_cancel b d).symm
     _ ≤ max (a - c) (b - d) + max c d := add_le_add (le_max_right _ _) (le_max_right _ _)
 #align max_sub_max_le_max max_sub_max_le_max

Mathlib/Algebra/Order/Sub/Defs.lean

@@ -389,9 +389,9 @@ variable [CovariantClass α α (· + ·) (· ≤ ·)] [ContravariantClass α α
 
 theorem add_tsub_add_eq_tsub_right (a c b : α) : a + c - (b + c) = a - b := by
   refine' add_tsub_add_le_tsub_right.antisymm (tsub_le_iff_right.2 <| le_of_add_le_add_right _)
-  exact c
-  rw [add_assoc]
-  exact le_tsub_add
+  · exact c
+  · rw [add_assoc]
+    exact le_tsub_add
 #align add_tsub_add_eq_tsub_right add_tsub_add_eq_tsub_right
 
 theorem add_tsub_add_eq_tsub_left (a b c : α) : a + b - (a + c) = b - c := by

Mathlib/AlgebraicGeometry/Gluing.lean

@@ -129,7 +129,7 @@ def gluedScheme : Scheme := by
   intro x
   obtain ⟨i, y, rfl⟩ := D.toLocallyRingedSpaceGlueData.ι_jointly_surjective x
   refine' ⟨_, _ ≫ D.toLocallyRingedSpaceGlueData.toGlueData.ι i, _⟩
-  swap; exact (D.U i).affineCover.map y
+  swap; · exact (D.U i).affineCover.map y
   constructor
   · dsimp [-Set.mem_range]
     rw [coe_comp, Set.range_comp]
@@ -329,8 +329,8 @@ theorem glued_cover_cocycle_snd (x y z : 𝒰.J) :
 theorem glued_cover_cocycle (x y z : 𝒰.J) :
     gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y = 𝟙 _ := by
   apply pullback.hom_ext <;> simp_rw [Category.id_comp, Category.assoc]
-  apply glued_cover_cocycle_fst
-  apply glued_cover_cocycle_snd
+  · apply glued_cover_cocycle_fst
+  · apply glued_cover_cocycle_snd
 #align algebraic_geometry.Scheme.open_cover.glued_cover_cocycle AlgebraicGeometry.Scheme.OpenCover.glued_cover_cocycle
 
 /-- The glue data associated with an open cover.
@@ -355,7 +355,7 @@ def gluedCover : Scheme.GlueData.{u} where
 This is an isomorphism, as witnessed by an `IsIso` instance. -/
 def fromGlued : 𝒰.gluedCover.glued ⟶ X := by
   fapply Multicoequalizer.desc
-  exact fun x => 𝒰.map x
+  · exact fun x => 𝒰.map x
   rintro ⟨x, y⟩
   change pullback.fst ≫ _ = ((pullbackSymmetry _ _).hom ≫ pullback.fst) ≫ _
   simpa using pullback.condition
@@ -453,7 +453,7 @@ def glueMorphisms {Y : Scheme} (f : ∀ x, 𝒰.obj x ⟶ Y)
     X ⟶ Y := by
   refine' inv 𝒰.fromGlued ≫ _
   fapply Multicoequalizer.desc
-  exact f
+  · exact f
   rintro ⟨i, j⟩
   change pullback.fst ≫ f i = (_ ≫ _) ≫ f j
   erw [pullbackSymmetry_hom_comp_fst]

Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean

@@ -350,8 +350,8 @@ theorem hasFDerivAt_of_tendstoUniformlyOnFilter [NeBot l]
   have : 𝓝 (0 : G) = 𝓝 (0 + 0 + 0) := by simp only [add_zero]
   rw [this]
   refine' Tendsto.add (Tendsto.add _ _) _
-  simp only
-  · have := difference_quotients_converge_uniformly hf' hf hfg
+  · simp only
+    have := difference_quotients_converge_uniformly hf' hf hfg
     rw [Metric.tendstoUniformlyOnFilter_iff] at this
     rw [Metric.tendsto_nhds]
     intro ε hε

Mathlib/Combinatorics/Quiver/Arborescence.lean

@@ -75,8 +75,8 @@ noncomputable def arborescenceMk {V : Type u} [Quiver V] (r : V) (height : V →
       have height_le : ∀ {a b}, Path a b → height a ≤ height b := by
         intro a b p
         induction' p with b c _ e ih
-        rfl
-        exact le_of_lt (lt_of_le_of_lt ih (height_lt e))
+        · rfl
+        · exact le_of_lt (lt_of_le_of_lt ih (height_lt e))
       suffices ∀ p q : Path r b, p = q by
         intro p
         apply this

Mathlib/Control/Fix.lean

@@ -91,9 +91,9 @@ protected theorem fix_def {x : α} (h' : ∃ i, (Fix.approx f i x).Dom) :
     congr
     ext x: 1
     rw [assert_neg]
-    rfl
-    rw [Nat.zero_add] at _this
-    simpa only [not_not, Coe]
+    · rfl
+    · rw [Nat.zero_add] at _this
+      simpa only [not_not, Coe]
   | succ n n_ih =>
     intro x'
     rw [Fix.approx, WellFounded.fix_eq, fixAux]

Mathlib/Data/Fin/Basic.lean

@@ -1592,12 +1592,12 @@ theorem coe_sub_one {n} (a : Fin (n + 1)) : ↑(a - 1) = if a = 0 then n else a
 @[simp]
 theorem lt_sub_one_iff {n : ℕ} {k : Fin (n + 2)} : k < k - 1 ↔ k = 0 := by
   rcases k with ⟨_ | k, hk⟩
-  simp only [zero_eq, zero_eta, zero_sub, lt_iff_val_lt_val, val_zero, coe_neg_one, add_pos_iff,
-    _root_.zero_lt_one, or_true]
-  have : (k + 1 + (n + 1)) % (n + 2) = k % (n + 2) := by
-    rw [add_right_comm, add_assoc, add_mod_right]
-  simp [lt_iff_val_lt_val, ext_iff, Fin.coe_sub, succ_eq_add_one, this,
-    mod_eq_of_lt ((lt_succ_self _).trans hk)]
+  · simp only [zero_eq, zero_eta, zero_sub, lt_iff_val_lt_val, val_zero, coe_neg_one, add_pos_iff,
+      _root_.zero_lt_one, or_true]
+  · have : (k + 1 + (n + 1)) % (n + 2) = k % (n + 2) := by
+      rw [add_right_comm, add_assoc, add_mod_right]
+    simp [lt_iff_val_lt_val, ext_iff, Fin.coe_sub, succ_eq_add_one, this,
+      mod_eq_of_lt ((lt_succ_self _).trans hk)]
 #align fin.lt_sub_one_iff Fin.lt_sub_one_iff
 
 @[simp]

Mathlib/Data/Int/Bitwise.lean

@@ -227,8 +227,8 @@ theorem bit1_val (n : ℤ) : bit1 n = 2 * n + 1 :=
 
 theorem bit_val (b n) : bit b n = 2 * n + cond b 1 0 := by
   cases b
-  apply (bit0_val n).trans (add_zero _).symm
-  apply bit1_val
+  · apply (bit0_val n).trans (add_zero _).symm
+  · apply bit1_val
 #align int.bit_val Int.bit_val
 
 theorem bit_decomp (n : ℤ) : bit (bodd n) (div2 n) = n :=
@@ -539,7 +539,7 @@ theorem shiftLeft_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), m <<< (n : ℤ) = m * (2
 theorem shiftRight_eq_div_pow : ∀ (m : ℤ) (n : ℕ), m >>> (n : ℤ) = m / (2 ^ n : ℕ)
   | (m : ℕ), n => by rw [shiftRight_coe_nat, Nat.shiftRight_eq_div_pow _ _]; simp
   | -[m+1], n => by
-    rw [shiftRight_negSucc, negSucc_ediv, Nat.shiftRight_eq_div_pow]; rfl
+    rw [shiftRight_negSucc, negSucc_ediv, Nat.shiftRight_eq_div_pow]; · rfl
     exact ofNat_lt_ofNat_of_lt (Nat.pow_pos (by decide))
 #align int.shiftr_eq_div_pow Int.shiftRight_eq_div_pow
 

Mathlib/Data/List/Basic.lean

@@ -636,8 +636,8 @@ theorem isEmpty_iff_eq_nil {l : List α} : l.isEmpty ↔ l = [] := by cases l <;
 theorem getLast_cons {a : α} {l : List α} :
     ∀ h : l ≠ nil, getLast (a :: l) (cons_ne_nil a l) = getLast l h := by
   induction l <;> intros
-  contradiction
-  rfl
+  · contradiction
+  · rfl
 #align list.last_cons List.getLast_cons
 
 theorem getLast_append_singleton {a : α} (l : List α) :
@@ -820,11 +820,11 @@ theorem mem_of_mem_head? {x : α} {l : List α} (h : x ∈ l.head?) : x ∈ l :=
 
 @[simp]
 theorem head!_append [Inhabited α] (t : List α) {s : List α} (h : s ≠ []) :
-    head! (s ++ t) = head! s := by induction s; contradiction; rfl
+    head! (s ++ t) = head! s := by induction s; (· contradiction); rfl
 #align list.head_append List.head!_append
 
 theorem head?_append {s t : List α} {x : α} (h : x ∈ s.head?) : x ∈ (s ++ t).head? := by
-  cases s; contradiction; exact h
+  cases s; (· contradiction); exact h
 #align list.head'_append List.head?_append
 
 theorem head?_append_of_ne_nil :
@@ -834,7 +834,7 @@ theorem head?_append_of_ne_nil :
 
 theorem tail_append_singleton_of_ne_nil {a : α} {l : List α} (h : l ≠ nil) :
     tail (l ++ [a]) = tail l ++ [a] := by
-  induction l; contradiction; rw [tail, cons_append, tail]
+  induction l; (· contradiction); rw [tail, cons_append, tail]
 #align list.tail_append_singleton_of_ne_nil List.tail_append_singleton_of_ne_nil
 
 theorem cons_head?_tail : ∀ {l : List α} {a : α}, a ∈ head? l → a :: tail l = l

Mathlib/Data/List/Chain.lean

@@ -419,8 +419,8 @@ theorem Chain.induction (p : α → Prop) (l : List α) (h : Chain r a l)
   · rw [chain_cons] at h
     simp only [mem_cons]
     rintro _ (rfl | H)
-    apply carries h.1 (l_ih h.2 hb _ (mem_cons.2 (Or.inl rfl)))
-    apply l_ih h.2 hb _ (mem_cons.2 H)
+    · apply carries h.1 (l_ih h.2 hb _ (mem_cons.2 (Or.inl rfl)))
+    · apply l_ih h.2 hb _ (mem_cons.2 H)
 #align list.chain.induction List.Chain.induction
 
 /-- Given a chain from `a` to `b`, and a predicate true at `b`, if `r x y → p y → p x` then

Mathlib/Data/List/Dedup.lean

@@ -43,9 +43,9 @@ theorem dedup_cons_of_not_mem' {a : α} {l : List α} (h : a ∉ dedup l) :
 @[simp]
 theorem mem_dedup {a : α} {l : List α} : a ∈ dedup l ↔ a ∈ l := by
   have := not_congr (@forall_mem_pwFilter α (· ≠ ·) _ ?_ a l)
-  simpa only [dedup, forall_mem_ne, not_not] using this
-  intros x y z xz
-  exact not_and_or.1 <| mt (fun h ↦ h.1.trans h.2) xz
+  · simpa only [dedup, forall_mem_ne, not_not] using this
+  · intros x y z xz
+    exact not_and_or.1 <| mt (fun h ↦ h.1.trans h.2) xz
 #align list.mem_dedup List.mem_dedup
 
 @[simp]

Mathlib/Data/List/MinMax.lean

@@ -218,7 +218,7 @@ theorem index_of_argmax :
     · cases not_le_of_lt ‹_› ‹_›
     · rw [if_pos rfl]
     · rw [if_neg, if_neg]
-      exact Nat.succ_le_succ (index_of_argmax h (by assumption) ham)
+      · exact Nat.succ_le_succ (index_of_argmax h (by assumption) ham)
       · exact ne_of_apply_ne f (lt_of_lt_of_le ‹_› ‹_›).ne
       · exact ne_of_apply_ne _ ‹f hd < f _›.ne
     · rw [if_pos rfl]
@@ -509,8 +509,8 @@ theorem le_max_of_le {l : List α} {a x : α} (hx : x ∈ l) (h : a ≤ x) : a 
   induction' l with y l IH
   · exact absurd hx (not_mem_nil _)
   · obtain hl | hl := hx
-    simp only [foldr, foldr_cons]
-    · exact le_max_of_le_left h
+    · simp only [foldr, foldr_cons]
+      exact le_max_of_le_left h
     · exact le_max_of_le_right (IH (by assumption))
 #align list.le_max_of_le List.le_max_of_le
 

Mathlib/Data/List/Perm.lean

@@ -845,9 +845,9 @@ theorem nodup_permutations'Aux_iff {s : List α} {x : α} : Nodup (permutations'
     · obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_lt H'
       erw [length_insertNth _ _ hk.le, Nat.succ_lt_succ_iff, Nat.succ_add] at hn
       rw [nthLe_insertNth_add_succ]
-      convert nthLe_insertNth_add_succ s x k m.succ (by simpa using hn) using 2
-      · simp [Nat.add_succ, Nat.succ_add]
-      · simp [Nat.add_left_comm, Nat.add_comm]
+      · convert nthLe_insertNth_add_succ s x k m.succ (by simpa using hn) using 2
+        · simp [Nat.add_succ, Nat.succ_add]
+        · simp [Nat.add_left_comm, Nat.add_comm]
       · simpa [Nat.succ_add] using hn
 #align list.nodup_permutations'_aux_iff List.nodup_permutations'Aux_iff
 

Mathlib/Data/List/Permutation.lean

@@ -95,15 +95,15 @@ theorem map_permutationsAux2' {α β α' β'} (g : α → α') (g' : β → β')
   · simp
   · simp only [map, permutationsAux2_snd_cons, cons_append, cons.injEq]
     rw [ys_ih, permutationsAux2_fst]
-    refine' ⟨_, rfl⟩
-    · simp only [← map_cons, ← map_append]; apply H
+    · refine' ⟨_, rfl⟩
+      simp only [← map_cons, ← map_append]; apply H
     · intro a; apply H
 #align list.map_permutations_aux2' List.map_permutationsAux2'
 
 /-- The `f` argument to `permutationsAux2` when `r = []` can be eliminated. -/
 theorem map_permutationsAux2 (t : α) (ts : List α) (ys : List α) (f : List α → β) :
     (permutationsAux2 t ts [] ys id).2.map f = (permutationsAux2 t ts [] ys f).2 := by
-  rw [map_permutationsAux2' id, map_id, map_id]; rfl
+  rw [map_permutationsAux2' id, map_id, map_id]; · rfl
   simp
 #align list.map_permutations_aux2 List.map_permutationsAux2
 

Mathlib/Data/List/Sublists.lean

@@ -84,9 +84,10 @@ theorem mem_sublists' {s t : List α} : s ∈ sublists' t ↔ s <+ t := by
   · simp only [sublists'_nil, mem_singleton]
     exact ⟨fun h => by rw [h], eq_nil_of_sublist_nil⟩
   simp only [sublists'_cons, mem_append, IH, mem_map]
-  constructor <;> intro h; rcases h with (h | ⟨s, h, rfl⟩)
-  · exact sublist_cons_of_sublist _ h
-  · exact h.cons_cons _
+  constructor <;> intro h
+  · rcases h with (h | ⟨s, h, rfl⟩)
+    · exact sublist_cons_of_sublist _ h
+    · exact h.cons_cons _
   · cases' h with _ _ _ h s _ _ h
     · exact Or.inl h
     · exact Or.inr ⟨s, h, rfl⟩

Mathlib/Data/List/Zip.lean

@@ -264,8 +264,8 @@ theorem get?_zip_with (f : α → β → γ) (l₁ : List α) (l₂ : List β) (
   induction' l₁ with head tail generalizing l₂ i
   · rw [zipWith] <;> simp
   · cases l₂
-    simp only [zipWith, Seq.seq, Functor.map, get?, Option.map_none']
-    · cases (head :: tail).get? i <;> rfl
+    · simp only [zipWith, Seq.seq, Functor.map, get?, Option.map_none']
+      cases (head :: tail).get? i <;> rfl
     · cases i <;> simp only [Option.map_some', get?, Option.some_bind', *]
 #align list.nth_zip_with List.get?_zip_with
 

Mathlib/Data/Nat/Bits.lean

@@ -149,8 +149,8 @@ lemma bit1_val (n : Nat) : bit1 n = 2 * n + 1 := congr_arg succ (bit0_val _)
 
 lemma bit_val (b n) : bit b n = 2 * n + cond b 1 0 := by
   cases b
-  apply bit0_val
-  apply bit1_val
+  · apply bit0_val
+  · apply bit1_val
 #align nat.bit_val Nat.bit_val
 
 lemma bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=

Mathlib/Data/Nat/Defs.lean

@@ -1197,7 +1197,7 @@ lemma dvd_sub_mod (k : ℕ) : n ∣ k - k % n :=
 
 lemma add_mod_eq_ite :
     (m + n) % k = if k ≤ m % k + n % k then m % k + n % k - k else m % k + n % k := by
-  cases k; simp only [zero_eq, mod_zero, zero_le, ↓reduceIte, Nat.sub_zero]
+  cases k; · simp
   rw [Nat.add_mod]
   split_ifs with h
   · rw [Nat.mod_eq_sub_mod h, Nat.mod_eq_of_lt]
@@ -1292,9 +1292,9 @@ set_option linter.deprecated false in
 protected theorem not_two_dvd_bit1 (n : ℕ) : ¬2 ∣ bit1 n := by
   rw [bit1, Nat.dvd_add_right, Nat.dvd_one]
   -- Porting note: was `cc`
-  decide
-  rw [bit0, ← Nat.two_mul]
-  exact Nat.dvd_mul_right _ _
+  · decide
+  · rw [bit0, ← Nat.two_mul]
+    exact Nat.dvd_mul_right _ _
 #align nat.not_two_dvd_bit1 Nat.not_two_dvd_bit1
 
 /-- A natural number `m` divides the sum `m + n` if and only if `m` divides `n`.-/

Mathlib/Data/Nat/PSub.lean

@@ -118,8 +118,8 @@ def psub' (m n : ℕ) : Option ℕ :=
 theorem psub'_eq_psub (m n) : psub' m n = psub m n := by
   rw [psub']
   split_ifs with h
-  exact (psub_eq_sub h).symm
-  exact (psub_eq_none.2 (not_le.1 h)).symm
+  · exact (psub_eq_sub h).symm
+  · exact (psub_eq_none.2 (not_le.1 h)).symm
 #align nat.psub'_eq_psub Nat.psub'_eq_psub
 
 end Nat

Mathlib/Data/Nat/WithBot.lean

@@ -26,35 +26,35 @@ instance : WellFoundedRelation (WithBot ℕ) where
 
 theorem add_eq_zero_iff {n m : WithBot ℕ} : n + m = 0 ↔ n = 0 ∧ m = 0 := by
   rcases n, m with ⟨_ | _, _ | _⟩
-  any_goals (exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩)
-  exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.2⟩
-  repeat' erw [WithBot.coe_eq_coe]
-  exact add_eq_zero_iff' (zero_le _) (zero_le _)
+  repeat (· exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.1⟩)
+  · exact ⟨fun h => Option.noConfusion h, fun h => Option.noConfusion h.2⟩
+  · repeat erw [WithBot.coe_eq_coe]
+    exact add_eq_zero_iff' (zero_le _) (zero_le _)
 #align nat.with_bot.add_eq_zero_iff Nat.WithBot.add_eq_zero_iff
 
 theorem add_eq_one_iff {n m : WithBot ℕ} : n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0 := by
   rcases n, m with ⟨_ | _, _ | _⟩
-  any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩;
+  repeat refine' ⟨fun h => Option.noConfusion h, fun h => _⟩;
               aesop (simp_config := { decide := true })
-  repeat' erw [WithBot.coe_eq_coe]
-  exact Nat.add_eq_one_iff
+  · repeat erw [WithBot.coe_eq_coe]
+    exact Nat.add_eq_one_iff
 #align nat.with_bot.add_eq_one_iff Nat.WithBot.add_eq_one_iff
 
 theorem add_eq_two_iff {n m : WithBot ℕ} :
     n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0 := by
   rcases n, m with ⟨_ | _, _ | _⟩
-  any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩;
+  repeat refine' ⟨fun h => Option.noConfusion h, fun h => _⟩;
               aesop (simp_config := { decide := true })
-  repeat' erw [WithBot.coe_eq_coe]
-  exact Nat.add_eq_two_iff
+  · repeat erw [WithBot.coe_eq_coe]
+    exact Nat.add_eq_two_iff
 #align nat.with_bot.add_eq_two_iff Nat.WithBot.add_eq_two_iff
 
 theorem add_eq_three_iff {n m : WithBot ℕ} :
     n + m = 3 ↔ n = 0 ∧ m = 3 ∨ n = 1 ∧ m = 2 ∨ n = 2 ∧ m = 1 ∨ n = 3 ∧ m = 0 := by
   rcases n, m with ⟨_ | _, _ | _⟩
-  any_goals refine' ⟨fun h => Option.noConfusion h, fun h => _⟩;
+  repeat refine' ⟨fun h => Option.noConfusion h, fun h => _⟩;
               aesop (simp_config := { decide := true })
-  repeat' erw [WithBot.coe_eq_coe]
+  repeat erw [WithBot.coe_eq_coe]
   exact Nat.add_eq_three_iff
 #align nat.with_bot.add_eq_three_iff Nat.WithBot.add_eq_three_iff