Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_2
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✝ : ℕ
heq✝ : ringChar K = 3
⊢ is_singular_point e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3)

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)
Tactic:
. 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]
Proof state after:
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)