internlm/Lean-Github huggingface dataset:
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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 ^ 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
Proof state after:
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_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 _ _ 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
hc6 : c6 e = 0
x✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
hh : 2 = 0
⊢ Nat.Prime 2
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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
hh : 3 = 0
⊢ Nat.Prime 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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
⊢ 12 ≠ 0
Tactic:
rw [show (12 : K) = 2 * 2 * 3 by norm_num]
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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
⊢ 2 * 2 * 3 ≠ 0
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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
⊢ 2 * 2 * 3 ≠ 0
Tactic:
repeat' apply mul_ne_zero
Proof state after:
case ha.ha
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
⊢ 2 ≠ 0

case ha.hb
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
⊢ 2 ≠ 0

case hb
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
⊢ 3 ≠ 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case ha.ha
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
⊢ 2 ≠ 0

case ha.hb
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
⊢ 2 ≠ 0

case hb
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
⊢ 3 ≠ 0
Tactic:
all_goals 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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
⊢ 12 = 2 * 2 * 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case ha
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
⊢ 2 * 2 ≠ 0
Tactic:
apply mul_ne_zero
Proof state after:
case ha.ha
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
⊢ 2 ≠ 0

case ha.hb
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
⊢ 2 ≠ 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case hb
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
⊢ 3 ≠ 0
Tactic:
assumption
Proof state after:
no goals
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
Tactic:
apply nzero_mul_left_cancel (12 ^ 3) _ _ (pow_ne_zero _ h12)
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
⊢ 12 ^ 3 * weierstrass e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 12 ^ 3 * 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
⊢ 12 ^ 3 * weierstrass e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 12 ^ 3 * 0
Tactic:
simp only [weierstrass, div_eq_mul_inv, mul_zero]
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
⊢ 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)) =
    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
⊢ 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)) =
    0
Tactic:
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]
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
⊢ 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) =
    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
⊢ 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) =
    0
Tactic:
simp only [mul_inv_cancel h2, mul_inv_cancel h12, one_mul, mul_one]
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
⊢ 3 * (-(-e.a1 * b2 e + 12 * e.a3)) ^ 2 + e.a1 * -b2 e * (-(-e.a1 * b2 e + 12 * e.a3) * 6) +
        12 * e.a3 * (-(-e.a1 * b2 e + 12 * e.a3) * 6) -
      ((-b2 e) ^ 3 + 12 * e.a2 * (-b2 e) ^ 2 + 12 ^ 2 * e.a4 * -b2 e + 12 ^ 3 * e.a6) =
    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
⊢ 3 * (-(-e.a1 * b2 e + 12 * e.a3)) ^ 2 + e.a1 * -b2 e * (-(-e.a1 * b2 e + 12 * e.a3) * 6) +
        12 * e.a3 * (-(-e.a1 * b2 e + 12 * e.a3) * 6) -
      ((-b2 e) ^ 3 + 12 * e.a2 * (-b2 e) ^ 2 + 12 ^ 2 * e.a4 * -b2 e + 12 ^ 3 * e.a6) =
    0
Tactic:
rw [← mul_zero (2 : K), ← hc6]
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
⊢ 3 * (-(-e.a1 * b2 e + 12 * e.a3)) ^ 2 + e.a1 * -b2 e * (-(-e.a1 * b2 e + 12 * e.a3) * 6) +
        12 * e.a3 * (-(-e.a1 * b2 e + 12 * e.a3) * 6) -
      ((-b2 e) ^ 3 + 12 * e.a2 * (-b2 e) ^ 2 + 12 ^ 2 * e.a4 * -b2 e + 12 ^ 3 * e.a6) =
    2 * c6 e
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
⊢ 3 * (-(-e.a1 * b2 e + 12 * e.a3)) ^ 2 + e.a1 * -b2 e * (-(-e.a1 * b2 e + 12 * e.a3) * 6) +
        12 * e.a3 * (-(-e.a1 * b2 e + 12 * e.a3) * 6) -
      ((-b2 e) ^ 3 + 12 * e.a2 * (-b2 e) ^ 2 + 12 ^ 2 * e.a4 * -b2 e + 12 ^ 3 * e.a6) =
    2 * c6 e
Tactic:
simp only [c6, b2, b4, b6]
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
⊢ 3 * (-(-e.a1 * (e.a1 * e.a1 + 4 * e.a2) + 12 * e.a3)) ^ 2 +
          e.a1 * -(e.a1 * e.a1 + 4 * e.a2) * (-(-e.a1 * (e.a1 * e.a1 + 4 * e.a2) + 12 * e.a3) * 6) +
        12 * e.a3 * (-(-e.a1 * (e.a1 * e.a1 + 4 * e.a2) + 12 * e.a3) * 6) -
      ((-(e.a1 * e.a1 + 4 * e.a2)) ^ 3 + 12 * e.a2 * (-(e.a1 * e.a1 + 4 * e.a2)) ^ 2 +
          12 ^ 2 * e.a4 * -(e.a1 * e.a1 + 4 * e.a2) +
        12 ^ 3 * e.a6) =
    2 *
      (-(e.a1 * e.a1 + 4 * e.a2) ^ 3 + 36 * (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4) -
        216 * (e.a3 * e.a3 + 4 * e.a6))
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
⊢ 3 * (-(-e.a1 * (e.a1 * e.a1 + 4 * e.a2) + 12 * e.a3)) ^ 2 +
          e.a1 * -(e.a1 * e.a1 + 4 * e.a2) * (-(-e.a1 * (e.a1 * e.a1 + 4 * e.a2) + 12 * e.a3) * 6) +
        12 * e.a3 * (-(-e.a1 * (e.a1 * e.a1 + 4 * e.a2) + 12 * e.a3) * 6) -
      ((-(e.a1 * e.a1 + 4 * e.a2)) ^ 3 + 12 * e.a2 * (-(e.a1 * e.a1 + 4 * e.a2)) ^ 2 +
          12 ^ 2 * e.a4 * -(e.a1 * e.a1 + 4 * e.a2) +
        12 ^ 3 * e.a6) =
    2 *
      (-(e.a1 * e.a1 + 4 * e.a2) ^ 3 + 36 * (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4) -
        216 * (e.a3 * e.a3 + 4 * e.a6))
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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
h12 : 12 ≠ 0
⊢ 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)
Tactic:
ring
Proof state after:
no goals
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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
Tactic:
apply nzero_mul_left_cancel (12 ^ 2) _ _ (pow_ne_zero _ h12)
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
⊢ 12 ^ 2 * dweierstrass_dx e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 12 ^ 2 * 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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
⊢ 12 ^ 2 * dweierstrass_dx e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 12 ^ 2 * 0
Tactic:
simp only [dweierstrass_dx, div_eq_mul_inv, mul_zero]
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
⊢ 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)) =
    0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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
⊢ 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)) =
    0
Tactic:
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]
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
⊢ 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) =
    0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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
⊢ 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) =
    0
Tactic:
simp only [mul_inv_cancel h2, mul_inv_cancel h12, one_mul, mul_one]
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
⊢ e.a1 * (-(-e.a1 * b2 e + 12 * e.a3) * 6) - (3 * (-b2 e) ^ 2 + 24 * e.a2 * -b2 e + 144 * e.a4) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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
⊢ e.a1 * (-(-e.a1 * b2 e + 12 * e.a3) * 6) - (3 * (-b2 e) ^ 2 + 24 * e.a2 * -b2 e + 144 * e.a4) = 0
Tactic:
rw [← mul_zero (3 : K), ← hc4]
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
⊢ e.a1 * (-(-e.a1 * b2 e + 12 * e.a3) * 6) - (3 * (-b2 e) ^ 2 + 24 * e.a2 * -b2 e + 144 * e.a4) = 3 * c4 e
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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
⊢ e.a1 * (-(-e.a1 * b2 e + 12 * e.a3) * 6) - (3 * (-b2 e) ^ 2 + 24 * e.a2 * -b2 e + 144 * e.a4) = 3 * c4 e
Tactic:
simp only [c4, c6, b2, b4, b6]
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
⊢ e.a1 * (-(-e.a1 * (e.a1 * e.a1 + 4 * e.a2) + 12 * e.a3) * 6) -
      (3 * (-(e.a1 * e.a1 + 4 * e.a2)) ^ 2 + 24 * e.a2 * -(e.a1 * e.a1 + 4 * e.a2) + 144 * e.a4) =
    3 * ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4))
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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
⊢ e.a1 * (-(-e.a1 * (e.a1 * e.a1 + 4 * e.a2) + 12 * e.a3) * 6) -
      (3 * (-(e.a1 * e.a1 + 4 * e.a2)) ^ 2 + 24 * e.a2 * -(e.a1 * e.a1 + 4 * e.a2) + 144 * e.a4) =
    3 * ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * 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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
h12 : 12 ≠ 0
⊢ 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)
Tactic:
ring
Proof state after:
no goals
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
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 _ _ h12
Proof state after:
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
⊢ 12 * dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 12 * 0