Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos
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
    (match ringChar K with
    | 2 => (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6))
    | 3 => (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3)
    | x => (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2))

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)
Tactic:
. have hc6 : c6 e = 0 := by
    simpa [h, hc4, pow_succ, mul_eq_zero] using discr_identity e
  split
  . rw [is_singular_point]
    have hchar : ringChar K = 2 := by assumption
    have hchar' : (ringChar K : K) = 2 := by simp [hchar]
    have hchar'' : (2 : K) = 0 := by simp [← hchar', ringChar.Nat.cast_ringChar]
    have hcharne : ringChar K ≠ 0 := by simp [hchar]
    have ha1 : e.a1 = 0 := by simpa [c4_zero_iff_a1_zero_of_char_two e hchar] using hc4
    have ha3 : e.a3 = 0 := a3_zero_of_a1_zero_of_disc_zero_of_char_two e hchar h ha1
    refine ⟨?_, ?_, ?_⟩
    . rw [weierstrass]
      simp only [ha1, ha3, mul_zero, zero_add, zero_mul, add_zero]
      rw [show 3 = 2 + 1 by norm_num]
      rw [pow_succ _ 2]
      rw [← hchar, pth_root_pow_char hcharne]
      rw [pth_root_pow_char hcharne]
      ring_nf
      simp [hchar'']
    . rw [dweierstrass_dx]
      simp only [ha1, zero_mul, hchar'', add_zero, zero_sub, neg_add_rev]
      rw [← hchar, pth_root_pow_char hcharne, ← sub_eq_add_neg]
      simp only [add_sub_add_right_eq_sub, sub_eq_iff_eq_add, zero_add]
      rw [show (3 : K) = 2 * 2 - 1 by norm_num]
      rw [hchar'']
      simp [← neg_mul_eq_neg_mul]
    . simp [dweierstrass_dy, ha1, ha3, hchar'']
  . rw [is_singular_point]
    have hchar : ringChar K = 3 := by assumption
    have hcharne : ringChar K ≠ 0 := by simp [hchar]
    have hchar' : (ringChar K : K) = 3 := by simp [hchar]
    have hchar'' : (3 : K) = 0 := by simp [← hchar', ringChar.Nat.cast_ringChar]
    have hb2 : e.b2 = 0 := by simpa [c4_zero_iff_b2_zero_of_char_three e hchar] using hc4
    have hb4 : e.b4 = 0 := b4_zero_of_b2_zero_of_disc_zero_of_char_three e hchar h hb2
    rw [b2] at hb2 rw [b4] at hb4
    refine ⟨?_, ?_, ?_⟩
    . rw [weierstrass]
      rw [← hchar, pth_root_pow_char hcharne]
      simp only
      rw [show
        (e.a1 * pth_root (-(e.a3 ^ 2) - e.a6) + e.a3) ^ 2 +
        e.a1 * pth_root (-(e.a3 ^ 2) - e.a6) * (e.a1 * pth_root (-(e.a3 ^ 2) - e.a6) + e.a3) +
        e.a3 * (e.a1 * pth_root (-(e.a3 ^ 2) - e.a6) + e.a3) -
        (-(e.a3 ^ 2) - e.a6 + e.a2 * pth_root (-(e.a3 ^ 2) - e.a6) ^ 2 + e.a4 * pth_root (-(e.a3 ^ 2) - e.a6) + e.a6) =
        (2 * e.a1 ^ 2 - e.a2) * pth_root (-(e.a3 ^ 2) - e.a6) ^ 2 +
        (4 * e.a1 * e.a3 - e.a4) * pth_root (-(e.a3 ^ 2) - e.a6) +
        3 * e.a3 ^ 2
        by ring]
      rw [show 2 * e.a1 ^ 2 - e.a2 = 0 from ?_]
      rw [show 4 * e.a1 * e.a3 - e.a4 = 0 from ?_]
      simp only [zero_mul, add_zero, hchar'']
      . rw [show (2 : K) = -1 by rw [← add_zero (-1), ← hchar'']; norm_num] at hb4
        rw [show (4 : K) = 1 by rw [← add_zero 1, ← hchar'']; norm_num]
        simp only [neg_mul, one_mul] at hb4
        simp [sub_eq_add_neg, hb4]
      . linear_combination (norm := ring_nf <;> simp [hchar'']) -hb2
    . rw [dweierstrass_dx]
      rw [hchar'', zero_mul, zero_add]
      simp only
      rw [show e.a1 * (e.a1 * pth_root (-(e.a3 ^ 2) - e.a6) + e.a3) - (2 * e.a2 * pth_root (-(e.a3 ^ 2) - e.a6) + e.a4) =
               (e.a1 * e.a1 - 2 * e.a2) * pth_root (-(e.a3 ^ 2) - e.a6) + (e.a1 * e.a3 - e.a4)
        by ring]
      rw [show (2 : K) = -1 by rw [← add_zero (-1), ← hchar'']; norm_num] at hb4
      rw [show (4 : K) = -2 by rw [← add_zero (-2), ← zero_mul (2 : K), ← hchar'']; norm_num] at hb2
      simp only [neg_mul, one_mul, ← sub_eq_add_neg] at hb4 hb2
      rw [hb4, hb2, zero_mul, zero_add]
    . rw [dweierstrass_dy]
      simp only
      rw [show 2 * (e.a1 * pth_root (-(e.a3 ^ 2) - e.a6) + e.a3)
          + e.a1 * pth_root (- (e.a3 ^ 2) - e.a6) + e.a3 = 3 * ((e.a1 * pth_root (-(e.a3 ^ 2) - e.a6)) + e.a3) by ring]
      rw [hchar'', zero_mul]
  . 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
Proof state after:
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)