chore: update std 05-22 (#4248)

The main breaking change is that `tac <;> [t1, t2]` is now written `tac <;> [t1; t2]`, to avoid clashing with tactics like `cases` and `use` that take comma-separated lists.

Author: digama0

Mathlib/Algebra/EuclideanDomain/Basic.lean

@@ -143,7 +143,7 @@ theorem gcd_zero_right (a : R) : gcd a 0 = a := by
 
 theorem gcd_val (a b : R) : gcd a b = gcd (b % a) a := by
   rw [gcd]
-  split_ifs with h <;> [simp only [h, mod_zero, gcd_zero_right], rfl]
+  split_ifs with h <;> [simp only [h, mod_zero, gcd_zero_right]; rfl]
 #align euclidean_domain.gcd_val EuclideanDomain.gcd_val
 
 theorem gcd_dvd (a b : R) : gcd a b ∣ a ∧ gcd a b ∣ b :=

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -730,7 +730,7 @@ theorem lcm_eq_zero_iff [GCDMonoid α] (a b : α) : lcm a b = 0 ↔ a = 0 ∨ b
     (fun h : lcm a b = 0 => by
       have : Associated (a * b) 0 := (gcd_mul_lcm a b).symm.trans <| by rw [h, mul_zero]
       rwa [← mul_eq_zero, ← associated_zero_iff_eq_zero])
-    (by rintro (rfl | rfl) <;> [apply lcm_zero_left, apply lcm_zero_right])
+    (by rintro (rfl | rfl) <;> [apply lcm_zero_left; apply lcm_zero_right])
 #align lcm_eq_zero_iff lcm_eq_zero_iff
 
 -- Porting note: lower priority to avoid linter complaints about simp-normal form

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -501,7 +501,7 @@ theorem WithBot.coe_nsmul [AddMonoid A] (a : A) (n : ℕ) : ↑(n • a) = n •
 #align with_bot.coe_nsmul WithBot.coe_nsmul
 
 theorem nsmul_eq_mul' [NonAssocSemiring R] (a : R) (n : ℕ) : n • a = a * n := by
-  induction' n with n ih <;> [rw [zero_nsmul, Nat.cast_zero, mul_zero],
+  induction' n with n ih <;> [rw [zero_nsmul, Nat.cast_zero, mul_zero];
     rw [succ_nsmul', ih, Nat.cast_succ, mul_add, mul_one]]
 #align nsmul_eq_mul' nsmul_eq_mul'ₓ
 -- typeclasses do not match up exactly.
@@ -548,7 +548,7 @@ theorem Int.coe_nat_pow (n m : ℕ) : ((n ^ m : ℕ) : ℤ) = (n : ℤ) ^ m := b
 #align int.coe_nat_pow Int.coe_nat_pow
 
 theorem Int.natAbs_pow (n : ℤ) (k : ℕ) : Int.natAbs (n ^ k) = Int.natAbs n ^ k := by
-  induction' k with k ih <;> [rfl, rw [pow_succ', Int.natAbs_mul, pow_succ', ih]]
+  induction' k with k ih <;> [rfl; rw [pow_succ', Int.natAbs_mul, pow_succ', ih]]
 #align int.nat_abs_pow Int.natAbs_pow
 
 section bit0_bit1

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -177,12 +177,12 @@ theorem mul_right_inj' (ha : a ≠ 0) : a * b = a * c ↔ b = c :=
 
 @[simp]
 theorem mul_eq_mul_right_iff : a * c = b * c ↔ a = b ∨ c = 0 := by
-  by_cases hc : c = 0 <;> [simp [hc], simp [mul_left_inj', hc]]
+  by_cases hc : c = 0 <;> [simp [hc]; simp [mul_left_inj', hc]]
 #align mul_eq_mul_right_iff mul_eq_mul_right_iff
 
 @[simp]
 theorem mul_eq_mul_left_iff : a * b = a * c ↔ b = c ∨ a = 0 := by
-  by_cases ha : a = 0 <;> [simp [ha], simp [mul_right_inj', ha]]
+  by_cases ha : a = 0 <;> [simp [ha]; simp [mul_right_inj', ha]]
 #align mul_eq_mul_left_iff mul_eq_mul_left_iff
 
 theorem mul_right_eq_self₀ : a * b = a ↔ b = 1 ∨ a = 0 :=

Mathlib/Algebra/Order/Floor.lean

@@ -1410,7 +1410,7 @@ theorem abs_sub_round_eq_min (x : α) : |x - round x| = min (fract x) (1 - fract
 
 theorem round_le (x : α) (z : ℤ) : |x - round x| ≤ |x - z| := by
   rw [abs_sub_round_eq_min, min_le_iff]
-  rcases le_or_lt (z : α) x with (hx | hx) <;> [left, right]
+  rcases le_or_lt (z : α) x with (hx | hx) <;> [left; right]
   · conv_rhs => rw [abs_eq_self.mpr (sub_nonneg.mpr hx), ← fract_add_floor x, add_sub_assoc]
     simpa only [le_add_iff_nonneg_right, sub_nonneg, cast_le] using le_floor.mpr hx
   · rw [abs_eq_neg_self.mpr (sub_neg.mpr hx).le]

Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

@@ -138,7 +138,7 @@ def transReflReparamAux (t : I) : ℝ :=
 @[continuity]
 theorem continuous_transReflReparamAux : Continuous transReflReparamAux := by
   refine' continuous_if_le _ _ (Continuous.continuousOn _) (Continuous.continuousOn _) _ <;>
-    [continuity, continuity, continuity, continuity, skip]
+    [continuity; continuity; continuity; continuity; skip]
   intro x hx
   -- Porting note: norm_num ignores arguments.
   simp [hx]
@@ -203,7 +203,7 @@ theorem continuous_transAssocReparamAux : Continuous transAssocReparamAux := by
   refine' continuous_if_le _ _ (Continuous.continuousOn _)
       (continuous_if_le _ _ (Continuous.continuousOn _) (Continuous.continuousOn _) _).continuousOn
       _ <;>
-    [continuity, continuity, continuity, continuity, continuity, continuity, continuity, skip,
+    [continuity; continuity; continuity; continuity; continuity; continuity; continuity; skip;
       skip] <;>
     · intro x hx
       -- Porting note: norm_num ignores arguments.

Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

@@ -197,7 +197,7 @@ variable {α β : Type _} [NormedField β] {t u v w : α → β} {l : Filter α}
 theorem isEquivalent_iff_exists_eq_mul :
     u ~[l] v ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v := by
   rw [IsEquivalent, isLittleO_iff_exists_eq_mul]
-  constructor <;> rintro ⟨φ, hφ, h⟩ <;> [refine' ⟨φ + 1, _, _⟩, refine' ⟨φ - 1, _, _⟩]
+  constructor <;> rintro ⟨φ, hφ, h⟩ <;> [refine' ⟨φ + 1, _, _⟩; refine' ⟨φ - 1, _, _⟩]
   · conv in 𝓝 _ => rw [← zero_add (1 : β)]
     exact hφ.add tendsto_const_nhds
   · convert h.add (EventuallyEq.refl l v) <;> simp [add_mul]

Mathlib/Analysis/BoxIntegral/Partition/Split.lean

@@ -206,7 +206,7 @@ theorem split_of_not_mem_Ioo (h : x ∉ Ioo (I.lower i) (I.upper i)) : split I i
   rcases mem_top.1 hJ with rfl; clear hJ
   rw [mem_boxes, mem_split_iff]
   rw [mem_Ioo, not_and_or, not_lt, not_lt] at h
-  cases h <;> [right, left]
+  cases h <;> [right; left]
   · rwa [eq_comm, Box.splitUpper_eq_self]
   · rwa [eq_comm, Box.splitLower_eq_self]
 #align box_integral.prepartition.split_of_not_mem_Ioo BoxIntegral.Prepartition.split_of_not_mem_Ioo
@@ -230,7 +230,7 @@ theorem restrict_split (h : I ≤ J) (i : ι) (x : ℝ) : (split J i x).restrict
   refine' ((isPartitionSplit J i x).restrict h).eq_of_boxes_subset _
   simp only [Finset.subset_iff, mem_boxes, mem_restrict', exists_prop, mem_split_iff']
   have : ∀ s, (I ∩ s : Set (ι → ℝ)) ⊆ J := fun s => (inter_subset_left _ _).trans h
-  rintro J₁ ⟨J₂, H₂ | H₂, H₁⟩ <;> [left, right] <;>
+  rintro J₁ ⟨J₂, H₂ | H₂, H₁⟩ <;> [left; right] <;>
     simp [H₁, H₂, inter_left_comm (I : Set (ι → ℝ)), this]
 #align box_integral.prepartition.restrict_split BoxIntegral.Prepartition.restrict_split
 

Mathlib/Analysis/Convex/Slope.lean

@@ -37,13 +37,13 @@ theorem ConvexOn.slope_mono_adjacent (hf : ConvexOn 𝕜 s f) {x y z : 𝕜} (hx
   set b := (y - x) / (z - x)
   have hy : a • x + b • z = y := by
     field_simp
-    rw [div_eq_iff] <;> [ring, linarith]
+    rw [div_eq_iff] <;> [ring; linarith]
   have key :=
     hf.2 hx hz (show 0 ≤ a by apply div_nonneg <;> linarith)
       (show 0 ≤ b by apply div_nonneg <;> linarith)
       (show a + b = 1 by
         field_simp
-        rw [div_eq_iff] <;> [ring, linarith])
+        rw [div_eq_iff] <;> [ring; linarith])
   rw [hy] at key
   replace key := mul_le_mul_of_nonneg_left key hxz.le
   field_simp [hxy.ne', hyz.ne', hxz.ne', mul_comm (z - x) _]  at key⊢
@@ -77,12 +77,12 @@ theorem StrictConvexOn.slope_strict_mono_adjacent (hf : StrictConvexOn 𝕜 s f)
   set b := (y - x) / (z - x)
   have hy : a • x + b • z = y := by
     field_simp
-    rw [div_eq_iff] <;> [ring, linarith]
+    rw [div_eq_iff] <;> [ring; linarith]
   have key :=
     hf.2 hx hz hxz' (div_pos hyz hxz) (div_pos hxy hxz)
       (show a + b = 1 by
         field_simp
-        rw [div_eq_iff] <;> [ring, linarith])
+        rw [div_eq_iff] <;> [ring; linarith])
   rw [hy] at key
   replace key := mul_lt_mul_of_pos_left key hxz
   field_simp [hxy.ne', hyz.ne', hxz.ne', mul_comm (z - x) _]  at key⊢

Mathlib/Analysis/Convex/Strict.lean

@@ -163,7 +163,7 @@ variable [TopologicalSpace β] [LinearOrderedCancelAddCommMonoid β] [OrderTopol
 protected theorem Set.OrdConnected.strictConvex {s : Set β} (hs : OrdConnected s) :
     StrictConvex 𝕜 s := by
   refine' strictConvex_iff_openSegment_subset.2 fun x hx y hy hxy => _
-  cases' hxy.lt_or_lt with hlt hlt <;> [skip, rw [openSegment_symm]] <;>
+  cases' hxy.lt_or_lt with hlt hlt <;> [skip; rw [openSegment_symm]] <;>
     exact
       (openSegment_subset_Ioo hlt).trans
         (isOpen_Ioo.subset_interior_iff.2 <| Ioo_subset_Icc_self.trans <| hs.out ‹_› ‹_›)