. rw [is_singular_point]
  refine ⟨?_, ?_, ?_⟩
  . rw [weierstrass]
    apply nzero_mul_left_cancel (e.c4 ^ 3) _ _ (pow_ne_zero _ hc4)
    rw [mul_zero]
    simp only [div_eq_mul_inv]
    rw [show c4 e ^ 3 * (((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) ^ 2 +
          e.a1 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) +
        e.a3 * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) -
        (((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 3 + e.a2 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 2 +
        e.a4 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) + e.a6)) =
      (c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * ((b2 e * b5 e + 3 * b7 e)) ^ 2 +
        c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a1 * ((18 * b6 e - b2 e * b4 e)) * ((b2 e * b5 e + 3 * b7 e)) +
      c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a3 * ((b2 e * b5 e + 3 * b7 e)) -
      (c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * ((18 * b6 e - b2 e * b4 e)) ^ 3 +
      c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a2 * ((18 * b6 e - b2 e * b4 e)) ^ 2 +
        c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a4 * ((18 * b6 e - b2 e * b4 e)) +
      c4 e * c4 e * c4 e * e.a6)) by ring]
    simp only [mul_inv_cancel hc4, one_mul]
    rw [b5, b7, c4, b2, b4, b6]
    rw [← mul_zero (e.a1^6 + 12*e.a1^4*e.a2 + 48*e.a1^2*e.a2^2 - 36*e.a1^3*e.a3 + 64*e.a2^3
      - 144*e.a1*e.a2*e.a3 - 72*e.a1^2*e.a4 + 216*e.a3^2 - 288*e.a2*e.a4 + 864*e.a6),
      ← h, discr_eq_neg_singular]
    ring
  . 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
  . rw [dweierstrass_dy]
    apply nzero_mul_left_cancel e.c4 _ _ hc4
    simp only [div_eq_mul_inv, mul_zero]
    rw [show c4 e * (2 * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹)
        + e.a1 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) + e.a3) =
      c4 e * (c4 e)⁻¹ * (2 * (b2 e * b5 e + 3 * b7 e)
      + e.a1 * ((18 * b6 e - b2 e * b4 e))) + c4 e * e.a3 by ring]
    simp only [mul_inv_cancel hc4, one_mul]
    rw [b5, b7, c4, b2, b4, b6]
    ring
case neg
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ is_singular_point e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e)
no goals