internlm/Lean-Github huggingface dataset:
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
⊢ 12 * dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 12 * 0
Tactic:
simp only [dweierstrass_dy, div_eq_mul_inv, mul_zero]
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 * (2 * (-(-e.a1 * b2 e * 12⁻¹ + e.a3) * 2⁻¹) + e.a1 * (-b2 e * 12⁻¹) + e.a3) = 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
⊢ 12 * (2 * (-(-e.a1 * b2 e * 12⁻¹ + e.a3) * 2⁻¹) + e.a1 * (-b2 e * 12⁻¹) + e.a3) = 0
Tactic:
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]
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
⊢ -(-e.a1 * b2 e * (12 * 12⁻¹) + 12 * e.a3) * (2 * 2⁻¹) + e.a1 * (-b2 e * (12 * 12⁻¹)) + 12 * e.a3 = 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
⊢ -(-e.a1 * b2 e * (12 * 12⁻¹) + 12 * e.a3) * (2 * 2⁻¹) + e.a1 * (-b2 e * (12 * 12⁻¹)) + 12 * e.a3 = 0
Tactic:
simp only [mul_inv_cancel h2, mul_inv_cancel h12, one_mul, mul_one]
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
⊢ -(-e.a1 * b2 e + 12 * e.a3) + e.a1 * -b2 e + 12 * e.a3 = 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
⊢ -(-e.a1 * b2 e + 12 * e.a3) + e.a1 * -b2 e + 12 * e.a3 = 0
Tactic:
simp only [c6, b2, b4, b6]
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
⊢ -(-e.a1 * (e.a1 * e.a1 + 4 * e.a2) + 12 * e.a3) + e.a1 * -(e.a1 * e.a1 + 4 * e.a2) + 12 * e.a3 = 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
⊢ -(-e.a1 * (e.a1 * e.a1 + 4 * e.a2) + 12 * e.a3) + e.a1 * -(e.a1 * e.a1 + 4 * e.a2) + 12 * e.a3 = 0
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 * 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
Tactic:
ring
Proof state after:
no goals
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case neg
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ is_singular_point e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e)
Tactic:
rw [is_singular_point]
Proof state after:
case neg
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ weierstrass e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0 ∧
    dweierstrass_dx e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0 ∧
      dweierstrass_dy e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case neg
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ weierstrass e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0 ∧
    dweierstrass_dx e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0 ∧
      dweierstrass_dy e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0
Tactic:
refine ⟨?_, ?_, ?_⟩
Proof state after:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ weierstrass e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0

case neg.refine_2
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ dweierstrass_dx e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0

case neg.refine_3
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ dweierstrass_dy e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ weierstrass e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0

case neg.refine_2
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ dweierstrass_dx e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0

case neg.refine_3
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ dweierstrass_dy e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0
Tactic:
. rw [weierstrass]
  apply nzero_mul_left_cancel (e.c4 ^ 3) _ _ (pow_ne_zero _ hc4)
  rw [mul_zero]
  simp only [div_eq_mul_inv]
  rw [show c4 e ^ 3 * (((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) ^ 2 +
        e.a1 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) +
      e.a3 * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) -
      (((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 3 + e.a2 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 2 +
      e.a4 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) + e.a6)) =
    (c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * ((b2 e * b5 e + 3 * b7 e)) ^ 2 +
      c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a1 * ((18 * b6 e - b2 e * b4 e)) * ((b2 e * b5 e + 3 * b7 e)) +
    c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a3 * ((b2 e * b5 e + 3 * b7 e)) -
    (c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * ((18 * b6 e - b2 e * b4 e)) ^ 3 +
    c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a2 * ((18 * b6 e - b2 e * b4 e)) ^ 2 +
      c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a4 * ((18 * b6 e - b2 e * b4 e)) +
    c4 e * c4 e * c4 e * e.a6)) by ring]
  simp only [mul_inv_cancel hc4, one_mul]
  rw [b5, b7, c4, b2, b4, b6]
  rw [← mul_zero (e.a1^6 + 12*e.a1^4*e.a2 + 48*e.a1^2*e.a2^2 - 36*e.a1^3*e.a3 + 64*e.a2^3
    - 144*e.a1*e.a2*e.a3 - 72*e.a1^2*e.a4 + 216*e.a3^2 - 288*e.a2*e.a4 + 864*e.a6),
    ← h, discr_eq_neg_singular]
  ring
Proof state after:
case neg.refine_2
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ dweierstrass_dx e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0

case neg.refine_3
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ dweierstrass_dy e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case neg.refine_2
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ dweierstrass_dx e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0

case neg.refine_3
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ dweierstrass_dy e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0
Tactic:
. rw [dweierstrass_dx]
  apply nzero_mul_left_cancel (e.c4 ^ 2) _ _ (pow_ne_zero _ hc4)
  rw [mul_zero, pow_two]
  simp only [div_eq_mul_inv]
  rw [show c4 e * c4 e *
    (e.a1 * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) -
      (3 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 2
      + 2 * e.a2 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) + e.a4)) =
      c4 e * (c4 e)⁻¹ * c4 e * (e.a1 * (b2 e * b5 e + 3 * b7 e)
      - 2 * e.a2 * ((18 * b6 e - b2 e * b4 e)))
      - c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ *
      3 * (18 * b6 e - b2 e * b4 e) ^ 2 - e.a4 * c4 e * c4 e
    by ring]
  simp only [mul_inv_cancel hc4, one_mul]
  rw [b5, b7, c4, b2, b4, b6]
  rw [← mul_zero (36 : K), ← h, discr_eq_neg_singular]
  ring
Proof state after:
case neg.refine_3
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ dweierstrass_dy e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case neg.refine_3
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ dweierstrass_dy e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0
Tactic:
. rw [dweierstrass_dy]
  apply nzero_mul_left_cancel e.c4 _ _ hc4
  simp only [div_eq_mul_inv, mul_zero]
  rw [show c4 e * (2 * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹)
      + e.a1 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) + e.a3) =
    c4 e * (c4 e)⁻¹ * (2 * (b2 e * b5 e + 3 * b7 e)
    + e.a1 * ((18 * b6 e - b2 e * b4 e))) + c4 e * e.a3 by ring]
  simp only [mul_inv_cancel hc4, one_mul]
  rw [b5, b7, c4, b2, b4, b6]
  ring
Proof state after:
no goals
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ weierstrass e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e) = 0
Tactic:
rw [weierstrass]
Proof state after:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd ^ 2 +
          e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst *
            ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd +
        e.a3 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd -
      (((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 3 +
            e.a2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 2 +
          e.a4 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
        e.a6) =
    0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd ^ 2 +
          e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst *
            ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd +
        e.a3 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd -
      (((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 3 +
            e.a2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 2 +
          e.a4 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
        e.a6) =
    0
Tactic:
apply nzero_mul_left_cancel (e.c4 ^ 3) _ _ (pow_ne_zero _ hc4)
Proof state after:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ c4 e ^ 3 *
      (((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd ^ 2 +
            e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst *
              ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd +
          e.a3 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd -
        (((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 3 +
              e.a2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 2 +
            e.a4 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
          e.a6)) =
    c4 e ^ 3 * 0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ c4 e ^ 3 *
      (((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd ^ 2 +
            e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst *
              ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd +
          e.a3 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd -
        (((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 3 +
              e.a2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 2 +
            e.a4 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
          e.a6)) =
    c4 e ^ 3 * 0
Tactic:
rw [mul_zero]
Proof state after:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ c4 e ^ 3 *
      (((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd ^ 2 +
            e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst *
              ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd +
          e.a3 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd -
        (((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 3 +
              e.a2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 2 +
            e.a4 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
          e.a6)) =
    0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ c4 e ^ 3 *
      (((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd ^ 2 +
            e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst *
              ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd +
          e.a3 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd -
        (((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 3 +
              e.a2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 2 +
            e.a4 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
          e.a6)) =
    0
Tactic:
simp only [div_eq_mul_inv]
Proof state after:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ c4 e ^ 3 *
      (((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) ^ 2 +
            e.a1 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) +
          e.a3 * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) -
        (((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 3 + e.a2 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 2 +
            e.a4 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) +
          e.a6)) =
    0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ c4 e ^ 3 *
      (((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) ^ 2 +
            e.a1 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) +
          e.a3 * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) -
        (((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 3 + e.a2 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 2 +
            e.a4 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) +
          e.a6)) =
    0
Tactic:
rw [show c4 e ^ 3 * (((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) ^ 2 +
      e.a1 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) +
    e.a3 * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) -
    (((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 3 + e.a2 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 2 +
    e.a4 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) + e.a6)) =
  (c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * ((b2 e * b5 e + 3 * b7 e)) ^ 2 +
    c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a1 * ((18 * b6 e - b2 e * b4 e)) * ((b2 e * b5 e + 3 * b7 e)) +
  c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a3 * ((b2 e * b5 e + 3 * b7 e)) -
  (c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * ((18 * b6 e - b2 e * b4 e)) ^ 3 +
  c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a2 * ((18 * b6 e - b2 e * b4 e)) ^ 2 +
    c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a4 * ((18 * b6 e - b2 e * b4 e)) +
  c4 e * c4 e * c4 e * e.a6)) by ring]
Proof state after:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * (b2 e * b5 e + 3 * b7 e) ^ 2 +
          c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a1 * (18 * b6 e - b2 e * b4 e) * (b2 e * b5 e + 3 * b7 e) +
        c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a3 * (b2 e * b5 e + 3 * b7 e) -
      (c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * (18 * b6 e - b2 e * b4 e) ^ 3 +
            c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a2 * (18 * b6 e - b2 e * b4 e) ^ 2 +
          c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a4 * (18 * b6 e - b2 e * b4 e) +
        c4 e * c4 e * c4 e * e.a6) =
    0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * (b2 e * b5 e + 3 * b7 e) ^ 2 +
          c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a1 * (18 * b6 e - b2 e * b4 e) * (b2 e * b5 e + 3 * b7 e) +
        c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a3 * (b2 e * b5 e + 3 * b7 e) -
      (c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * (18 * b6 e - b2 e * b4 e) ^ 3 +
            c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a2 * (18 * b6 e - b2 e * b4 e) ^ 2 +
          c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a4 * (18 * b6 e - b2 e * b4 e) +
        c4 e * c4 e * c4 e * e.a6) =
    0
Tactic:
simp only [mul_inv_cancel hc4, one_mul]
Proof state after:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ c4 e * (b2 e * b5 e + 3 * b7 e) ^ 2 + c4 e * e.a1 * (18 * b6 e - b2 e * b4 e) * (b2 e * b5 e + 3 * b7 e) +
        c4 e * c4 e * e.a3 * (b2 e * b5 e + 3 * b7 e) -
      ((18 * b6 e - b2 e * b4 e) ^ 3 + c4 e * e.a2 * (18 * b6 e - b2 e * b4 e) ^ 2 +
          c4 e * c4 e * e.a4 * (18 * b6 e - b2 e * b4 e) +
        c4 e * c4 e * c4 e * e.a6) =
    0
Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ c4 e * (b2 e * b5 e + 3 * b7 e) ^ 2 + c4 e * e.a1 * (18 * b6 e - b2 e * b4 e) * (b2 e * b5 e + 3 * b7 e) +
        c4 e * c4 e * e.a3 * (b2 e * b5 e + 3 * b7 e) -
      ((18 * b6 e - b2 e * b4 e) ^ 3 + c4 e * e.a2 * (18 * b6 e - b2 e * b4 e) ^ 2 +
          c4 e * c4 e * e.a4 * (18 * b6 e - b2 e * b4 e) +
        c4 e * c4 e * c4 e * e.a6) =
    0
Tactic:
rw [b5, b7, c4, b2, b4, b6]
Proof state after:
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
            ((e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a4 - 2 * e.a2 * e.a3) +
                3 * (e.a1 * (e.a3 ^ 2 - 12 * e.a6) + 8 * e.a3 * e.a4)) ^
              2 +
          ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) * e.a1 *
              (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) *
            ((e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a4 - 2 * e.a2 * e.a3) +
              3 * (e.a1 * (e.a3 ^ 2 - 12 * e.a6) + 8 * e.a3 * e.a4)) +
        ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
              ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
            e.a3 *
          ((e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a4 - 2 * e.a2 * e.a3) +
            3 * (e.a1 * (e.a3 ^ 2 - 12 * e.a6) + 8 * e.a3 * e.a4)) -
      ((18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) ^ 3 +
            ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) * e.a2 *
              (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) ^ 2 +
          ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
                ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
              e.a4 *
            (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) +
        ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
              ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
            ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
          e.a6) =
    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
⊢ c4 e ^ 3 *
      (((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) ^ 2 +
            e.a1 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) +
          e.a3 * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) -
        (((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 3 + e.a2 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 2 +
            e.a4 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) +
          e.a6)) =
    c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * (b2 e * b5 e + 3 * b7 e) ^ 2 +
          c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a1 * (18 * b6 e - b2 e * b4 e) * (b2 e * b5 e + 3 * b7 e) +
        c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a3 * (b2 e * b5 e + 3 * b7 e) -
      (c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * (18 * b6 e - b2 e * b4 e) ^ 3 +
            c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a2 * (18 * b6 e - b2 e * b4 e) ^ 2 +
          c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a4 * (18 * b6 e - b2 e * b4 e) +
        c4 e * c4 e * c4 e * e.a6)
Tactic:
ring
Proof state after:
no goals