. rename_i hn2 hn3
  rw [is_singular_point]
  have h2 : (2 : K) ≠ 0 := fun hh => hn2 (ringChar_eq_of_Prime hh (by norm_num))
  have h3 : (3 : K) ≠ 0 := fun hh => hn3 (ringChar_eq_of_Prime hh (by norm_num))
  have h12 : (12 : K) ≠ 0 := by
    rw [show (12 : K) = 2 * 2 * 3 by norm_num]
    repeat' apply mul_ne_zero
    all_goals assumption
  refine ⟨?_, ?_, ?_⟩
  . apply nzero_mul_left_cancel (12 ^ 3) _ _ (pow_ne_zero _ h12)
    simp only [weierstrass, div_eq_mul_inv, mul_zero]
    rw [show
      12 ^ 3 * ((-(-e.a1 * b2 e * 12⁻¹ + e.a3) * 2⁻¹) ^ 2 +
      e.a1 * (-b2 e * 12⁻¹) * (-(-e.a1 * b2 e * 12⁻¹ + e.a3) * 2⁻¹) +
      e.a3 * (-(-e.a1 * b2 e * 12⁻¹ + e.a3) * 2⁻¹) -
      ((-b2 e * 12⁻¹) ^ 3 + e.a2 * (-b2 e * 12⁻¹) ^ 2 + e.a4 * (-b2 e * 12⁻¹) + e.a6)) =
      3*(-(-e.a1 * b2 e * (12 * 12⁻¹) + 12 * e.a3) * (2 * 2⁻¹)) ^ 2 +
      e.a1 * (-b2 e * (12 * 12⁻¹)) * (-(-e.a1 * b2 e * (12 * 12⁻¹) + 12 * e.a3) * (6 * (2 * 2⁻¹))) +
      12 * e.a3 * (-(-e.a1 * b2 e * (12 * 12⁻¹) + 12 * e.a3) * (6 * (2 * 2⁻¹))) -
      ((-b2 e * (12 * 12⁻¹)) ^ 3 + 12 * e.a2 * (-b2 e * (12 * 12⁻¹)) ^ 2 + 12 ^ 2 * e.a4 * (-b2 e * (12 * 12⁻¹)) + 12 ^ 3 * e.a6) by ring]
    simp only [mul_inv_cancel h2, mul_inv_cancel h12, one_mul, mul_one]
    rw [← mul_zero (2 : K), ← hc6]
    simp only [c6, b2, b4, b6]
    ring
  . apply nzero_mul_left_cancel (12 ^ 2) _ _ (pow_ne_zero _ h12)
    simp only [dweierstrass_dx, div_eq_mul_inv, mul_zero]
    rw [show
      12 ^ 2 * (e.a1 * (-(-e.a1 * b2 e * 12⁻¹ + e.a3) * 2⁻¹) - (3 * (-b2 e * 12⁻¹) ^ 2 + 2 * e.a2 * (-b2 e * 12⁻¹) + e.a4))
      =
      e.a1 * (-(-e.a1 * b2 e * (12 * 12⁻¹) + 12* e.a3) * 6 * (2 * 2⁻¹)) - (3 * (-b2 e * (12 * 12⁻¹)) ^ 2 + 24 * e.a2 * (-b2 e * (12 * 12⁻¹)) + 144 * e.a4)
      by ring]
    simp only [mul_inv_cancel h2, mul_inv_cancel h12, one_mul, mul_one]
    rw [← mul_zero (3 : K), ← hc4]
    simp only [c4, c6, b2, b4, b6]
    ring
  . 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
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✝² : ℕ
x✝¹ : ringChar K = 2 → False
x✝ : ringChar K = 3 → False
⊢ is_singular_point e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2)
no goals