internlm/Lean-Github huggingface dataset:
Theorem: Int.odd_part_nat_pos
Proof state before:
x : ℕ
⊢ x ≠ 0 → 0 < (val_bin_nat x).snd
Tactic:
cases x with
| zero =>
  intro absurd
  apply False.elim
  apply absurd
  rfl
| succ x =>
  intro _
  exact odd_part_succ_pos x
Proof state after:
no goals
Theorem: Int.odd_part_nat_pos
Proof state before:
case zero

⊢ zero ≠ 0 → 0 < (val_bin_nat zero).snd
Tactic:
intro absurd
Proof state after:
case zero
absurd : zero ≠ 0
⊢ 0 < (val_bin_nat zero).snd
Theorem: Int.odd_part_nat_pos
Proof state before:
case zero
absurd : zero ≠ 0
⊢ 0 < (val_bin_nat zero).snd
Tactic:
apply False.elim
Proof state after:
case zero.h
absurd : zero ≠ 0
⊢ False
Theorem: Int.odd_part_nat_pos
Proof state before:
case zero.h
absurd : zero ≠ 0
⊢ False
Tactic:
apply absurd
Proof state after:
case zero.h
absurd : zero ≠ 0
⊢ zero = 0
Theorem: Int.odd_part_nat_pos
Proof state before:
case zero.h
absurd : zero ≠ 0
⊢ zero = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Int.odd_part_nat_pos
Proof state before:
case succ
x : ℕ
⊢ Nat.succ x ≠ 0 → 0 < (val_bin_nat (Nat.succ x)).snd
Tactic:
intro _
Proof state after:
case succ
x : ℕ
a✝ : Nat.succ x ≠ 0
⊢ 0 < (val_bin_nat (Nat.succ x)).snd
Theorem: Int.odd_part_nat_pos
Proof state before:
case succ
x : ℕ
a✝ : Nat.succ x ≠ 0
⊢ 0 < (val_bin_nat (Nat.succ x)).snd
Tactic:
exact odd_part_succ_pos x
Proof state after:
no goals
Theorem: QuadRing.coe_inj
Proof state before:
F : Type u_1
a b : F
inst✝ : Zero F
z w : F
⊢ z = w → { b1 := z, b2 := 0 } = { b1 := w, b2 := 0 }
Tactic:
aesop
Proof state after:
no goals
Theorem: QuadRing.coe_add
Proof state before:
F : Type u_1
a b : F
inst✝ : CommRing F
r s : F
⊢ { b1 := r + s, b2 := 0 }.b1 = ({ b1 := r, b2 := 0 } + { b1 := s, b2 := 0 }).b1 ∧
    { b1 := r + s, b2 := 0 }.b2 = ({ b1 := r, b2 := 0 } + { b1 := s, b2 := 0 }).b2
Tactic:
simp
Proof state after:
no goals
Theorem: QuadRing.coe_neg
Proof state before:
F : Type u_1
a b : F
inst✝ : CommRing F
n : F
⊢ { b1 := -n, b2 := 0 } = -{ b1 := n, b2 := 0 }
Tactic:
ext
Proof state after:
case b1
F : Type u_1
a b : F
inst✝ : CommRing F
n : F
⊢ { b1 := -n, b2 := 0 }.b1 = (-{ b1 := n, b2 := 0 }).b1

case b2
F : Type u_1
a b : F
inst✝ : CommRing F
n : F
⊢ { b1 := -n, b2 := 0 }.b2 = (-{ b1 := n, b2 := 0 }).b2
Theorem: QuadRing.coe_neg
Proof state before:
case b1
F : Type u_1
a b : F
inst✝ : CommRing F
n : F
⊢ { b1 := -n, b2 := 0 }.b1 = (-{ b1 := n, b2 := 0 }).b1

case b2
F : Type u_1
a b : F
inst✝ : CommRing F
n : F
⊢ { b1 := -n, b2 := 0 }.b2 = (-{ b1 := n, b2 := 0 }).b2
Tactic:
simp
Proof state after:
case b2
F : Type u_1
a b : F
inst✝ : CommRing F
n : F
⊢ { b1 := -n, b2 := 0 }.b2 = (-{ b1 := n, b2 := 0 }).b2
Theorem: QuadRing.coe_neg
Proof state before:
case b2
F : Type u_1
a b : F
inst✝ : CommRing F
n : F
⊢ { b1 := -n, b2 := 0 }.b2 = (-{ b1 := n, b2 := 0 }).b2
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadRing.coe_sub
Proof state before:
F : Type u_1
a b : F
inst✝ : CommRing F
z w : F
⊢ { b1 := z - w, b2 := 0 } = { b1 := z, b2 := 0 } - { b1 := w, b2 := 0 }
Tactic:
ext
Proof state after:
case b1
F : Type u_1
a b : F
inst✝ : CommRing F
z w : F
⊢ { b1 := z - w, b2 := 0 }.b1 = ({ b1 := z, b2 := 0 } - { b1 := w, b2 := 0 }).b1

case b2
F : Type u_1
a b : F
inst✝ : CommRing F
z w : F
⊢ { b1 := z - w, b2 := 0 }.b2 = ({ b1 := z, b2 := 0 } - { b1 := w, b2 := 0 }).b2
Theorem: QuadRing.coe_sub
Proof state before:
case b1
F : Type u_1
a b : F
inst✝ : CommRing F
z w : F
⊢ { b1 := z - w, b2 := 0 }.b1 = ({ b1 := z, b2 := 0 } - { b1 := w, b2 := 0 }).b1

case b2
F : Type u_1
a b : F
inst✝ : CommRing F
z w : F
⊢ { b1 := z - w, b2 := 0 }.b2 = ({ b1 := z, b2 := 0 } - { b1 := w, b2 := 0 }).b2
Tactic:
simp
Proof state after:
case b2
F : Type u_1
a b : F
inst✝ : CommRing F
z w : F
⊢ { b1 := z - w, b2 := 0 }.b2 = ({ b1 := z, b2 := 0 } - { b1 := w, b2 := 0 }).b2
Theorem: QuadRing.coe_sub
Proof state before:
case b2
F : Type u_1
a b : F
inst✝ : CommRing F
z w : F
⊢ { b1 := z - w, b2 := 0 }.b2 = ({ b1 := z, b2 := 0 } - { b1 := w, b2 := 0 }).b2
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadRing.coe_nat_add
Proof state before:
F : Type u_1
a b : F
inst✝ : CommRing F
r s : ℕ
⊢ ↑(r + s) = ↑r + ↑s
Tactic:
ext <;> simp only [coe_nat_b1, coe_nat_b2, add_b1, add_b2, Nat.cast_add, add_zero]
Proof state after:
no goals
Theorem: QuadRing.coe_int_add
Proof state before:
F : Type u_1
a b : F
inst✝ : CommRing F
r s : ℤ
⊢ ↑(r + s) = ↑r + ↑s
Tactic:
ext <;> simp only [coe_int_b1, coe_int_b2, add_b1, add_b2, Int.cast_add, add_zero]
Proof state after:
no goals
Theorem: QuadRing.coe_mul
Proof state before:
F : Type u_1
a b : F
inst✝ : CommRing F
r s : F
⊢ { b1 := r * s, b2 := 0 } = { b1 := r, b2 := 0 } * { b1 := s, b2 := 0 }
Tactic:
apply (QuadRing.ext_iff _ _).2
Proof state after:
F : Type u_1
a b : F
inst✝ : CommRing F
r s : F
⊢ { b1 := r * s, b2 := 0 }.b1 = ({ b1 := r, b2 := 0 } * { b1 := s, b2 := 0 }).b1 ∧
    { b1 := r * s, b2 := 0 }.b2 = ({ b1 := r, b2 := 0 } * { b1 := s, b2 := 0 }).b2
Theorem: QuadRing.coe_mul
Proof state before:
F : Type u_1
a b : F
inst✝ : CommRing F
r s : F
⊢ { b1 := r * s, b2 := 0 }.b1 = ({ b1 := r, b2 := 0 } * { b1 := s, b2 := 0 }).b1 ∧
    { b1 := r * s, b2 := 0 }.b2 = ({ b1 := r, b2 := 0 } * { b1 := s, b2 := 0 }).b2
Tactic:
simp [mul_comm]
Proof state after:
no goals
Theorem: ECTate.PerfectRing.pth_root_pow_char
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h : ringChar R ≠ 0
x : R
⊢ pth_root x ^ ringChar R = x
Tactic:
simp only [pth_root, h, dite_false]
Proof state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h : ringChar R ≠ 0
x : R
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) x ^ ringChar R = x
Theorem: ECTate.PerfectRing.pth_root_pow_char
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h : ringChar R ≠ 0
x : R
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) x ^ ringChar R = x
Tactic:
exact Function.rightInverse_surjInv (pth_power_bijective_of_char_nonzero h).2 x
Proof state after:
no goals
Theorem: ECTate.PerfectRing.pth_root_pow_eq
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)
Tactic:
by_cases h : ringChar R = 0
Proof state after:
case pos
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)

case neg
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ¬ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)
Theorem: ECTate.PerfectRing.pth_root_pow_eq
Proof state before:
case pos
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)

case neg
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ¬ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)
Tactic:
. simp [h]
Proof state after:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ¬ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)
Theorem: ECTate.PerfectRing.pth_root_pow_eq
Proof state before:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ¬ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)
Tactic:
conv =>
  lhs
  rw [← Nat.mod_add_div n (ringChar R)]
Proof state after:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ¬ringChar R = 0
⊢ pth_root x ^ (n % ringChar R + ringChar R * (n / ringChar R)) = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)
Theorem: ECTate.PerfectRing.pth_root_pow_eq
Proof state before:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ¬ringChar R = 0
⊢ pth_root x ^ (n % ringChar R + ringChar R * (n / ringChar R)) = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)
Tactic:
rw [pow_add, pow_mul, pth_root_pow_char h, mul_comm]
Proof state after:
no goals
Theorem: ECTate.PerfectRing.pth_root_pow_eq
Proof state before:
case pos
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)
Tactic:
simp [h]
Proof state after:
no goals
Theorem: ECTate.PerfectRing.pth_root_zero
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
⊢ pth_root 0 = 0
Tactic:
rw [pth_root]
Proof state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
⊢ dite (ringChar R = 0) (fun h => id) (fun h => Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R)) 0 =
    0
Theorem: ECTate.PerfectRing.pth_root_zero
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
⊢ dite (ringChar R = 0) (fun h => id) (fun h => Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R)) 0 =
    0
Tactic:
split
Proof state after:
case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ringChar R = 0
⊢ id 0 = 0

case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0 = 0
Theorem: ECTate.PerfectRing.pth_root_zero
Proof state before:
case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ringChar R = 0
⊢ id 0 = 0

case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0 = 0
Tactic:
. simp
Proof state after:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0 = 0
Theorem: ECTate.PerfectRing.pth_root_zero
Proof state before:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0 = 0
Tactic:
. apply_fun (fun x : R => x ^ ringChar R)
  . simp only [ne_eq]
    rw [Function.surjInv_eq
          (pth_power_bijective_of_char_nonzero (by assumption)).surjective,
        zero_pow]
    rwa [zero_lt_iff]
  . exact (pth_power_bijective_of_char_nonzero (by assumption)).injective
Proof state after:
no goals
Theorem: ECTate.PerfectRing.pth_root_zero
Proof state before:
case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ringChar R = 0
⊢ id 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: ECTate.PerfectRing.pth_root_zero
Proof state before:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0 = 0
Tactic:
apply_fun (fun x : R => x ^ ringChar R)
Proof state after:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ (fun x => x ^ ringChar R) (Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0) =
    (fun x => x ^ ringChar R) 0

case inr.inj
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.Injective fun x => x ^ ringChar R
Theorem: ECTate.PerfectRing.pth_root_zero
Proof state before:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ (fun x => x ^ ringChar R) (Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0) =
    (fun x => x ^ ringChar R) 0

case inr.inj
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.Injective fun x => x ^ ringChar R
Tactic:
. simp only [ne_eq]
  rw [Function.surjInv_eq
        (pth_power_bijective_of_char_nonzero (by assumption)).surjective,
      zero_pow]
  rwa [zero_lt_iff]
Proof state after:
case inr.inj
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.Injective fun x => x ^ ringChar R
Theorem: ECTate.PerfectRing.pth_root_zero
Proof state before:
case inr.inj
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.Injective fun x => x ^ ringChar R
Tactic:
. exact (pth_power_bijective_of_char_nonzero (by assumption)).injective
Proof state after:
no goals
Theorem: ECTate.PerfectRing.pth_root_zero
Proof state before:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ (fun x => x ^ ringChar R) (Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0) =
    (fun x => x ^ ringChar R) 0
Tactic:
simp only [ne_eq]
Proof state after:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0 ^ ringChar R = 0 ^ ringChar R
Theorem: ECTate.PerfectRing.pth_root_zero
Proof state before:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0 ^ ringChar R = 0 ^ ringChar R
Tactic:
rw [Function.surjInv_eq
      (pth_power_bijective_of_char_nonzero (by assumption)).surjective,
    zero_pow]
Proof state after:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ 0 < ringChar R
Theorem: ECTate.PerfectRing.pth_root_zero
Proof state before:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ 0 < ringChar R
Tactic:
rwa [zero_lt_iff]
Proof state after:
no goals
Theorem: ECTate.PerfectRing.pth_root_zero
Proof state before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ ringChar R ≠ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: ECTate.PerfectRing.pth_root_zero
Proof state before:
case inr.inj
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.Injective fun x => x ^ ringChar R
Tactic:
exact (pth_power_bijective_of_char_nonzero (by assumption)).injective
Proof state after:
no goals
Theorem: Model.b8_identity
Proof state before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 4 * b8 e = b2 e * b6 e - b4 e ^ 2
Tactic:
simp only [b2, b4, b6, b8]
Proof state after:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 4 * (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) =
    (e.a1 * e.a1 + 4 * e.a2) * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a3 + 2 * e.a4) ^ 2
Theorem: Model.b8_identity
Proof state before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 4 * (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) =
    (e.a1 * e.a1 + 4 * e.a2) * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a3 + 2 * e.a4) ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: Model.discr_identity
Proof state before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 1728 * discr e = c4 e ^ 3 - c6 e ^ 2
Tactic:
simp only [c4, c6, discr, mul_sub, mul_add]
Proof state after:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 1728 * (-b2 e * b2 e * b8 e) - 1728 * (8 * b4 e ^ 3) - 1728 * (27 * b6 e * b6 e) + 1728 * (9 * b2 e * b4 e * b6 e) =
    (b2 e ^ 2 - 24 * b4 e) ^ 3 - (-b2 e ^ 3 + 36 * b2 e * b4 e - 216 * b6 e) ^ 2
Theorem: Model.discr_identity
Proof state before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 1728 * (-b2 e * b2 e * b8 e) - 1728 * (8 * b4 e ^ 3) - 1728 * (27 * b6 e * b6 e) + 1728 * (9 * b2 e * b4 e * b6 e) =
    (b2 e ^ 2 - 24 * b4 e) ^ 3 - (-b2 e ^ 3 + 36 * b2 e * b4 e - 216 * b6 e) ^ 2
Tactic:
rw [(by ring : 1728 * (-e.b2 * e.b2 * e.b8) = -432 * e.b2 * e.b2 * (4 * e.b8))]
Proof state after:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ -432 * b2 e * b2 e * (4 * b8 e) - 1728 * (8 * b4 e ^ 3) - 1728 * (27 * b6 e * b6 e) +
      1728 * (9 * b2 e * b4 e * b6 e) =
    (b2 e ^ 2 - 24 * b4 e) ^ 3 - (-b2 e ^ 3 + 36 * b2 e * b4 e - 216 * b6 e) ^ 2
Theorem: Model.discr_identity
Proof state before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ -432 * b2 e * b2 e * (4 * b8 e) - 1728 * (8 * b4 e ^ 3) - 1728 * (27 * b6 e * b6 e) +
      1728 * (9 * b2 e * b4 e * b6 e) =
    (b2 e ^ 2 - 24 * b4 e) ^ 3 - (-b2 e ^ 3 + 36 * b2 e * b4 e - 216 * b6 e) ^ 2
Tactic:
rw [b8_identity]
Proof state after:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ -432 * b2 e * b2 e * (b2 e * b6 e - b4 e ^ 2) - 1728 * (8 * b4 e ^ 3) - 1728 * (27 * b6 e * b6 e) +
      1728 * (9 * b2 e * b4 e * b6 e) =
    (b2 e ^ 2 - 24 * b4 e) ^ 3 - (-b2 e ^ 3 + 36 * b2 e * b4 e - 216 * b6 e) ^ 2
Theorem: Model.discr_identity
Proof state before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ -432 * b2 e * b2 e * (b2 e * b6 e - b4 e ^ 2) - 1728 * (8 * b4 e ^ 3) - 1728 * (27 * b6 e * b6 e) +
      1728 * (9 * b2 e * b4 e * b6 e) =
    (b2 e ^ 2 - 24 * b4 e) ^ 3 - (-b2 e ^ 3 + 36 * b2 e * b4 e - 216 * b6 e) ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: Model.discr_identity
Proof state before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 1728 * (-b2 e * b2 e * b8 e) = -432 * b2 e * b2 e * (4 * b8 e)
Tactic:
ring
Proof state after:
no goals
Theorem: Model.rst_b2
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ b2 (rst_iso r s t e) = b2 e + 12 * r
Tactic:
simp [rst_iso, b2]
Proof state after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ (e.a1 + 2 * s) * (e.a1 + 2 * s) + 4 * (e.a2 - s * e.a1 + 3 * r - s * s) = e.a1 * e.a1 + 4 * e.a2 + 12 * r
Theorem: Model.rst_b2
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ (e.a1 + 2 * s) * (e.a1 + 2 * s) + 4 * (e.a2 - s * e.a1 + 3 * r - s * s) = e.a1 * e.a1 + 4 * e.a2 + 12 * r
Tactic:
ring
Proof state after:
no goals
Theorem: Model.rst_b4
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ b4 (rst_iso r s t e) = b4 e + r * (b2 e + 6 * r)
Tactic:
simp only [rst_iso, b2, b4]
Proof state after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ (e.a1 + 2 * s) * (e.a3 + r * e.a1 + 2 * t) +
      2 * (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) =
    e.a1 * e.a3 + 2 * e.a4 + r * (e.a1 * e.a1 + 4 * e.a2 + 6 * r)
Theorem: Model.rst_b4
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ (e.a1 + 2 * s) * (e.a3 + r * e.a1 + 2 * t) +
      2 * (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) =
    e.a1 * e.a3 + 2 * e.a4 + r * (e.a1 * e.a1 + 4 * e.a2 + 6 * r)
Tactic:
ring
Proof state after:
no goals
Theorem: Model.rst_b6
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ b6 (rst_iso r s t e) = b6 e + 2 * r * b4 e + r * r * b2 e + 4 * r * r * r
Tactic:
simp only [rst_iso, b2, b4, b6]
Proof state after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ (e.a3 + r * e.a1 + 2 * t) * (e.a3 + r * e.a1 + 2 * t) +
      4 * (e.a6 + r * e.a4 + r * r * e.a2 + r * r * r - t * (e.a3 + t + r * e.a1)) =
    e.a3 * e.a3 + 4 * e.a6 + 2 * r * (e.a1 * e.a3 + 2 * e.a4) + r * r * (e.a1 * e.a1 + 4 * e.a2) + 4 * r * r * r
Theorem: Model.rst_b6
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ (e.a3 + r * e.a1 + 2 * t) * (e.a3 + r * e.a1 + 2 * t) +
      4 * (e.a6 + r * e.a4 + r * r * e.a2 + r * r * r - t * (e.a3 + t + r * e.a1)) =
    e.a3 * e.a3 + 4 * e.a6 + 2 * r * (e.a1 * e.a3 + 2 * e.a4) + r * r * (e.a1 * e.a1 + 4 * e.a2) + 4 * r * r * r
Tactic:
ring
Proof state after:
no goals
Theorem: Model.rst_b8
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ b8 (rst_iso r s t e) = b8 e + 3 * r * b6 e + 3 * r * r * b4 e + r * r * r * b2 e + 3 * r * r * r * r
Tactic:
simp only [rst_iso, b2, b4, b6, b8]
Proof state after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ (e.a1 + 2 * s) * (e.a1 + 2 * s) * (e.a6 + r * e.a4 + r * r * e.a2 + r * r * r - t * (e.a3 + t + r * e.a1)) -
            (e.a1 + 2 * s) * (e.a3 + r * e.a1 + 2 * t) *
              (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) +
          4 * (e.a2 - s * e.a1 + 3 * r - s * s) *
            (e.a6 + r * e.a4 + r * r * e.a2 + r * r * r - t * (e.a3 + t + r * e.a1)) +
        (e.a2 - s * e.a1 + 3 * r - s * s) * (e.a3 + r * e.a1 + 2 * t) * (e.a3 + r * e.a1 + 2 * t) -
      (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) *
        (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) =
    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 +
            3 * r * (e.a3 * e.a3 + 4 * e.a6) +
          3 * r * r * (e.a1 * e.a3 + 2 * e.a4) +
        r * r * r * (e.a1 * e.a1 + 4 * e.a2) +
      3 * r * r * r * r
Theorem: Model.rst_b8
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ (e.a1 + 2 * s) * (e.a1 + 2 * s) * (e.a6 + r * e.a4 + r * r * e.a2 + r * r * r - t * (e.a3 + t + r * e.a1)) -
            (e.a1 + 2 * s) * (e.a3 + r * e.a1 + 2 * t) *
              (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) +
          4 * (e.a2 - s * e.a1 + 3 * r - s * s) *
            (e.a6 + r * e.a4 + r * r * e.a2 + r * r * r - t * (e.a3 + t + r * e.a1)) +
        (e.a2 - s * e.a1 + 3 * r - s * s) * (e.a3 + r * e.a1 + 2 * t) * (e.a3 + r * e.a1 + 2 * t) -
      (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) *
        (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) =
    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 +
            3 * r * (e.a3 * e.a3 + 4 * e.a6) +
          3 * r * r * (e.a1 * e.a3 + 2 * e.a4) +
        r * r * r * (e.a1 * e.a1 + 4 * e.a2) +
      3 * r * r * r * r
Tactic:
ring
Proof state after:
no goals
Theorem: Model.rst_c4
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ c4 (rst_iso r s t e) = c4 e
Tactic:
simp only [rst_iso, b2, b4, b6, b8, c4]
Proof state after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ ((e.a1 + 2 * s) * (e.a1 + 2 * s) + 4 * (e.a2 - s * e.a1 + 3 * r - s * s)) ^ 2 -
      24 *
        ((e.a1 + 2 * s) * (e.a3 + r * e.a1 + 2 * t) +
          2 * (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t)) =
    (e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)
Theorem: Model.rst_c4
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ ((e.a1 + 2 * s) * (e.a1 + 2 * s) + 4 * (e.a2 - s * e.a1 + 3 * r - s * s)) ^ 2 -
      24 *
        ((e.a1 + 2 * s) * (e.a3 + r * e.a1 + 2 * t) +
          2 * (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t)) =
    (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.rst_c6
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ c6 (rst_iso r s t e) = c6 e
Tactic:
simp only [rst_iso, b2, b4, b6, b8, c6]
Proof state after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ -((e.a1 + 2 * s) * (e.a1 + 2 * s) + 4 * (e.a2 - s * e.a1 + 3 * r - s * s)) ^ 3 +
        36 * ((e.a1 + 2 * s) * (e.a1 + 2 * s) + 4 * (e.a2 - s * e.a1 + 3 * r - s * s)) *
          ((e.a1 + 2 * s) * (e.a3 + r * e.a1 + 2 * t) +
            2 * (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t)) -
      216 *
        ((e.a3 + r * e.a1 + 2 * t) * (e.a3 + r * e.a1 + 2 * t) +
          4 * (e.a6 + r * e.a4 + r * r * e.a2 + r * r * r - t * (e.a3 + t + r * e.a1))) =
    -(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.rst_c6
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ -((e.a1 + 2 * s) * (e.a1 + 2 * s) + 4 * (e.a2 - s * e.a1 + 3 * r - s * s)) ^ 3 +
        36 * ((e.a1 + 2 * s) * (e.a1 + 2 * s) + 4 * (e.a2 - s * e.a1 + 3 * r - s * s)) *
          ((e.a1 + 2 * s) * (e.a3 + r * e.a1 + 2 * t) +
            2 * (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t)) -
      216 *
        ((e.a3 + r * e.a1 + 2 * t) * (e.a3 + r * e.a1 + 2 * t) +
          4 * (e.a6 + r * e.a4 + r * r * e.a2 + r * r * r - t * (e.a3 + t + r * e.a1))) =
    -(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