perf(tactic/lint/simp): speed up simp_comm linter (#2760)

This is a fairly unimportant linter, but takes 35% of the linting runtime in my unscientific small-case profiling run.

src/algebra/euclidean_domain.lean

@@ -204,7 +204,7 @@ using_well_founded {dec_tac := tactic.assumption,
 @[simp] theorem xgcd_zero_left {s t r' s' t' : α} : xgcd_aux 0 s t r' s' t' = (r', s', t') :=
 by unfold xgcd_aux; exact if_pos rfl
 
-@[simp] theorem xgcd_aux_rec {r s t r' s' t' : α} (h : r ≠ 0) :
+theorem xgcd_aux_rec {r s t r' s' t' : α} (h : r ≠ 0) :
   xgcd_aux r s t r' s' t' = xgcd_aux (r' % r) (s' - (r' / r) * s) (t' - (r' / r) * t) r s t :=
 by conv {to_lhs, rw [xgcd_aux]}; exact if_neg h
 

src/data/int/gcd.lean

@@ -32,7 +32,7 @@ def xgcd_aux : ℕ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ
 @[simp] theorem xgcd_zero_left {s t r' s' t'} : xgcd_aux 0 s t r' s' t' = (r', s', t') :=
 by simp [xgcd_aux]
 
-@[simp] theorem xgcd_aux_rec {r s t r' s' t'} (h : 0 < r) :
+theorem xgcd_aux_rec {r s t r' s' t'} (h : 0 < r) :
   xgcd_aux r s t r' s' t' = xgcd_aux (r' % r) (s' - (r' / r) * s) (t' - (r' / r) * t) r s t :=
 by cases r; [exact absurd h (lt_irrefl _), {simp only [xgcd_aux], refl}]
 
@@ -48,7 +48,7 @@ def gcd_b (x y : ℕ) : ℤ := (xgcd x y).2
 
 @[simp] theorem xgcd_aux_fst (x y) : ∀ s t s' t',
   (xgcd_aux x s t y s' t').1 = gcd x y :=
-gcd.induction x y (by simp) (λ x y h IH s t s' t', by simp [h, IH]; rw ← gcd_rec)
+gcd.induction x y (by simp) (λ x y h IH s t s' t', by simp [xgcd_aux_rec, h, IH]; rw ← gcd_rec)
 
 theorem xgcd_aux_val (x y) : xgcd_aux x 1 0 y 0 1 = (gcd x y, xgcd x y) :=
 by rw [xgcd, ← xgcd_aux_fst x y 1 0 0 1]; cases xgcd_aux x 1 0 y 0 1; refl

src/tactic/lint/simp.lean

@@ -188,10 +188,10 @@ tt ← is_valid_simp_lemma_cnst d.to_name | pure none,
 (lhs, rhs) ← simp_lhs_rhs d.type,
 if lhs.get_app_fn.const_name ≠ rhs.get_app_fn.const_name then pure none else do
 (lhs', rhs') ← (prod.snd <$> mk_meta_pis d.type) >>= simp_lhs_rhs,
-tt ← succeeds $ unify rhs' lhs transparency.reducible | pure none,
+tt ← succeeds $ unify rhs lhs' transparency.reducible | pure none,
 tt ← succeeds $ is_def_eq rhs lhs' transparency.reducible | pure none,
 -- ensure that the second application makes progress:
-ff ← succeeds $ is_def_eq lhs' rhs' transparency.reducible | pure none,
+ff ← succeeds $ unify lhs' rhs' transparency.reducible | pure none,
 pure $ "should not be marked simp"
 
 /-- A linter for commutativity lemmas that are marked simp. -/