chore: update std4 11-13 (#587)

The main work is cleaning up all the new linter warnings. Also turns on `warningAsError` globally, which in particular means that `sorry`s will break the build; you have to use `set_option warningAsError false` to locally disable this behavior when needed.

Author: digama0

Mathlib/Algebra/Group/Basic.lean

@@ -497,7 +497,7 @@ theorem mul_div_cancel'' (a b : G) : a * b / b = a :=
 
 @[simp, to_additive]
 theorem mul_div_mul_right_eq_div (a b c : G) : a * c / (b * c) = a / b := by
-  rw [div_mul_eq_div_div_swap] <;> simp only [mul_left_inj, eq_self_iff_true, mul_div_cancel'']
+  rw [div_mul_eq_div_div_swap]; simp only [mul_left_inj, eq_self_iff_true, mul_div_cancel'']
 
 @[to_additive eq_sub_of_add_eq]
 theorem eq_div_of_mul_eq' (h : a * c = b) : a = b / c := by simp [← h]
@@ -633,8 +633,8 @@ theorem div_eq_iff_eq_mul' : a / b = c ↔ a = b * c := by rw [div_eq_iff_eq_mul
 theorem mul_div_cancel''' (a b : G) : a * b / a = b := by rw [div_eq_inv_mul, inv_mul_cancel_left]
 
 @[simp, to_additive]
-theorem mul_div_cancel'_right (a b : G) : a * (b / a) = b :=
-  by rw [← mul_div_assoc, mul_div_cancel''']
+theorem mul_div_cancel'_right (a b : G) : a * (b / a) = b := by
+  rw [← mul_div_assoc, mul_div_cancel''']
 
 @[simp, to_additive sub_add_cancel']
 theorem div_mul_cancel'' (a b : G) : a / (a * b) = b⁻¹ := by rw [← inv_div, mul_div_cancel''']
@@ -643,24 +643,24 @@ theorem div_mul_cancel'' (a b : G) : a / (a * b) = b⁻¹ := by rw [← inv_div,
 -- along with the additive version `add_neg_cancel_comm_assoc`,
 -- defined  in `algebra/group/commute`
 @[to_additive]
-theorem mul_mul_inv_cancel'_right (a b : G) : a * (b * a⁻¹) = b :=
-  by rw [← div_eq_mul_inv, mul_div_cancel'_right a b]
+theorem mul_mul_inv_cancel'_right (a b : G) : a * (b * a⁻¹) = b := by
+  rw [← div_eq_mul_inv, mul_div_cancel'_right a b]
 
 @[simp, to_additive]
-theorem mul_mul_div_cancel (a b c : G) : a * c * (b / c) = a * b :=
-  by rw [mul_assoc, mul_div_cancel'_right]
+theorem mul_mul_div_cancel (a b c : G) : a * c * (b / c) = a * b := by
+  rw [mul_assoc, mul_div_cancel'_right]
 
 @[simp, to_additive]
-theorem div_mul_mul_cancel (a b c : G) : a / c * (b * c) = a * b :=
-  by rw [mul_left_comm, div_mul_cancel', mul_comm]
+theorem div_mul_mul_cancel (a b c : G) : a / c * (b * c) = a * b := by
+  rw [mul_left_comm, div_mul_cancel', mul_comm]
 
 @[simp, to_additive sub_add_sub_cancel']
-theorem div_mul_div_cancel'' (a b c : G) : a / b * (c / a) = c / b :=
-  by rw [mul_comm] <;> apply div_mul_div_cancel'
+theorem div_mul_div_cancel'' (a b c : G) : a / b * (c / a) = c / b := by
+  rw [mul_comm]; apply div_mul_div_cancel'
 
 @[simp, to_additive]
-theorem mul_div_div_cancel (a b c : G) : a * b / (a / c) = b * c :=
-  by rw [← div_mul, mul_div_cancel''']
+theorem mul_div_div_cancel (a b c : G) : a * b / (a / c) = b * c := by
+  rw [← div_mul, mul_div_cancel''']
 
 @[simp, to_additive]
 theorem div_div_div_cancel_left (a b c : G) : c / a / (c / b) = b / a := by

Mathlib/Algebra/Ring/Basic.lean

@@ -60,7 +60,7 @@ lemma Nat.cast_pow [Semiring R] {m n : ℕ} : (m ^ n).cast = (m.cast ^ n : R) :=
 theorem Nat.cast_commute [Semiring α] (n : ℕ) (x : α) : Commute (↑n) x := by
   induction n with
   | zero => rw [Nat.cast_zero]; exact Commute.zero_left x
-  | succ n ihn => rw [Nat.cast_succ] <;> exact ihn.add_left (Commute.one_left x)
+  | succ n ihn => rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)
 
 end Semiring
 

Mathlib/Data/Fin/Basic.lean

@@ -28,7 +28,7 @@ lemma Fin.size_positive' [Nonempty (Fin n)] : 0 < n :=
 
 @[simp]
 protected theorem Fin.eta (a : Fin n) (h : (a : ℕ) < n) : (⟨(a : ℕ), h⟩ : Fin n) = a := by
-  cases a <;> rfl
+  cases a; rfl
 
 lemma zero_lt_of_lt {a : Nat} : ∀ {x : Nat}, x < a -> 0 < a
 | 0, h   => h

Mathlib/Data/FunLike/Basic.lean

@@ -157,7 +157,7 @@ theorem coe_injective : Function.Injective (fun f : F => (f : ∀ a : α, β a))
 
 @[simp]
 theorem coe_fn_eq {f g : F} : (f : ∀ a : α, β a) = (g : ∀ a : α, β a) ↔ f = g :=
-  ⟨fun h => FunLike.coe_injective' h, fun h => by cases h <;> rfl⟩
+  ⟨fun h => FunLike.coe_injective' h, fun h => by cases h; rfl⟩
 
 theorem ext' {f g : F} (h : (f : ∀ a : α, β a) = (g : ∀ a : α, β a)) : f = g :=
   FunLike.coe_injective' h

Mathlib/Data/List/Basic.lean

@@ -250,10 +250,10 @@ theorem pmap_map {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β) (l H)
 
 theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) :
     pmap f l H = l.attach.map fun x => f x.1 (H _ x.2) := by
-  rw [attach, map_pmap] <;> exact pmap_congr l fun _ _ _ _ => rfl
+  rw [attach, map_pmap]; exact pmap_congr l fun _ _ _ _ => rfl
 
 theorem attach_map_val (l : List α) : l.attach.map Subtype.val = l := by
-  rw [attach, map_pmap] <;> exact (pmap_eq_map _ _ _ _).trans (map_id l)
+  rw [attach, map_pmap]; exact (pmap_eq_map ..).trans (map_id l)
 
 @[simp]
 theorem mem_attach (l : List α) : ∀ x, x ∈ l.attach

Mathlib/Data/List/Pairwise.lean

@@ -17,7 +17,7 @@ theorem pairwise_append_comm (s : Symmetric R) {l₁ l₂ : List α} :
     Pairwise R (l₁ ++ l₂) ↔ Pairwise R (l₂ ++ l₁) := by
   have : ∀ l₁ l₂ : List α, (∀ x : α, x ∈ l₁ → ∀ y : α, y ∈ l₂ → R x y) →
     ∀ x : α, x ∈ l₂ → ∀ y : α, y ∈ l₁ → R x y := fun l₁ l₂ a x xm y ym => s (a y ym x xm)
-  simp only [pairwise_append, and_left_comm] <;> rw [Iff.intro (this l₁ l₂) (this l₂ l₁)]
+  simp only [pairwise_append, and_left_comm]; rw [Iff.intro (this l₁ l₂) (this l₂ l₁)]
 
 theorem pairwise_middle (s : Symmetric R) {a : α} {l₁ l₂ : List α} :
     Pairwise R (l₁ ++ a :: l₂) ↔ Pairwise R (a :: (l₁ ++ l₂)) :=

Mathlib/Data/List/Range.lean

@@ -32,8 +32,7 @@ theorem mem_range' {m : ℕ} : ∀ {s n : ℕ}, m ∈ range' s n ↔ s ≤ m ∧
     have l : m = s ∨ s + 1 ≤ m ↔ s ≤ m := by
       simpa only [eq_comm] using (@Decidable.le_iff_eq_or_lt _ _ _ s m).symm
     mem_cons.trans <| by
-      simp only [mem_range', or_and_left, or_iff_right_of_imp this, l, Nat.add_right_comm]
-        <;> rfl
+      simp only [mem_range', or_and_left, or_iff_right_of_imp this, l, Nat.add_right_comm]; rfl
 
 theorem rangeAux_range' : ∀ s n : ℕ, rangeAux s (range' s n) = range' 0 (n + s)
   | 0, n => rfl

Mathlib/Data/Option/Basic.lean

@@ -273,7 +273,7 @@ theorem getD_default_eq_iget [Inhabited α] (o : Option α) :
 @[simp]
 theorem guard_eq_some' {p : Prop} [Decidable p] (u) : _root_.guard p = some u ↔ p := by
   cases u
-  by_cases p <;> simp [_root_.guard, h] <;> first |rfl|contradiction
+  by_cases p <;> simp [_root_.guard, h]
 
 theorem liftOrGet_choice {f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b = b) :
     ∀ o₁ o₂, liftOrGet f o₁ o₂ = o₁ ∨ liftOrGet f o₁ o₂ = o₂

Mathlib/Data/Prod/Basic.lean

@@ -180,7 +180,7 @@ theorem Lex_def (r : α → α → Prop) (s : β → β → Prop) {p q : α × 
   ⟨fun h => by cases h <;> simp [*], fun h =>
     match p, q, h with
     | (a, b), (c, d), Or.inl h => Lex.left _ _ h
-    | (a, b), (c, d), Or.inr ⟨e, h⟩ => by subst e <;> exact Lex.right _ h⟩
+    | (a, b), (c, d), Or.inr ⟨e, h⟩ => by subst e; exact Lex.right _ h⟩
 
 instance Lex.decidable [DecidableEq α]
     (r : α → α → Prop) (s : β → β → Prop) [DecidableRel r] [DecidableRel s] :

Mathlib/Init/CcLemmas.lean

@@ -49,16 +49,16 @@ theorem or_eq_of_eq {a b : Prop} (h : a = b) : (a ∨ b) = a :=
   h ▸ propext or_self_iff
 
 theorem imp_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a → b) = b :=
-  h.symm ▸ propext (Iff.intro (fun h => h trivial) fun h₁ _ => h₁)
+  h.symm ▸ propext ⟨fun h => h trivial, fun h₁ _ => h₁⟩
 
 theorem imp_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a → b) = True :=
-  h.symm ▸ propext (Iff.intro (fun h => trivial) fun h₁ _ => h₁)
+  h.symm ▸ propext ⟨fun _ => trivial, fun h₁ _ => h₁⟩
 
 theorem imp_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a → b) = True :=
-  h.symm ▸ propext (Iff.intro (fun h => trivial) fun _ h₂ => False.elim h₂)
+  h.symm ▸ propext ⟨fun _ => trivial, fun _ h₂ => False.elim h₂⟩
 
 theorem imp_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a → b) = Not a :=
-  h.symm ▸ propext (Iff.intro (fun h => h) fun hna ha => hna ha)
+  h.symm ▸ propext ⟨fun h => h, fun hna ha => hna ha⟩
 
 /- Remark: the congruence closure module will only use the following lemma is
    cc_config.em is tt. -/
@@ -67,7 +67,7 @@ theorem not_imp_eq_of_eq_false_right {a b : Prop} (h : b = False) : (Not a → b
     fun h' => Classical.byContradiction fun hna => h' hna) fun ha hna => hna ha)
 
 theorem imp_eq_true_of_eq {a b : Prop} (h : a = b) : (a → b) = True :=
-  h ▸ propext (Iff.intro (fun _ => trivial) fun _ ha => ha)
+  h ▸ propext ⟨fun _ => trivial, fun _ ha => ha⟩
 
 theorem not_eq_of_eq_true {a : Prop} (h : a = True) : Not a = False :=
   h.symm ▸ propext not_true