internlm/Lean-Github huggingface dataset:
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
Tactic:
rw [dweierstrass_dx]
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
⊢ e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd -
      (3 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 2 +
          2 * e.a2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
        e.a4) =
    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
⊢ e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd -
      (3 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 2 +
          2 * e.a2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
        e.a4) =
    0
Tactic:
apply nzero_mul_left_cancel (e.c4 ^ 2) _ _ (pow_ne_zero _ hc4)
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
⊢ c4 e ^ 2 *
      (e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd -
        (3 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 2 +
            2 * e.a2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
          e.a4)) =
    c4 e ^ 2 * 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
⊢ c4 e ^ 2 *
      (e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd -
        (3 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 2 +
            2 * e.a2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
          e.a4)) =
    c4 e ^ 2 * 0
Tactic:
rw [mul_zero, pow_two]
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
⊢ c4 e * c4 e *
      (e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd -
        (3 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 2 +
            2 * e.a2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
          e.a4)) =
    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
⊢ c4 e * c4 e *
      (e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd -
        (3 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 2 +
            2 * e.a2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
          e.a4)) =
    0
Tactic:
simp only [div_eq_mul_inv]
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
⊢ 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)) =
    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
⊢ 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)) =
    0
Tactic:
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]
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
⊢ 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 =
    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
⊢ 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 =
    0
Tactic:
simp only [mul_inv_cancel hc4, one_mul]
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
⊢ c4 e * (e.a1 * (b2 e * b5 e + 3 * b7 e) - 2 * e.a2 * (18 * b6 e - b2 e * b4 e)) - 3 * (18 * b6 e - b2 e * b4 e) ^ 2 -
      e.a4 * c4 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
⊢ c4 e * (e.a1 * (b2 e * b5 e + 3 * b7 e) - 2 * e.a2 * (18 * b6 e - b2 e * b4 e)) - 3 * (18 * b6 e - b2 e * b4 e) ^ 2 -
      e.a4 * c4 e * c4 e =
    0
Tactic:
rw [b5, b7, c4, b2, b4, b6]
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
⊢ ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
          (e.a1 *
              ((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.a2 * (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4))) -
        3 * (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) ^ 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)) =
    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
⊢ ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
          (e.a1 *
              ((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.a2 * (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4))) -
        3 * (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) ^ 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)) =
    0
Tactic:
rw [← mul_zero (36 : K), ← h, discr_eq_neg_singular]
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
⊢ ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
          (e.a1 *
              ((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.a2 * (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4))) -
        3 * (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) ^ 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)) =
    36 *
      -(e.a1 ^ 4 * e.a2 * e.a3 ^ 2 - e.a1 ^ 5 * e.a3 * e.a4 + e.a1 ^ 6 * e.a6 + 8 * e.a1 ^ 2 * e.a2 ^ 2 * e.a3 ^ 2 -
                                                    e.a1 ^ 3 * e.a3 ^ 3 -
                                                  8 * e.a1 ^ 3 * e.a2 * e.a3 * e.a4 -
                                                e.a1 ^ 4 * e.a4 ^ 2 +
                                              12 * e.a1 ^ 4 * e.a2 * e.a6 +
                                            16 * e.a2 ^ 3 * e.a3 ^ 2 -
                                          36 * e.a1 * e.a2 * e.a3 ^ 3 -
                                        16 * e.a1 * e.a2 ^ 2 * e.a3 * e.a4 +
                                      30 * e.a1 ^ 2 * e.a3 ^ 2 * e.a4 -
                                    8 * e.a1 ^ 2 * e.a2 * e.a4 ^ 2 +
                                  48 * e.a1 ^ 2 * e.a2 ^ 2 * e.a6 -
                                36 * e.a1 ^ 3 * e.a3 * e.a6 +
                              27 * e.a3 ^ 4 -
                            72 * e.a2 * e.a3 ^ 2 * e.a4 -
                          16 * e.a2 ^ 2 * e.a4 ^ 2 +
                        96 * e.a1 * e.a3 * e.a4 ^ 2 +
                      64 * e.a2 ^ 3 * e.a6 -
                    144 * e.a1 * e.a2 * e.a3 * e.a6 -
                  72 * e.a1 ^ 2 * e.a4 * e.a6 +
                64 * e.a4 ^ 3 +
              216 * e.a3 ^ 2 * e.a6 -
            288 * e.a2 * e.a4 * e.a6 +
          432 * e.a6 ^ 2)
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
⊢ ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
          (e.a1 *
              ((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.a2 * (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4))) -
        3 * (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) ^ 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)) =
    36 *
      -(e.a1 ^ 4 * e.a2 * e.a3 ^ 2 - e.a1 ^ 5 * e.a3 * e.a4 + e.a1 ^ 6 * e.a6 + 8 * e.a1 ^ 2 * e.a2 ^ 2 * e.a3 ^ 2 -
                                                    e.a1 ^ 3 * e.a3 ^ 3 -
                                                  8 * e.a1 ^ 3 * e.a2 * e.a3 * e.a4 -
                                                e.a1 ^ 4 * e.a4 ^ 2 +
                                              12 * e.a1 ^ 4 * e.a2 * e.a6 +
                                            16 * e.a2 ^ 3 * e.a3 ^ 2 -
                                          36 * e.a1 * e.a2 * e.a3 ^ 3 -
                                        16 * e.a1 * e.a2 ^ 2 * e.a3 * e.a4 +
                                      30 * e.a1 ^ 2 * e.a3 ^ 2 * e.a4 -
                                    8 * e.a1 ^ 2 * e.a2 * e.a4 ^ 2 +
                                  48 * e.a1 ^ 2 * e.a2 ^ 2 * e.a6 -
                                36 * e.a1 ^ 3 * e.a3 * e.a6 +
                              27 * e.a3 ^ 4 -
                            72 * e.a2 * e.a3 ^ 2 * e.a4 -
                          16 * e.a2 ^ 2 * e.a4 ^ 2 +
                        96 * e.a1 * e.a3 * e.a4 ^ 2 +
                      64 * e.a2 ^ 3 * e.a6 -
                    144 * e.a1 * e.a2 * e.a3 * e.a6 -
                  72 * e.a1 ^ 2 * e.a4 * e.a6 +
                64 * e.a4 ^ 3 +
              216 * e.a3 ^ 2 * e.a6 -
            288 * e.a2 * e.a4 * e.a6 +
          432 * e.a6 ^ 2)
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
⊢ 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
Tactic:
ring
Proof state after:
no goals
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]
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
⊢ 2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd +
        e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
      e.a3 =
    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
⊢ 2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd +
        e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
      e.a3 =
    0
Tactic:
apply nzero_mul_left_cancel e.c4 _ _ hc4
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
⊢ c4 e *
      (2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd +
          e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
        e.a3) =
    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
⊢ c4 e *
      (2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd +
          e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
        e.a3) =
    c4 e * 0
Tactic:
simp only [div_eq_mul_inv, mul_zero]
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
⊢ 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) = 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
⊢ 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) = 0
Tactic:
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]
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
⊢ 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 = 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
⊢ 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 = 0
Tactic:
simp only [mul_inv_cancel hc4, one_mul]
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
⊢ 2 * (b2 e * b5 e + 3 * b7 e) + e.a1 * (18 * b6 e - b2 e * b4 e) + c4 e * e.a3 = 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
⊢ 2 * (b2 e * b5 e + 3 * b7 e) + e.a1 * (18 * b6 e - b2 e * b4 e) + c4 e * e.a3 = 0
Tactic:
rw [b5, b7, c4, b2, b4, b6]
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
⊢ 2 *
          ((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 * (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.a3 =
    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
⊢ 2 *
          ((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 * (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.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
⊢ 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
Tactic:
ring
Proof state after:
no goals
Theorem: Model.Field.move_singular_point
Proof state before:
K : Type u
inst✝ : Field K
e : Model K
r t : K
P : K × K
h : is_singular_point e P
⊢ is_singular_point (rst_iso r 0 t e) (var_change (-r) 0 (-t) P)
Tactic:
rw [is_singular_point, weierstrass_iso_eq_var_change,
  dweierstrass_dx_iso_eq_var_change, zero_mul, add_zero,
  dweierstrass_dy_iso_eq_var_change, var_change_comp]
Proof state after:
K : Type u
inst✝ : Field K
e : Model K
r t : K
P : K × K
h : is_singular_point e P
⊢ weierstrass e (var_change (r + -r) (0 + 0) (t + -t + 0 * -r) P) = 0 ∧
    dweierstrass_dx e (var_change (r + -r) (0 + 0) (t + -t + 0 * -r) P) = 0 ∧
      dweierstrass_dy e (var_change (r + -r) (0 + 0) (t + -t + 0 * -r) P) = 0
Theorem: Model.Field.move_singular_point
Proof state before:
K : Type u
inst✝ : Field K
e : Model K
r t : K
P : K × K
h : is_singular_point e P
⊢ weierstrass e (var_change (r + -r) (0 + 0) (t + -t + 0 * -r) P) = 0 ∧
    dweierstrass_dx e (var_change (r + -r) (0 + 0) (t + -t + 0 * -r) P) = 0 ∧
      dweierstrass_dy e (var_change (r + -r) (0 + 0) (t + -t + 0 * -r) P) = 0
Tactic:
simpa
Proof state after:
no goals
Theorem: Model.Field.move_singular_point_to_origin
Proof state before:
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
⊢ is_singular_point (move_singular_point_to_origin_iso e) (0, 0)
Tactic:
rw [move_singular_point_to_origin_iso, rst_triple, move_singular_point_to_origin_triple]
Proof state after:
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
⊢ is_singular_point
    (rst_iso ((singular_point e).fst, 0, (singular_point e).snd).fst
      ((singular_point e).fst, 0, (singular_point e).snd).snd.fst
      ((singular_point e).fst, 0, (singular_point e).snd).snd.snd e)
    (0, 0)
Theorem: Model.Field.move_singular_point_to_origin
Proof state before:
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
⊢ is_singular_point
    (rst_iso ((singular_point e).fst, 0, (singular_point e).snd).fst
      ((singular_point e).fst, 0, (singular_point e).snd).snd.fst
      ((singular_point e).fst, 0, (singular_point e).snd).snd.snd e)
    (0, 0)
Tactic:
convert move_singular_point e (singular_point e).fst (singular_point e).snd
  (is_singular_point_singular_point e h) using 2 <;> simp [var_change]
Proof state after:
no goals
Theorem: Model.Field.move_singular_point_to_origin'
Proof state before:
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
⊢ (∃ P, is_singular_point e P) → is_singular_point (move_singular_point_to_origin_iso e) (0, 0)
Tactic:
rintro ⟨P, hP⟩
Proof state after:
case intro
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
P : K × K
hP : is_singular_point e P
⊢ is_singular_point (move_singular_point_to_origin_iso e) (0, 0)
Theorem: Model.Field.move_singular_point_to_origin'
Proof state before:
case intro
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
P : K × K
hP : is_singular_point e P
⊢ is_singular_point (move_singular_point_to_origin_iso e) (0, 0)
Tactic:
have hd := discr_eq_zero_of_singular e hP
Proof state after:
case intro
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
P : K × K
hP : is_singular_point e P
hd : discr e = 0
⊢ is_singular_point (move_singular_point_to_origin_iso e) (0, 0)
Theorem: Model.Field.move_singular_point_to_origin'
Proof state before:
case intro
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
P : K × K
hP : is_singular_point e P
hd : discr e = 0
⊢ is_singular_point (move_singular_point_to_origin_iso e) (0, 0)
Tactic:
exact move_singular_point_to_origin e hd
Proof state after:
no goals
Theorem: mod_neg_right
Proof state before:
m k : Int
⊢ m % -k = m % k
Tactic:
simp
Proof state after:
no goals
Theorem: div_neg_right
Proof state before:
m k : Int
⊢ m / -k = -(m / k)
Tactic:
simp
Proof state after:
no goals
Theorem: Model.is_local_singular_point_iff
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
P : R × R
⊢ is_local_singular_point evr.valtn e P ↔
    is_singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)
      (Prod.map (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) P)
Tactic:
rw [is_singular_point, weierstrass_map, dweierstrass_dx_map, dweierstrass_dy_map, is_local_singular_point]
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
P : R × R
⊢ SurjVal.v evr.valtn (weierstrass e P) > 0 ∧
      SurjVal.v evr.valtn (dweierstrass_dx e P) > 0 ∧ SurjVal.v evr.valtn (dweierstrass_dy e P) > 0 ↔
    ↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (weierstrass e P) = 0 ∧
      ↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (dweierstrass_dx e P) = 0 ∧
        ↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (dweierstrass_dy e P) = 0
Theorem: Model.is_local_singular_point_iff
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
P : R × R
⊢ SurjVal.v evr.valtn (weierstrass e P) > 0 ∧
      SurjVal.v evr.valtn (dweierstrass_dx e P) > 0 ∧ SurjVal.v evr.valtn (dweierstrass_dy e P) > 0 ↔
    ↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (weierstrass e P) = 0 ∧
      ↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (dweierstrass_dx e P) = 0 ∧
        ↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (dweierstrass_dy e P) = 0
Tactic:
simp [Ideal.Quotient.eq_zero_iff_mem]
Proof state after:
no goals
Theorem: Model.singular_of_val_discr
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h : SurjVal.v evr.valtn (discr e) > 0
⊢ ∃ P, is_local_singular_point evr.valtn e P
Tactic:
sorry
Proof state after:
no goals
Theorem: Model.move_singular_point_to_origin
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
⊢ (∃ P, is_local_singular_point evr.valtn e P) →
    is_local_singular_point evr.valtn (move_singular_point_to_origin_iso evr e) (0, 0)
Tactic:
rintro ⟨P, h⟩
Proof state after:
case intro
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
⊢ is_local_singular_point evr.valtn (move_singular_point_to_origin_iso evr e) (0, 0)