internlm/Lean-Github huggingface dataset:
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 = 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 + -1 * e.a4 = 0
⊢ 4 = 1 + 3
Tactic:
norm_num
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 = 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
⊢ 2 * e.a1 ^ 2 - e.a2 = 0
Tactic:
linear_combination (norm := ring_nf <;> simp [hchar'']) -hb2
Proof state after:
no goals
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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
Tactic:
rw [dweierstrass_dx]
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
⊢ e.a1 * (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3).snd -
      (3 * (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3).fst ^ 2 +
          2 * e.a2 * (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3).fst +
        e.a4) =
    0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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
⊢ e.a1 * (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3).snd -
      (3 * (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3).fst ^ 2 +
          2 * e.a2 * (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3).fst +
        e.a4) =
    0
Tactic:
rw [hchar'', zero_mul, zero_add]
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
⊢ e.a1 * (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3).snd -
      (2 * e.a2 * (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3).fst + e.a4) =
    0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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
⊢ e.a1 * (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3).snd -
      (2 * e.a2 * (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3).fst + e.a4) =
    0
Tactic:
simp only
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
⊢ 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) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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
⊢ 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) = 0
Tactic:
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]
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
⊢ (e.a1 * e.a1 - 2 * e.a2) * pth_root (-e.a3 ^ 2 - e.a6) + (e.a1 * e.a3 - e.a4) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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
⊢ (e.a1 * e.a1 - 2 * e.a2) * pth_root (-e.a3 ^ 2 - e.a6) + (e.a1 * e.a3 - e.a4) = 0
Tactic:
rw [show (2 : K) = -1 by rw [← add_zero (-1), ← hchar'']; norm_num] at hb4
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 + -1 * e.a4 = 0
⊢ (e.a1 * e.a1 - 2 * e.a2) * pth_root (-e.a3 ^ 2 - e.a6) + (e.a1 * e.a3 - e.a4) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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 + -1 * e.a4 = 0
⊢ (e.a1 * e.a1 - 2 * e.a2) * pth_root (-e.a3 ^ 2 - e.a6) + (e.a1 * e.a3 - e.a4) = 0
Tactic:
rw [show (4 : K) = -2 by rw [← add_zero (-2), ← zero_mul (2 : K), ← hchar'']; norm_num] at 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 + -2 * e.a2 = 0
hb4 : e.a1 * e.a3 + -1 * e.a4 = 0
⊢ (e.a1 * e.a1 - 2 * e.a2) * pth_root (-e.a3 ^ 2 - e.a6) + (e.a1 * e.a3 - e.a4) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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 + -2 * e.a2 = 0
hb4 : e.a1 * e.a3 + -1 * e.a4 = 0
⊢ (e.a1 * e.a1 - 2 * e.a2) * pth_root (-e.a3 ^ 2 - e.a6) + (e.a1 * e.a3 - e.a4) = 0
Tactic:
simp only [neg_mul, one_mul, ← sub_eq_add_neg] at hb4 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
hb4 : e.a1 * e.a3 - e.a4 = 0
hb2 : e.a1 * e.a1 - 2 * e.a2 = 0
⊢ (e.a1 * e.a1 - 2 * e.a2) * pth_root (-e.a3 ^ 2 - e.a6) + (e.a1 * e.a3 - e.a4) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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
hb4 : e.a1 * e.a3 - e.a4 = 0
hb2 : e.a1 * e.a1 - 2 * e.a2 = 0
⊢ (e.a1 * e.a1 - 2 * e.a2) * pth_root (-e.a3 ^ 2 - e.a6) + (e.a1 * e.a3 - e.a4) = 0
Tactic:
rw [hb4, hb2, zero_mul, zero_add]
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 = 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
⊢ 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)
Tactic:
ring
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 = 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 + -1 * e.a4 = 0
⊢ 4 = -2
Tactic:
rw [← add_zero (-2), ← zero_mul (2 : K), ← hchar'']
Proof state after:
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 + -1 * e.a4 = 0
⊢ 4 = -2 + 3 * 2
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 = 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 + -1 * e.a4 = 0
⊢ 4 = -2 + 3 * 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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 [dweierstrass_dy]
Proof state after:
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
⊢ 2 * (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3).snd +
        e.a1 * (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3).fst +
      e.a3 =
    0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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
⊢ 2 * (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3).snd +
        e.a1 * (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3).fst +
      e.a3 =
    0
Tactic:
simp only
Proof state after:
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
⊢ 2 * (e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) + 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_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
⊢ 2 * (e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) + e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3 = 0
Tactic:
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]
Proof state after:
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
⊢ 3 * (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_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
⊢ 3 * (e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
Tactic:
rw [hchar'', zero_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 = 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
⊢ 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)
Tactic:
ring
Proof state after:
no goals
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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:
rename_i hn2 hn3
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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
⊢ is_singular_point e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2)
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
⊢ is_singular_point e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2)
Tactic:
rw [is_singular_point]
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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
⊢ weierstrass e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
    dweierstrass_dx e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
      dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
⊢ weierstrass e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
    dweierstrass_dx e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
      dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0
Tactic:
have h2 : (2 : K) ≠ 0 := fun hh => hn2 (ringChar_eq_of_Prime hh (by norm_num))
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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
⊢ weierstrass e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
    dweierstrass_dx e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
      dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
⊢ weierstrass e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
    dweierstrass_dx e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
      dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0
Tactic:
have h3 : (3 : K) ≠ 0 := fun hh => hn3 (ringChar_eq_of_Prime hh (by norm_num))
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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
⊢ weierstrass e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
    dweierstrass_dx e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
      dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
⊢ weierstrass e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
    dweierstrass_dx e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
      dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0
Tactic:
have h12 : (12 : K) ≠ 0 := by
  rw [show (12 : K) = 2 * 2 * 3 by norm_num]
  repeat' apply mul_ne_zero
  all_goals assumption
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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
h12 : 12 ≠ 0
⊢ weierstrass e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
    dweierstrass_dx e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
      dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
h12 : 12 ≠ 0
⊢ weierstrass e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
    dweierstrass_dx e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
      dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0
Tactic:
refine ⟨?_, ?_, ?_⟩
Proof state after:
case pos.h_3.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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
h12 : 12 ≠ 0
⊢ weierstrass e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0

case pos.h_3.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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
h12 : 12 ≠ 0
⊢ dweierstrass_dx e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0

case pos.h_3.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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
h12 : 12 ≠ 0
⊢ dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_3.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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
h12 : 12 ≠ 0
⊢ weierstrass e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0

case pos.h_3.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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
h12 : 12 ≠ 0
⊢ dweierstrass_dx e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0

case pos.h_3.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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
h12 : 12 ≠ 0
⊢ dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0
Tactic:
. 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
Proof state after:
case pos.h_3.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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
h12 : 12 ≠ 0
⊢ dweierstrass_dx e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0

case pos.h_3.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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
h12 : 12 ≠ 0
⊢ dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0