chore: fix linter warnings in tests (#662)

Author: digama0

lean_packages/manifest.json

@@ -21,7 +21,7 @@
    "name": "Unicode",
    "inputRev": "main"},
   {"url": "https://github.com/leanprover/std4",
-   "rev": "4261f9bcb56ada27ad9307beaf8c4dba5a0a6883",
+   "rev": "eb43042ebfebcc111ccd1986d3f7615cdf986a0d",
    "name": "std",
    "inputRev": "main"},
   {"url": "https://github.com/leanprover/lake",

test/Clear!.lean

@@ -1,7 +1,7 @@
 import Mathlib.Tactic.Clear!
 
 -- Most basic test
-example (delete_this : Nat) (delete_this_dep : delete_this = delete_this) : Nat := by
+example (delete_this : Nat) (_delete_this_dep : delete_this = delete_this) : Nat := by
   clear! delete_this
   fail_if_success assumption
   exact 0
@@ -13,7 +13,7 @@ example [delete_this : Inhabited Nat] : Inhabited Nat := by
   infer_instance
 
 -- Confirms clear! can clear the dependencies of multiple hypotheses
-example (delete_this : Nat) (delete_this2 : Nat) (delete_this_dep : delete_this = delete_this2) : Nat := by
+example (delete_this : Nat) (delete_this2 : Nat) (_delete_this_dep : delete_this = delete_this2) : Nat := by
   clear! delete_this delete_this2
   fail_if_success assumption
   exact 0

test/ClearExcept.lean

@@ -1,7 +1,7 @@
 import Mathlib.Tactic.ClearExcept
 
 -- Most basic test
-example (delete_this : Nat) (dont_delete_this : Int) : Nat := by
+example (_delete_this : Nat) (dont_delete_this : Int) : Nat := by
   clear * - dont_delete_this
   fail_if_success assumption
   exact dont_delete_this.toNat
@@ -12,7 +12,7 @@ example [dont_delete_this : Inhabited Nat] (dont_delete_this2 : Prop) : Inhabite
   assumption
 
 -- Confirms that clearExcept can clear hypotheses even when they have dependencies
-example (delete_this : Nat) (delete_this2 : delete_this = delete_this) (dont_delete_this : Int) : Nat := by
+example (delete_this : Nat) (_delete_this2 : delete_this = delete_this) (dont_delete_this : Int) : Nat := by
   clear * - dont_delete_this
   fail_if_success assumption
   exact dont_delete_this.toNat
@@ -23,7 +23,7 @@ example (dont_delete_this : Nat) (dont_delete_this2 : dont_delete_this = dont_de
   exact dont_delete_this
 
 -- Confirms that clearExcept can preserve multiple identifiers
-example (delete_this : Nat) (dont_delete_this : Int) (dont_delete_this2 : Int) : Nat := by
+example (_delete_this : Nat) (dont_delete_this : Int) (dont_delete_this2 : Int) : Nat := by
   clear * - dont_delete_this dont_delete_this2
   fail_if_success assumption
   exact dont_delete_this.toNat + dont_delete_this2.toNat

test/Clear_.lean

@@ -24,7 +24,6 @@ example (_delete_this : Type) (_delete_this_dep : _delete_this) (_delete_this_rw
   clear_
   fail_if_success
     rw [← _delete_this_rw]
-    assumption
   exact 0
 
 -- Confirms that clear_ does not clear hypotheses when they have dependencies that should not be cleared

test/Have.lean

@@ -26,20 +26,20 @@ example {a : Nat} : a = a := by
   exact this
 
 example : True := by
-  (let N) -- FIXME: lean4#1670
+  (let _N) -- FIXME: lean4#1670
   exact Nat
   have
   · exact 0
-  have h : Nat
+  have _h : Nat
   · exact 5
-  have h' x : x < x + 1
+  have _h' x : x < x + 1
   · exact Nat.lt.base x
-  have h'' (x : Nat) : x < x + 1
+  have _h'' (x : Nat) : x < x + 1
   · exact Nat.lt.base x
-  let m
+  let _m
   · exact 6
-  let m' x (y : Nat) : x + y = y + x
+  let _m' x (y : Nat) : x + y = y + x
   rw [Nat.add_comm]
-  have q
+  have _q
   · exact 6
   simp

test/PermuteGoals.lean

@@ -17,11 +17,11 @@ example (p q r : Prop) : p → q → r → p ∧ q ∧ r := by
 example (p q r : Prop) : p → q → r → p ∧ q ∧ r := by
   intros a b c
   constructor
-  fail_if_success on_goal -3 => exact a
+  fail_if_success on_goal -3 => unreachable!
   fail_if_success on_goal -1 => exact a
-  fail_if_success on_goal 0 => exact a
+  fail_if_success on_goal 0 => unreachable!
   fail_if_success on_goal 2 => exact a
-  fail_if_success on_goal 3 => exact a
+  fail_if_success on_goal 3 => unreachable!
   on_goal 1 => exact a
   constructor
   swap

test/Replace.lean

@@ -5,7 +5,9 @@ Authors: Arthur Paulino
 -/
 import Mathlib.Tactic.Replace
 
--- tests with a explicitly named hipothesis
+set_option linter.unusedVariables false
+
+-- tests with a explicitly named hypothesis
 
 example (h : Int) : Nat := by
   replace h : Nat := 0

test/Set.lean

@@ -19,7 +19,7 @@ example (x : Nat) (h : x + x - x = 3) : x + x - x = 3 := by
   guard_hyp w := x
   guard_hyp h : w + w - w = 3
   guard_hyp h2 : w = y
-  set z := w with h3
+  set z := w with _h3
   set a := 3
   guard_target = z + z - z = a
   set i'm_the_goal : Prop := z + z - z = a
@@ -28,6 +28,6 @@ example (x : Nat) (h : x + x - x = 3) : x + x - x = 3 := by
 
 example (x : Nat) (h : x - x = 0) : x = x := by
   set y : Nat := x
-  set! z := y + 1 with ← eq1
-  set! p : x - x = 0 := h with eq2
+  set! z := y + 1 with ← _eq1
+  set! p : x - x = 0 := h with _eq2
   rfl

test/Simps.lean

@@ -124,12 +124,12 @@ example (n : ℕ) : foo.rfl.invFun n = n := by rw [foo.rfl_invFun]
 -- note: in Lean 4 the first test succeeds without `@[simps]`, however, the remaining tests don't
 example : foo.1 = 1 := by simp
 example {a : ℕ} {h : 1 = a} : foo.1 = a := by rw [foo_fst, h]
-example {a : ℕ} {h : 1 = a} : foo.1 = a := by simp <;> rw [h]
-example {a : ℤ} {h : 2 = a} : foo.2 = a := by simp <;> rw [h]
-example {a : ℕ} {h : 1 = a} : foo.1 = a := by dsimp <;> rw [h] -- check that dsimp also unfolds
-example {a : ℤ} {h : 2 = a} : foo.2 = a := by dsimp <;> rw [h]
-example {α} (x y : α) (h : x = y) : foo.rfl.toFun x = y := by simp <;> rw [h]
-example {α} (x y : α) (h : x = y) : foo.rfl.invFun x = y := by simp <;> rw [h]
+example {a : ℕ} {h : 1 = a} : foo.1 = a := by simp; rw [h]
+example {a : ℤ} {h : 2 = a} : foo.2 = a := by simp; rw [h]
+example {a : ℕ} {h : 1 = a} : foo.1 = a := by dsimp; rw [h] -- check that dsimp also unfolds
+example {a : ℤ} {h : 2 = a} : foo.2 = a := by dsimp; rw [h]
+example {α} (x y : α) (h : x = y) : foo.rfl.toFun x = y := by simp; rw [h]
+example {α} (x y : α) (h : x = y) : foo.rfl.invFun x = y := by simp; rw [h]
 -- example {α} (x y : α) (h : x = y) : foo.rfl.toFun = @id α := by { successIfFail {simp}, rfl }
 
 /- check some failures -/
@@ -367,8 +367,8 @@ example {α} {b : Bool} {x} (h : (⟨3, 5⟩ : MyProd _ _) = x) : (@test α).ext
 @[simps (config := {simpRhs := true})] def Equiv'.trans {α β γ} (f : α ≃ β) (g : β ≃ γ) : α ≃ γ :=
 ⟨ g.toFun ∘ f.toFun,
   f.invFun ∘ g.invFun,
-  (by intro x <;> simp [Equiv'.left_inv _ _]),
-  (by intro x <;> simp [Equiv'.right_inv _ _])⟩
+  (by intro x; simp [Equiv'.left_inv _ _]),
+  (by intro x; simp [Equiv'.right_inv _ _])⟩
 
 
 example {α β γ : Type} (f : α ≃ β) (g : β ≃ γ) (x : α) {z : γ} (h : g.toFun (f.toFun x) = z) :
@@ -378,13 +378,13 @@ example {α β γ : Type} (f : α ≃ β) (g : β ≃ γ) (x : α) {z : γ} (h :
 
 attribute [local simp] Nat.zero_add Nat.one_mul Nat.mul_one
 @[simps (config := {simpRhs := true})] def myNatEquiv : ℕ ≃ ℕ :=
-⟨λ n => 0 + n, λ n => 1 * n * 1, by intro n <;> simp, by intro n <;> simp⟩
+⟨λ n => 0 + n, λ n => 1 * n * 1, by intro n; simp, by intro n; simp⟩
 
 example (n : ℕ) : myNatEquiv.toFun (myNatEquiv.toFun $ myNatEquiv.invFun n) = n :=
 by { /-successIfFail { rfl },-/ simp only [myNatEquiv_toFun, myNatEquiv_invFun] }
 
 @[simps (config := {simpRhs := true})] def succeed_without_simplification_possible : ℕ ≃ ℕ :=
-⟨λ n => n, λ n => n, by intro n <;> rfl, by intro n <;> rfl⟩
+⟨λ n => n, λ n => n, by intro n; rfl, by intro n; rfl⟩
 
 
 /- test that we don't recursively take projections of `prod` and `PProd` -/
@@ -437,10 +437,10 @@ infixr:80 " ≫ " => CategoryStruct.comp -- type as \gg
 
 @[ext] theorem types.ext {X Y : Type u} {f g : X ⟶ Y} : (∀ x, f x = g x) → f = g := funext
 
-example (X : Type u) {x : Type u} (h : (X → X) = x) : (X ⟶ X) = x := by simp <;> rw [h]
-example (X : Type u) {f : X → X} (h : ∀ x, f x = x) : 𝟙 X = f := by ext <;> simp <;> rw [h]
+example (X : Type u) {x : Type u} (h : (X → X) = x) : (X ⟶ X) = x := by simp; rw [h]
+example (X : Type u) {f : X → X} (h : ∀ x, f x = x) : 𝟙 X = f := by ext; simp; rw [h]
 example (X Y Z : Type u) (f : X ⟶ Y) (g : Y ⟶ Z) {k : X → Z} (h : ∀ x, g (f x) = k x) :
-  f ≫ g = k := by ext <;> simp <;> rw [h]
+  f ≫ g = k := by ext; simp; rw [h]
 
 namespace coercing
 
@@ -453,8 +453,8 @@ instance : CoeSort FooStr Type := ⟨FooStr.c⟩
 @[simps] def foo : FooStr := ⟨ℕ, 3⟩
 @[simps] def foo2 : FooStr := ⟨ℕ, 34⟩
 
-example {x : Type} (h : ℕ = x) : foo = x := by simp only [foo_c] <;> rw [h]
-example {x : ℕ} (h : (3 : ℕ) = x) : foo.x = x := by simp only [foo_x] <;> rw [h]
+example {x : Type} (h : ℕ = x) : foo = x := by simp only [foo_c]; rw [h]
+example {x : ℕ} (h : (3 : ℕ) = x) : foo.x = x := by simp only [foo_x]; rw [h]
 
 structure VooStr (n : ℕ) :=
  (c : Type)
@@ -465,8 +465,8 @@ instance (n : ℕ) : CoeSort (VooStr n) Type := ⟨VooStr.c⟩
 @[simps] def voo : VooStr 7 := ⟨ℕ, 3⟩
 @[simps] def voo2 : VooStr 4 := ⟨ℕ, 34⟩
 
-example {x : Type} (h : ℕ = x) : voo = x := by simp only [voo_c] <;> rw [h]
-example {x : ℕ} (h : (3 : ℕ) = x) : voo.x = x := by simp only [voo_x] <;> rw [h]
+example {x : Type} (h : ℕ = x) : voo = x := by simp only [voo_c]; rw [h]
+example {x : ℕ} (h : (3 : ℕ) = x) : voo.x = x := by simp only [voo_x]; rw [h]
 
 structure Equiv2 (α : Sort _) (β : Sort _) :=
 (toFun    : α → β)
@@ -480,8 +480,8 @@ instance {α β} : CoeFun (Equiv2 α β) (λ _ => α → β) := ⟨Equiv2.toFun
 ⟨λ x => x, λ x => x, λ _ => rfl, λ _ => rfl⟩
 
 example {α} (x x' : α) (h : x = x') : coercing.rfl2 x = x' := by rw [coercing.rfl2_toFun, h]
-example {α} (x x' : α) (h : x = x') : coercing.rfl2 x = x' := by simp <;> rw [h]
-example {α} (x x' : α) (h : x = x') : coercing.rfl2.invFun x = x' := by simp <;> rw [h]
+example {α} (x x' : α) (h : x = x') : coercing.rfl2 x = x' := by simp; rw [h]
+example {α} (x x' : α) (h : x = x') : coercing.rfl2.invFun x = x' := by simp; rw [h]
 
 @[simps] protected def Equiv2.symm {α β} (f : Equiv2 α β) : Equiv2 β α :=
 ⟨f.invFun, f, f.right_inv, f.left_inv⟩
@@ -492,12 +492,12 @@ example {α} (x x' : α) (h : x = x') : coercing.rfl2.invFun x = x' := by simp <
 @[simps (config := {fullyApplied := false})] protected def Equiv2.symm3 {α β} (f : Equiv2 α β) : Equiv2 β α :=
 ⟨f.invFun, f, f.right_inv, f.left_inv⟩
 
-example {α β} (f : Equiv2 α β) (y : β) {x} (h : f.invFun y = x) : f.symm y = x := by simp <;> rw [h]
-example {α β} (f : Equiv2 α β) (x : α) {z} (h : f x = z) : f.symm.invFun x = z := by simp <;> rw [h]
+example {α β} (f : Equiv2 α β) (y : β) {x} (h : f.invFun y = x) : f.symm y = x := by simp; rw [h]
+example {α β} (f : Equiv2 α β) (x : α) {z} (h : f x = z) : f.symm.invFun x = z := by simp; rw [h]
 
 -- example {α β} (f : Equiv2 α β) {x} (h : f = x) : f.symm.invFun = x :=
 -- by { /-successIfFail {simp <;> rw [h]} <;>-/ rfl }
-example {α β} (f : Equiv2 α β) {x} (h : f = x) : f.symm3.invFun = x := by simp <;> rw [h]
+example {α β} (f : Equiv2 α β) {x} (h : f = x) : f.symm3.invFun = x := by simp; rw [h]
 
 class Semigroup (G : Type u) extends Mul G where
   mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)
@@ -587,7 +587,7 @@ protected def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
 
 example (e₁ : α ≃ β) (e₂ : β ≃ γ) (x : γ) {z} (h : e₁.symm (e₂.symm x) = z) :
   (e₁.trans e₂).symm x = z :=
-by simp only [Equiv.trans_invFun] <;> rw [h]
+by simp only [Equiv.trans_invFun]; rw [h]
 
 end ManualCoercion
 
@@ -641,7 +641,7 @@ protected def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
 
 example (e₁ : α ≃ β) (e₂ : β ≃ γ) (x : γ) {z} (h : e₁.symm (e₂.symm x) = z) :
   (e₁.trans e₂).symm x = z :=
-by simp only [Equiv.trans_invFun] <;> rw [h]
+by simp only [Equiv.trans_invFun]; rw [h]
 
 end ManualInitialize
 
@@ -725,11 +725,11 @@ protected def Equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
 ⟨e₂ ∘ (e₁ : α → β), e₁.symm ∘ (e₂.symm : γ → β)⟩
 
 example (e₁ : α ≃ β) (e₂ : β ≃ γ) (x : α) {z} (h : e₂ (e₁ x) = z) : (e₁.trans e₂) x = z :=
-by simp only [Equiv.trans_apply] <;> rw [h]
+by simp only [Equiv.trans_apply]; rw [h]
 
 example (e₁ : α ≃ β) (e₂ : β ≃ γ) (x : γ) {z} (h : e₁.symm (e₂.symm x) = z) :
   (e₁.trans e₂).symm x = z :=
-by simp only [Equiv.trans_symm_apply] <;> rw [h]
+by simp only [Equiv.trans_symm_apply]; rw [h]
 
 -- the new projection names are parsed correctly (the old projection names won't work anymore)
 @[simps apply symm_apply] protected def Equiv.trans2 (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
@@ -1110,8 +1110,7 @@ initialize_simps_projections OneMore
   Q_toFun  := λ y => ⟨y, rfl⟩
   Q_invFun := λ y => ⟨y, rfl⟩ }
 
-example {α : Type} (x : α) : (fffoo α).symm x = x :=
-by dsimp <;> guard_target = x = x <;> rfl
+example {α : Type} (x : α) : (fffoo α).symm x = x := by dsimp
 
 @[simps apply to_dequiv_apply toFurtherDecoratedEquiv_apply to_dequiv]
 def fffoo2 (α : Type) : OneMore α α := fffoo α

test/SolveByElim.lean

@@ -9,14 +9,14 @@ example (h : Nat) : Nat := by solve_by_elim
 example {α β : Type} (f : α → β) (a : α) : β := by solve_by_elim
 example {α β : Type} (f : α → α → β) (a : α) : β := by solve_by_elim
 example {α β γ : Type} (f : α → β) (g : β → γ) (a : α) : γ := by solve_by_elim
-example {α β γ : Type} (f : α → β) (g : β → γ) (b : β) : γ := by solve_by_elim
+example {α β γ : Type} (_f : α → β) (g : β → γ) (b : β) : γ := by solve_by_elim
 example {α : Nat → Type} (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 5 := by solve_by_elim
 
 example (h : Nat) : Nat := by solve_by_elim []
 example {α β : Type} (f : α → β) (a : α) : β := by solve_by_elim []
 example {α β : Type} (f : α → α → β) (a : α) : β := by solve_by_elim []
 example {α β γ : Type} (f : α → β) (g : β → γ) (a : α) : γ := by solve_by_elim []
-example {α β γ : Type} (f : α → β) (g : β → γ) (b : β) : γ := by solve_by_elim []
+example {α β γ : Type} (_f : α → β) (g : β → γ) (b : β) : γ := by solve_by_elim []
 example {α : Nat → Type} (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 5 := by solve_by_elim []
 
 example {α β : Type} (f : α → β) (a : α) : β := by
@@ -27,12 +27,13 @@ example (h : Nat) : Nat := by solve_by_elim only [h]
 example {α β : Type} (f : α → β) (a : α) : β := by solve_by_elim only [f, a]
 example {α β : Type} (f : α → α → β) (a : α) : β := by solve_by_elim only [f, a]
 example {α β γ : Type} (f : α → β) (g : β → γ) (a : α) : γ := by solve_by_elim only [f, g, a]
-example {α β γ : Type} (f : α → β) (g : β → γ) (b : β) : γ := by solve_by_elim only [g, b]
-example {α : Nat → Type} (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 5 := by solve_by_elim only [f, a]
+example {α β γ : Type} (_f : α → β) (g : β → γ) (b : β) : γ := by solve_by_elim only [g, b]
+example {α : Nat → Type} (f : (n : Nat) → α n → α (n+1)) (a : α 0) : α 5 := by
+  solve_by_elim only [f, a]
 
 -- Verify that already assigned metavariables are skipped.
-example (P₁ P₂: α → Prop) (f: forall (a: α), P₁ a → P₂ a → β)
-        (a: α) (ha₁: P₁ a) (ha₂ : P₂ a) : β := by
+example (P₁ P₂ : α → Prop) (f : ∀ (a : α), P₁ a → P₂ a → β)
+    (a : α) (ha₁ : P₁ a) (ha₂ : P₂ a) : β := by
   solve_by_elim
 
 example {X : Type} (x : X) : x = x := by
@@ -41,16 +42,16 @@ example {X : Type} (x : X) : x = x := by
 
 -- Needs to apply `rfl` twice, with different implicit arguments each time.
 -- A naive implementation of solve_by_elim would get stuck.
-example {X : Type} (x y : X) (p : Prop) (h: x = x → y = y → p) : p := by solve_by_elim
+example {X : Type} (x y : X) (p : Prop) (h : x = x → y = y → p) : p := by solve_by_elim
 
 example : True := by
   fail_if_success solve_by_elim only -- needs the `trivial` lemma
   solve_by_elim
 
 -- Requires backtracking.
-example (P₁ P₂: α → Prop) (f: forall (a: α), P₁ a → P₂ a → β)
-        (a: α) (ha₁: P₁ a)
-        (a': α) (ha'₁: P₁ a') (ha'₂: P₂ a'): β := by
+example (P₁ P₂ : α → Prop) (f : ∀ (a: α), P₁ a → P₂ a → β)
+    (a : α) (_ha₁ : P₁ a)
+    (a' : α) (ha'₁ : P₁ a') (ha'₂ : P₂ a') : β := by
   solve_by_elim
 
 -- TODO this works in mathlib3 but not here yet, for some reason.