unused argument linter

Author: kim-em

Mathlib/Data/Nat/Order/Basic.lean

@@ -323,7 +323,7 @@ theorem diag_induction (P : ℕ → ℕ → Prop) (ha : ∀ a, P (a + 1) (a + 1)
     have _ : a + (b + 1) < (a + 1) + (b + 1) := by simp
     apply diag_induction P ha hb hd a (b + 1)
     apply lt_of_le_of_lt (Nat.le_succ _) h
-  termination_by a b c => a + b
+  termination_by a b => a + b
   decreasing_by all_goals assumption
 #align nat.diag_induction Nat.diag_induction