chore(tactic/cancel_denoms): remove an unused have (#14269)

leanprover-community · May 21, 2022 · eaa771f · eaa771f
1 parent d787d49
commit eaa771f
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/src/tactic/cancel_denoms.lean b/src/tactic/cancel_denoms.lean
@@ -32,7 +32,6 @@ namespace cancel_factors
 
 lemma mul_subst {α} [comm_ring α] {n1 n2 k e1 e2 t1 t2 : α} (h1 : n1 * e1 = t1) (h2 : n2 * e2 = t2)
      (h3 : n1*n2 = k) : k * (e1 * e2) = t1 * t2 :=
-have h3 : n1 * n2 = k, from h3,
 by rw [←h3, mul_comm n1, mul_assoc n2, ←mul_assoc n1, h1, ←mul_assoc n2, mul_comm n2, mul_assoc, h2]
 
 lemma div_subst {α} [field α] {n1 n2 k e1 e2 t1 : α} (h1 : n1 * e1 = t1) (h2 : n2 / e2 = 1)