internlm/Lean-Github huggingface dataset:
Theorem: Model.rst_discr
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ discr (rst_iso r s t e) = discr e
Tactic:
simp only [discr, rst_b2, rst_b4, rst_b6, rst_b8]
Proof state after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ -(b2 e + 12 * r) * (b2 e + 12 * r) * (b8 e + 3 * r * b6 e + 3 * r * r * b4 e + r * r * r * b2 e + 3 * r * r * r * r) -
          8 * (b4 e + r * (b2 e + 6 * r)) ^ 3 -
        27 * (b6 e + 2 * r * b4 e + r * r * b2 e + 4 * r * r * r) *
          (b6 e + 2 * r * b4 e + r * r * b2 e + 4 * r * r * r) +
      9 * (b2 e + 12 * r) * (b4 e + r * (b2 e + 6 * r)) * (b6 e + 2 * r * b4 e + r * r * b2 e + 4 * r * r * r) =
    -b2 e * b2 e * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * b2 e * b4 e * b6 e
Theorem: Model.rst_discr
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ -(b2 e + 12 * r) * (b2 e + 12 * r) * (b8 e + 3 * r * b6 e + 3 * r * r * b4 e + r * r * r * b2 e + 3 * r * r * r * r) -
          8 * (b4 e + r * (b2 e + 6 * r)) ^ 3 -
        27 * (b6 e + 2 * r * b4 e + r * r * b2 e + 4 * r * r * r) *
          (b6 e + 2 * r * b4 e + r * r * b2 e + 4 * r * r * r) +
      9 * (b2 e + 12 * r) * (b4 e + r * (b2 e + 6 * r)) * (b6 e + 2 * r * b4 e + r * r * b2 e + 4 * r * r * r) =
    -b2 e * b2 e * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * b2 e * b4 e * b6 e
Tactic:
simp only [mul_add]
Proof state after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * b8 e +
                  (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * b6 e) +
                (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * b4 e) +
              (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (r * r * r * b2 e) +
            (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * r * r) -
          8 * (b4 e + (r * b2 e + r * (6 * r))) ^ 3 -
        ((27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * b6 e +
              (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (2 * r * b4 e) +
            (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (r * r * b2 e) +
          (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (4 * r * r * r)) +
      (((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              b6 e +
            ((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              (2 * r * b4 e) +
          ((9 * b2 e + 9 * (12 * r)) * b4 e +
              ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
            (r * r * b2 e) +
        ((9 * b2 e + 9 * (12 * r)) * b4 e +
            ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
          (4 * r * r * r)) =
    -b2 e * b2 e * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * b2 e * b4 e * b6 e
Theorem: Model.rst_discr
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ -(b2 e ^ 2 * b8 e) + (-(3 * r) * b2 e + -(b2 e + 12 * r) * (3 * r)) * (b2 e * b6 e - b4 e ^ 2) +
                  (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * b6 e) +
                (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * b4 e) +
              (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (r * r * r * b2 e) +
            (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * r * r) -
          8 * (b4 e + (r * b2 e + r * (6 * r))) ^ 3 -
        ((27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * b6 e +
              (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (2 * r * b4 e) +
            (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (r * r * b2 e) +
          (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (4 * r * r * r)) +
      (((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              b6 e +
            ((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              (2 * r * b4 e) +
          ((9 * b2 e + 9 * (12 * r)) * b4 e +
              ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
            (r * r * b2 e) +
        ((9 * b2 e + 9 * (12 * r)) * b4 e +
            ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
          (4 * r * r * r)) =
    -b2 e * b2 e * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * b2 e * b4 e * b6 e
Tactic:
ring
Proof state after:
no goals
Theorem: Model.rst_discr
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * b8 e =
    -(b2 e ^ 2 * b8 e) + (-(3 * r) * b2 e + -(b2 e + 12 * r) * (3 * r)) * (4 * b8 e)
Tactic:
ring
Proof state after:
no goals
Theorem: Model.map_b2
Proof state before:
R✝ : Type u
inst✝² : CommRing R✝
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
e : Model R
⊢ b2 (map f e) = ↑f (b2 e)
Tactic:
simp [Model.b2]
Proof state after:
no goals
Theorem: Model.map_b4
Proof state before:
R✝ : Type u
inst✝² : CommRing R✝
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
e : Model R
⊢ b4 (map f e) = ↑f (b4 e)
Tactic:
simp [Model.b4]
Proof state after:
no goals
Theorem: Model.map_b5
Proof state before:
R✝ : Type u
inst✝² : CommRing R✝
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
e : Model R
⊢ b5 (map f e) = ↑f (b5 e)
Tactic:
simp [Model.b5]
Proof state after:
no goals
Theorem: Model.map_b6
Proof state before:
R✝ : Type u
inst✝² : CommRing R✝
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
e : Model R
⊢ b6 (map f e) = ↑f (b6 e)
Tactic:
simp [Model.b6]
Proof state after:
no goals
Theorem: Model.map_b7
Proof state before:
R✝ : Type u
inst✝² : CommRing R✝
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
e : Model R
⊢ b7 (map f e) = ↑f (b7 e)
Tactic:
simp [Model.b7]
Proof state after:
no goals
Theorem: Model.map_b8
Proof state before:
R✝ : Type u
inst✝² : CommRing R✝
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
e : Model R
⊢ b8 (map f e) = ↑f (b8 e)
Tactic:
simp [Model.b8]
Proof state after:
no goals
Theorem: Model.map_c4
Proof state before:
R✝ : Type u
inst✝² : CommRing R✝
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
e : Model R
⊢ c4 (map f e) = ↑f (c4 e)
Tactic:
simp [Model.c4]
Proof state after:
no goals
Theorem: Model.map_c6
Proof state before:
R✝ : Type u
inst✝² : CommRing R✝
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
e : Model R
⊢ c6 (map f e) = ↑f (c6 e)
Tactic:
simp [Model.c6]
Proof state after:
no goals
Theorem: Model.map_discr
Proof state before:
R✝ : Type u
inst✝² : CommRing R✝
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
e : Model R
⊢ discr (map f e) = ↑f (discr e)
Tactic:
simp [Model.discr]
Proof state after:
no goals
Theorem: Model.weierstrass_map
Proof state before:
R✝ : Type u
inst✝² : CommRing R✝
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
e : Model R
P : R × R
⊢ weierstrass (map f e) (Prod.map (↑f) (↑f) P) = ↑f (weierstrass e P)
Tactic:
simp [weierstrass]
Proof state after:
no goals
Theorem: Model.dweierstrass_dx_map
Proof state before:
R✝ : Type u
inst✝² : CommRing R✝
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
e : Model R
P : R × R
⊢ dweierstrass_dx (map f e) (Prod.map (↑f) (↑f) P) = ↑f (dweierstrass_dx e P)
Tactic:
simp [dweierstrass_dx]
Proof state after:
no goals
Theorem: Model.dweierstrass_dy_map
Proof state before:
R✝ : Type u
inst✝² : CommRing R✝
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
e : Model R
P : R × R
⊢ dweierstrass_dy (map f e) (Prod.map (↑f) (↑f) P) = ↑f (dweierstrass_dy e P)
Tactic:
simp [dweierstrass_dy]
Proof state after:
no goals
Theorem: Model.discr_eq_neg_singular
Proof state before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ -(e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a1 + 4 * e.a2) *
            (e.a1 * e.a1 * e.a6 - e.a1 * e.a3 * e.a4 + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4) -
          8 * (e.a1 * e.a3 + 2 * e.a4) ^ 3 -
        27 * (e.a3 * e.a3 + 4 * e.a6) * (e.a3 * e.a3 + 4 * e.a6) +
      9 * (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4) * (e.a3 * e.a3 + 4 * e.a6) =
    -(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.var_change_comp
Proof state before:
R : Type u
inst✝ : CommRing R
r s t r' s' t' : R
P : R × R
⊢ var_change r s t (var_change r' s' t' P) = var_change (r + r') (s + s') (t + t' + s * r') P
Tactic:
simp only [var_change, Prod.mk.injEq]
Proof state after:
R : Type u
inst✝ : CommRing R
r s t r' s' t' : R
P : R × R
⊢ P.fst + r' + r = P.fst + (r + r') ∧
    P.snd + s' * P.fst + t' + s * (P.fst + r') + t = P.snd + (s + s') * P.fst + (t + t' + s * r')
Theorem: Model.var_change_comp
Proof state before:
R : Type u
inst✝ : CommRing R
r s t r' s' t' : R
P : R × R
⊢ P.fst + r' + r = P.fst + (r + r') ∧
    P.snd + s' * P.fst + t' + s * (P.fst + r') + t = P.snd + (s + s') * P.fst + (t + t' + s * r')
Tactic:
apply And.intro <;>
ring
Proof state after:
no goals
Theorem: Model.var_change_zero
Proof state before:
R : Type u
inst✝ : CommRing R
P : R × R
⊢ var_change 0 0 0 P = P
Tactic:
simp [var_change]
Proof state after:
no goals
Theorem: Model.weierstrass_iso_eq_var_change
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
P : R × R
⊢ weierstrass (rst_iso r s t e) P = weierstrass e (var_change r s t P)
Tactic:
simp only [weierstrass, rst_iso, var_change]
Proof state after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
P : R × R
⊢ P.snd ^ 2 + (e.a1 + 2 * s) * P.fst * P.snd + (e.a3 + r * e.a1 + 2 * t) * P.snd -
      (P.fst ^ 3 + (e.a2 - s * e.a1 + 3 * r - s * s) * P.fst ^ 2 +
          (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) * P.fst +
        (e.a6 + r * e.a4 + r * r * e.a2 + r * r * r - t * (e.a3 + t + r * e.a1))) =
    (P.snd + s * P.fst + t) ^ 2 + e.a1 * (P.fst + r) * (P.snd + s * P.fst + t) + e.a3 * (P.snd + s * P.fst + t) -
      ((P.fst + r) ^ 3 + e.a2 * (P.fst + r) ^ 2 + e.a4 * (P.fst + r) + e.a6)
Theorem: Model.weierstrass_iso_eq_var_change
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
P : R × R
⊢ P.snd ^ 2 + (e.a1 + 2 * s) * P.fst * P.snd + (e.a3 + r * e.a1 + 2 * t) * P.snd -
      (P.fst ^ 3 + (e.a2 - s * e.a1 + 3 * r - s * s) * P.fst ^ 2 +
          (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) * P.fst +
        (e.a6 + r * e.a4 + r * r * e.a2 + r * r * r - t * (e.a3 + t + r * e.a1))) =
    (P.snd + s * P.fst + t) ^ 2 + e.a1 * (P.fst + r) * (P.snd + s * P.fst + t) + e.a3 * (P.snd + s * P.fst + t) -
      ((P.fst + r) ^ 3 + e.a2 * (P.fst + r) ^ 2 + e.a4 * (P.fst + r) + e.a6)
Tactic:
ring
Proof state after:
no goals
Theorem: Model.dweierstrass_dx_iso_eq_var_change
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
P : R × R
⊢ dweierstrass_dx (rst_iso r s t e) P =
    dweierstrass_dx e (var_change r s t P) + s * dweierstrass_dy e (var_change r s t P)
Tactic:
simp only [dweierstrass_dx, dweierstrass_dy, rst_iso, var_change]
Proof state after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
P : R × R
⊢ (e.a1 + 2 * s) * P.snd -
      (3 * P.fst ^ 2 + 2 * (e.a2 - s * e.a1 + 3 * r - s * s) * P.fst +
        (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t)) =
    e.a1 * (P.snd + s * P.fst + t) - (3 * (P.fst + r) ^ 2 + 2 * e.a2 * (P.fst + r) + e.a4) +
      s * (2 * (P.snd + s * P.fst + t) + e.a1 * (P.fst + r) + e.a3)
Theorem: Model.dweierstrass_dx_iso_eq_var_change
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
P : R × R
⊢ (e.a1 + 2 * s) * P.snd -
      (3 * P.fst ^ 2 + 2 * (e.a2 - s * e.a1 + 3 * r - s * s) * P.fst +
        (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t)) =
    e.a1 * (P.snd + s * P.fst + t) - (3 * (P.fst + r) ^ 2 + 2 * e.a2 * (P.fst + r) + e.a4) +
      s * (2 * (P.snd + s * P.fst + t) + e.a1 * (P.fst + r) + e.a3)
Tactic:
ring
Proof state after:
no goals
Theorem: Model.dweierstrass_dy_iso_eq_var_change
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
P : R × R
⊢ dweierstrass_dy (rst_iso r s t e) P = dweierstrass_dy e (var_change r s t P)
Tactic:
simp only [dweierstrass_dy, rst_iso, var_change]
Proof state after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
P : R × R
⊢ 2 * P.snd + (e.a1 + 2 * s) * P.fst + (e.a3 + r * e.a1 + 2 * t) =
    2 * (P.snd + s * P.fst + t) + e.a1 * (P.fst + r) + e.a3
Theorem: Model.dweierstrass_dy_iso_eq_var_change
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
P : R × R
⊢ 2 * P.snd + (e.a1 + 2 * s) * P.fst + (e.a3 + r * e.a1 + 2 * t) =
    2 * (P.snd + s * P.fst + t) + e.a1 * (P.fst + r) + e.a3
Tactic:
ring
Proof state after:
no goals
Theorem: ValidModel.rt_of_a1
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
r t : R
⊢ (rst_iso r 0 t e).toModel.a1 = e.a1
Tactic:
simp only [rst_iso, Model.rst_iso, mul_zero, add_zero, one_mul]
Proof state after:
no goals
Theorem: ValidModel.t_of_a2
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
t : R
⊢ (rst_iso 0 0 t e).toModel.a2 = e.a2
Tactic:
simp only [rst_iso, Model.rst_iso, one_pow, zero_mul, sub_zero, mul_zero, add_zero, one_mul]
Proof state after:
no goals
Theorem: ValidModel.r_of_a2
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
r : R
⊢ (rst_iso r 0 0 e).toModel.a2 = e.a2 + 3 * r
Tactic:
simp only [rst_iso, Model.rst_iso, one_pow, zero_mul, sub_zero, mul_zero, add_zero, one_mul]
Proof state after:
no goals
Theorem: ValidModel.t_of_a3
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
t : R
⊢ (rst_iso 0 0 t e).toModel.a3 = e.a3 + 2 * t
Tactic:
simp only [rst_iso, Model.rst_iso, one_pow, zero_mul, sub_zero, mul_zero, add_zero, one_mul]
Proof state after:
no goals
Theorem: ValidModel.r_of_a3
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
r : R
⊢ (rst_iso r 0 0 e).toModel.a3 = e.a3 + r * e.a1
Tactic:
simp only [rst_iso, Model.rst_iso, one_pow, zero_mul, sub_zero, mul_zero, add_zero, one_mul]
Proof state after:
no goals
Theorem: ValidModel.t_of_a4
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
t : R
⊢ (rst_iso 0 0 t e).toModel.a4 = e.a4 - t * e.a1
Tactic:
simp only [rst_iso, Model.rst_iso, one_pow, zero_mul, sub_zero, mul_zero, add_zero, one_mul]
Proof state after:
no goals
Theorem: ValidModel.r_of_a4
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
r : R
⊢ (rst_iso r 0 0 e).toModel.a4 = e.a4 + 2 * r * e.a2 + 3 * r ^ 2
Tactic:
simp only [rst_iso, Model.rst_iso, one_pow, zero_mul,
sub_zero, mul_zero, one_mul, add_zero, mul_assoc, ←pow_two r]
Proof state after:
no goals
Theorem: ValidModel.t_of_a6
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
t : R
⊢ (rst_iso 0 0 t e).toModel.a6 = e.a6 - t * e.a3 - t ^ 2
Tactic:
simp only [rst_iso, Model.rst_iso, one_pow, zero_mul, sub_zero, mul_zero,
one_mul, add_zero, mul_add, ←pow_two t, sub_eq_add_neg, neg_add, ←add_assoc]
Proof state after:
no goals
Theorem: ValidModel.r_of_a6
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
r : R
⊢ (rst_iso r 0 0 e).toModel.a6 = e.a6 + r * e.a4 + r ^ 2 * e.a2 + r ^ 3
Tactic:
simp only [rst_iso, Model.rst_iso, one_pow, zero_mul, sub_zero,
mul_zero, one_mul, add_zero, mul_assoc, pow_two r, pow_succ r, pow_zero, mul_one]
Proof state after:
no goals
Theorem: ValidModel.st_of_a1
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
s t : R
⊢ (rst_iso 0 s t e).toModel.a1 = e.a1 + 2 * s
Tactic:
simp only [rst_iso, Model.rst_iso, one_pow, mul_zero, one_mul]
Proof state after:
no goals
Theorem: ValidModel.st_of_a2
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
s t : R
⊢ (rst_iso 0 s t e).toModel.a2 = e.a2 - s * e.a1 - s ^ 2
Tactic:
simp only [rst_iso, Model.rst_iso, one_pow, mul_zero, one_mul, add_zero, mul_assoc, ←pow_two s]
Proof state after:
no goals
Theorem: ValidModel.st_of_a3
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
s t : R
⊢ (rst_iso 0 s t e).toModel.a3 = e.a3 + 2 * t
Tactic:
simp only [rst_iso, Model.rst_iso, one_pow, mul_zero, one_mul, add_zero, mul_assoc, zero_mul]
Proof state after:
no goals
Theorem: ValidModel.st_of_a4
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
s t : R
⊢ (rst_iso 0 s t e).toModel.a4 = e.a4 - s * e.a3 - t * e.a1 - 2 * s * t
Tactic:
simp only [rst_iso, Model.rst_iso, one_pow, mul_zero, one_mul, add_zero, mul_assoc, zero_mul]
Proof state after:
no goals
Theorem: ValidModel.st_of_a6
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
s t : R
⊢ (rst_iso 0 s t e).toModel.a6 = e.a6 - t * e.a3 - t ^ 2
Tactic:
simp only [rst_iso, Model.rst_iso, one_pow, mul_zero, one_mul,
add_zero, mul_assoc, ←pow_two t, zero_mul, mul_add, sub_sub]
Proof state after:
no goals
Theorem: ValidModel.st_of_b8
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
s t : R
⊢ Model.b8 (rst_iso 0 s t e).toModel = Model.b8 e.toModel
Tactic:
rw [rst_iso, Model.rst_b8]
Proof state after:
R : Type u
inst✝ : CommRing R
e : ValidModel R
s t : R
⊢ Model.b8 e.toModel + 3 * 0 * Model.b6 e.toModel + 3 * 0 * 0 * Model.b4 e.toModel + 0 * 0 * 0 * Model.b2 e.toModel +
      3 * 0 * 0 * 0 * 0 =
    Model.b8 e.toModel
Theorem: ValidModel.st_of_b8
Proof state before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
s t : R
⊢ Model.b8 e.toModel + 3 * 0 * Model.b6 e.toModel + 3 * 0 * 0 * Model.b4 e.toModel + 0 * 0 * 0 * Model.b2 e.toModel +
      3 * 0 * 0 * 0 * 0 =
    Model.b8 e.toModel
Tactic:
simp only [mul_zero, add_zero, zero_mul]
Proof state after:
no goals
Theorem: Model.discr_eq_zero_of_singular
Proof state before:
K : Type u
inst✝ : CommRing K
e : Model K
P : K × K
h : is_singular_point e P
⊢ discr e = 0
Tactic:
rcases h with ⟨h₁, h₂, h₃⟩
Proof state after:
case intro.intro
K : Type u
inst✝ : CommRing K
e : Model K
P : K × K
h₁ : weierstrass e P = 0
h₂ : dweierstrass_dx e P = 0
h₃ : dweierstrass_dy e P = 0
⊢ discr e = 0
Theorem: Model.discr_eq_zero_of_singular
Proof state before:
case intro.intro
K : Type u
inst✝ : CommRing K
e : Model K
P : K × K
h₁ : weierstrass e P = 0
h₂ : dweierstrass_dx e P = 0
h₃ : dweierstrass_dy e P = 0
⊢ discr e = 0
Tactic:
rw [discr_in_jacobian_ideal, h₁, h₂, h₃, mul_zero,
  mul_zero, mul_zero, add_zero, add_zero, neg_eq_zero]
Proof state after:
no goals
Theorem: Model.c4_zero_iff_a1_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
⊢ c4 e = 0 ↔ e.a1 = 0
Tactic:
have hchar' : (ringChar K : K) = 2 := by simp [h]
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
⊢ c4 e = 0 ↔ e.a1 = 0
Theorem: Model.c4_zero_iff_a1_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
⊢ c4 e = 0 ↔ e.a1 = 0
Tactic:
have hchar'' : (2 : K) = 0 := by simp [← hchar', ringChar.Nat.cast_ringChar]
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ c4 e = 0 ↔ e.a1 = 0
Theorem: Model.c4_zero_iff_a1_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ c4 e = 0 ↔ e.a1 = 0
Tactic:
rw [c4, b2, show (24 : K) = 2 * 12 by norm_num, show (4 : K) = 2 * 2 by norm_num, hchar'', ← pow_two]
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ (e.a1 ^ 2 + 0 * 0 * e.a2) ^ 2 - 0 * 12 * b4 e = 0 ↔ e.a1 = 0
Theorem: Model.c4_zero_iff_a1_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ (e.a1 ^ 2 + 0 * 0 * e.a2) ^ 2 - 0 * 12 * b4 e = 0 ↔ e.a1 = 0
Tactic:
simp only [mul_zero, zero_mul, add_zero, ← pow_mul, sub_zero]
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ e.a1 ^ (2 * 2) = 0 ↔ e.a1 = 0
Theorem: Model.c4_zero_iff_a1_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ e.a1 ^ (2 * 2) = 0 ↔ e.a1 = 0
Tactic:
rw [pow_eq_zero_iff]
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ 0 < 2 * 2
Theorem: Model.c4_zero_iff_a1_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ 0 < 2 * 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Model.c4_zero_iff_a1_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
⊢ ↑(ringChar K) = 2
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Model.c4_zero_iff_a1_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
⊢ 2 = 0
Tactic:
simp [← hchar', ringChar.Nat.cast_ringChar]
Proof state after:
no goals
Theorem: Model.c4_zero_iff_a1_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ 24 = 2 * 12
Tactic:
norm_num
Proof state after:
no goals
Theorem: Model.c4_zero_iff_a1_zero_of_char_two
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ 4 = 2 * 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Model.c4_zero_iff_b2_zero_of_char_three
Proof state before:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
⊢ c4 e = 0 ↔ b2 e = 0
Tactic:
have hchar' : (ringChar K : K) = 3 := by simp [h]
Proof state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 3
hchar' : ↑(ringChar K) = 3
⊢ c4 e = 0 ↔ b2 e = 0