internlm/Lean-Github huggingface dataset:
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
  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:
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
⊢ c6 e = 0
Tactic:
simpa [h, hc4, pow_succ, mul_eq_zero] using discr_identity e
Proof state after:
no goals
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_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
⊢ is_singular_point e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6))
Tactic:
rw [is_singular_point]
Proof state after:
case pos.h_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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Tactic:
have hchar : ringChar K = 2 := by assumption
Proof state after:
case pos.h_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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Tactic:
have hchar' : (ringChar K : K) = 2 := by simp [hchar]
Proof state after:
case pos.h_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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Tactic:
have hchar'' : (2 : K) = 0 := by simp [← hchar', ringChar.Nat.cast_ringChar]
Proof state after:
case pos.h_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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Tactic:
have hcharne : ringChar K ≠ 0 := by simp [hchar]
Proof state after:
case pos.h_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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Tactic:
have ha1 : e.a1 = 0 := by simpa [c4_zero_iff_a1_zero_of_char_two e hchar] using hc4
Proof state after:
case pos.h_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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Tactic:
have ha3 : e.a3 = 0 := a3_zero_of_a1_zero_of_disc_zero_of_char_two e hchar h ha1
Proof state after:
case pos.h_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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case pos.h_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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Tactic:
refine ⟨?_, ?_, ?_⟩
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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0

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

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
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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0

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

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:
. 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'']
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
⊢ dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0

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
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

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:
. 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]
Proof state after:
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
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:
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
⊢ ringChar K = 2
Tactic:
assumption
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
⊢ ↑(ringChar K) = 2
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
⊢ 2 = 0
Tactic:
simp [← hchar', ringChar.Nat.cast_ringChar]
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
⊢ ringChar K ≠ 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
⊢ e.a1 = 0
Tactic:
simpa [c4_zero_iff_a1_zero_of_char_two e hchar] using hc4
Proof state after:
no goals
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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
Tactic:
rw [weierstrass]
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
⊢ (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).snd ^ 2 +
          e.a1 * (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).fst *
            (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).snd +
        e.a3 * (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).snd -
      ((pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).fst ^ 3 +
            e.a2 * (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).fst ^ 2 +
          e.a4 * (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).fst +
        e.a6) =
    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
⊢ (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).snd ^ 2 +
          e.a1 * (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).fst *
            (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).snd +
        e.a3 * (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).snd -
      ((pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).fst ^ 3 +
            e.a2 * (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).fst ^ 2 +
          e.a4 * (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)).fst +
        e.a6) =
    0
Tactic:
simp only [ha1, ha3, mul_zero, zero_add, zero_mul, add_zero]
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
⊢ pth_root (e.a2 * e.a4 + e.a6) ^ 2 - (pth_root e.a4 ^ 3 + e.a2 * pth_root e.a4 ^ 2 + e.a4 * pth_root e.a4 + e.a6) = 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
⊢ pth_root (e.a2 * e.a4 + e.a6) ^ 2 - (pth_root e.a4 ^ 3 + e.a2 * pth_root e.a4 ^ 2 + e.a4 * pth_root e.a4 + e.a6) = 0
Tactic:
rw [show 3 = 2 + 1 by norm_num]
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
⊢ pth_root (e.a2 * e.a4 + e.a6) ^ 2 -
      (pth_root e.a4 ^ (2 + 1) + e.a2 * pth_root e.a4 ^ 2 + e.a4 * pth_root e.a4 + e.a6) =
    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
⊢ pth_root (e.a2 * e.a4 + e.a6) ^ 2 -
      (pth_root e.a4 ^ (2 + 1) + e.a2 * pth_root e.a4 ^ 2 + e.a4 * pth_root e.a4 + e.a6) =
    0
Tactic:
rw [pow_succ _ 2]
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
⊢ pth_root (e.a2 * e.a4 + e.a6) ^ 2 -
      (pth_root e.a4 * pth_root e.a4 ^ 2 + e.a2 * pth_root e.a4 ^ 2 + e.a4 * pth_root e.a4 + e.a6) =
    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
⊢ pth_root (e.a2 * e.a4 + e.a6) ^ 2 -
      (pth_root e.a4 * pth_root e.a4 ^ 2 + e.a2 * pth_root e.a4 ^ 2 + e.a4 * pth_root e.a4 + e.a6) =
    0
Tactic:
rw [← hchar, pth_root_pow_char hcharne]
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.a2 * e.a4 + e.a6 -
      (pth_root e.a4 * pth_root e.a4 ^ ringChar K + e.a2 * pth_root e.a4 ^ ringChar K + e.a4 * pth_root e.a4 + e.a6) =
    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.a2 * e.a4 + e.a6 -
      (pth_root e.a4 * pth_root e.a4 ^ ringChar K + e.a2 * pth_root e.a4 ^ ringChar K + e.a4 * pth_root e.a4 + e.a6) =
    0
Tactic:
rw [pth_root_pow_char hcharne]
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.a2 * e.a4 + e.a6 - (pth_root e.a4 * e.a4 + e.a2 * e.a4 + e.a4 * pth_root e.a4 + e.a6) = 0