chore(tactic/linarith): remove final linting error (#3196)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/tactic/linarith/lemmas.lean

@@ -58,8 +58,10 @@ neg_of_neg_pos (by simpa)
 
 lemma mul_nonpos {α} [ordered_ring α] {a b : α} (ha : a ≤ 0) (hb : b > 0) : b * a ≤ 0 :=
 have (-b)*a ≥ 0, from mul_nonneg_of_nonpos_of_nonpos (le_of_lt (neg_neg_of_pos hb)) ha,
-(by simpa)
+by simpa
 
+-- used alongside `mul_neg` and `mul_nonpos`, so has the same argument pattern for uniformity
+@[nolint unused_arguments]
 lemma mul_eq {α} [ordered_semiring α] {a b : α} (ha : a = 0) (hb : b > 0) : b * a = 0 :=
 by simp *