. apply nzero_mul_left_cancel 12 _ _ h12
  simp only [dweierstrass_dy, div_eq_mul_inv, mul_zero]
  rw [show
    12 * (2 * (-(-e.a1 * b2 e * 12⁻¹ + e.a3) * 2⁻¹) + e.a1 * (-b2 e * 12⁻¹) + e.a3)
    =
    (-(-e.a1 * b2 e * (12 * 12⁻¹) + 12 * e.a3) * (2 * 2⁻¹)) + e.a1 * (-b2 e * (12 * 12⁻¹)) + 12 * e.a3
    by ring]
  simp only [mul_inv_cancel h2, mul_inv_cancel h12, one_mul, mul_one]
  simp only [c6, b2, b4, b6]
  ring
case pos.h_3.refine_3
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
hc6 : c6 e = 0
x✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
h12 : 12 ≠ 0
⊢ dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0
no goals