internlm/Lean-Github huggingface dataset:
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_1.refine_1
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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ e.a2 * e.a4 + e.a6 - (pth_root e.a4 * e.a4 + e.a2 * e.a4 + e.a4 * pth_root e.a4 + e.a6) = 0
Tactic:
ring_nf
Proof state after:
case pos.h_1.refine_1
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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ -(e.a4 * pth_root e.a4 * 2) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_1.refine_1
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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ -(e.a4 * pth_root e.a4 * 2) = 0
Tactic:
simp [hchar'']
Proof state after:
no goals
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ 3 = 2 + 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_1.refine_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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Tactic:
rw [dweierstrass_dx]
Proof state after:
case pos.h_1.refine_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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ e.a1 * (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).snd -
      (3 * (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).fst ^ 2 +
          2 * e.a2 * (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).fst +
        e.a4) =
    0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_1.refine_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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ e.a1 * (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).snd -
      (3 * (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).fst ^ 2 +
          2 * e.a2 * (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).fst +
        e.a4) =
    0
Tactic:
simp only [ha1, zero_mul, hchar'', add_zero, zero_sub, neg_add_rev]
Proof state after:
case pos.h_1.refine_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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ -e.a4 + -(3 * pth_root e.a4 ^ 2) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_1.refine_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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ -e.a4 + -(3 * pth_root e.a4 ^ 2) = 0
Tactic:
rw [← hchar, pth_root_pow_char hcharne, ← sub_eq_add_neg]
Proof state after:
case pos.h_1.refine_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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ -e.a4 - 3 * e.a4 = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_1.refine_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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ -e.a4 - 3 * e.a4 = 0
Tactic:
simp only [add_sub_add_right_eq_sub, sub_eq_iff_eq_add, zero_add]
Proof state after:
case pos.h_1.refine_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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ -e.a4 = 3 * e.a4
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_1.refine_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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ -e.a4 = 3 * e.a4
Tactic:
rw [show (3 : K) = 2 * 2 - 1 by norm_num]
Proof state after:
case pos.h_1.refine_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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ -e.a4 = (2 * 2 - 1) * e.a4
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_1.refine_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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ -e.a4 = (2 * 2 - 1) * e.a4
Tactic:
rw [hchar'']
Proof state after:
case pos.h_1.refine_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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ -e.a4 = (0 * 0 - 1) * e.a4
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_1.refine_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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ -e.a4 = (0 * 0 - 1) * e.a4
Tactic:
simp [← neg_mul_eq_neg_mul]
Proof state after:
no goals
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ 3 = 2 * 2 - 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_1.refine_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✝ : ℕ
heq✝ : ringChar K = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Tactic:
simp [dweierstrass_dy, ha1, ha3, hchar'']
Proof state after:
no goals
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)
Tactic:
rw [is_singular_point]
Proof state after:
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
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
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
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
Tactic:
have hchar : ringChar K = 3 := by assumption
Proof state after:
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
hchar : ringChar K = 3
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
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
hchar : ringChar K = 3
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
Tactic:
have hcharne : ringChar K ≠ 0 := by simp [hchar]
Proof state after:
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
Tactic:
have hchar' : (ringChar K : K) = 3 := by simp [hchar]
Proof state after:
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
Tactic:
have hchar'' : (3 : K) = 0 := by simp [← hchar', ringChar.Nat.cast_ringChar]
Proof state after:
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
Tactic:
have hb2 : e.b2 = 0 := by simpa [c4_zero_iff_b2_zero_of_char_three e hchar] using hc4
Proof state after:
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : b2 e = 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : b2 e = 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
Tactic:
have hb4 : e.b4 = 0 := b4_zero_of_b2_zero_of_disc_zero_of_char_three e hchar h hb2
Proof state after:
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : b2 e = 0
hb4 : b4 e = 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : b2 e = 0
hb4 : b4 e = 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
Tactic:
rw [b2] at hb2
Proof state after:
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : b4 e = 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : b4 e = 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
Tactic:
rw [b4] at hb4
Proof state after:
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : e.a1 * e.a3 + 2 * e.a4 = 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : e.a1 * e.a3 + 2 * e.a4 = 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
Tactic:
refine ⟨?_, ?_, ?_⟩
Proof state after:
case pos.h_2.refine_1
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : e.a1 * e.a3 + 2 * e.a4 = 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0

case pos.h_2.refine_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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : e.a1 * e.a3 + 2 * e.a4 = 0
⊢ dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0

case pos.h_2.refine_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✝ : ℕ
heq✝ : ringChar K = 3
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : e.a1 * e.a3 + 2 * e.a4 = 0
⊢ dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_2.refine_1
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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : e.a1 * e.a3 + 2 * e.a4 = 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0

case pos.h_2.refine_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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : e.a1 * e.a3 + 2 * e.a4 = 0
⊢ dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0

case pos.h_2.refine_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✝ : ℕ
heq✝ : ringChar K = 3
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : e.a1 * e.a3 + 2 * e.a4 = 0
⊢ dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
Tactic:
. 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
Proof state after:
case pos.h_2.refine_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
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : e.a1 * e.a3 + 2 * e.a4 = 0
⊢ dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0

case pos.h_2.refine_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✝ : ℕ
heq✝ : ringChar K = 3
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : e.a1 * e.a3 + 2 * e.a4 = 0
⊢ dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0