. rw [dweierstrass_dx]
  apply nzero_mul_left_cancel (e.c4 ^ 2) _ _ (pow_ne_zero _ hc4)
  rw [mul_zero, pow_two]
  simp only [div_eq_mul_inv]
  rw [show c4 e * c4 e *
    (e.a1 * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) -
      (3 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 2
      + 2 * e.a2 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) + e.a4)) =
      c4 e * (c4 e)⁻¹ * c4 e * (e.a1 * (b2 e * b5 e + 3 * b7 e)
      - 2 * e.a2 * ((18 * b6 e - b2 e * b4 e)))
      - c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ *
      3 * (18 * b6 e - b2 e * b4 e) ^ 2 - e.a4 * c4 e * c4 e
    by ring]
  simp only [mul_inv_cancel hc4, one_mul]
  rw [b5, b7, c4, b2, b4, b6]
  rw [← mul_zero (36 : K), ← h, discr_eq_neg_singular]
  ring
case neg.refine_2
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ dweierstrass_dx e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0

case neg.refine_3
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ dweierstrass_dy e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0
case neg.refine_3
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ dweierstrass_dy e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0