awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
gp : Pair K
zeroth_s_eq : g.s.get? 0 = some gp
⊢ g.contsAux 2 = { a := gp.b * g.h + gp.a, b := gp.b }

Tactic:
simp [zeroth_s_eq, contsAux, nextConts, nextDen, nextNum]

Premises used: GenContFract.contsAux, GenContFract.nextDen, GenContFract.nextConts, GenContFract.nextNum
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
gp : Pair K
zeroth_s_eq : g.s.get? 0 = some gp
⊢ g.conts 1 = { a := gp.b * g.h + gp.a, b := gp.b }

Tactic:
simp [nth_cont_eq_succ_nth_contAux, second_contAux_eq zeroth_s_eq]

Premises used: GenContFract.nth_cont_eq_succ_nth_contAux, GenContFract.second_contAux_eq
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
gp : Pair K
zeroth_s_eq : g.s.get? 0 = some gp
⊢ g.nums 1 = gp.b * g.h + gp.a

Tactic:
simp [num_eq_conts_a, first_cont_eq zeroth_s_eq]

Premises used: GenContFract.first_cont_eq, GenContFract.num_eq_conts_a
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
gp : Pair K
zeroth_s_eq : g.s.get? 0 = some gp
⊢ g.dens 1 = gp.b

Tactic:
simp [den_eq_conts_b, first_cont_eq zeroth_s_eq]

Premises used: GenContFract.first_cont_eq, GenContFract.den_eq_conts_b
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
inst : DivisionRing K
s : Stream'.Seq (Pair K)
⊢ convs'Aux s 0 = 0

Tactic:
rfl

Premises used: GenContFract.convs'Aux, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
⊢ g.convs' 0 = g.h

Tactic:
simp [convs']

Premises used: GenContFract.convs'
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
inst : DivisionRing K
s : Stream'.Seq (Pair K)
h : s.head = none
n : ℕ
⊢ convs'Aux s (n + 1) = 0

Tactic:
simp [convs'Aux, h]

Premises used: GenContFract.convs'Aux
-- Module: Mathlib.Algebra.ContinuedFractions.Translations
Goal:
K : Type u_1
inst : DivisionRing K
s : Stream'.Seq (Pair K)
p : Pair K
h : s.head = some p
n : ℕ
⊢ convs'Aux s (n + 1) = p.a / (p.b + convs'Aux s.tail n)

Tactic:
simp [convs'Aux, h]

Premises used: GenContFract.convs'Aux
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
S : Type u_2
inst : CommRing S
w x y z : S
simp :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X])
          (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X]) (HPow.hPow (α := S[X]) (β := ℕ) X 3) +
          HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X])
              (-HAdd.hAdd (β := S[X])
                  (HAdd.hAdd (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) ((C : (a : S) → S[X]) y : S[X]))
                  ((C : (a : S) → S[X]) z : S[X])) *
            HPow.hPow (α := S[X]) (β := ℕ) X 2 +
        HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X])
            (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) ((C : (a : S) → S[X]) y : S[X]) +
                HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) ((C : (a : S) → S[X]) z : S[X]) +
              HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) y : S[X]) ((C : (a : S) → S[X]) z : S[X])) *
          X +
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X])
        (-HMul.hMul (β := S[X])
            (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) ((C : (a : S) → S[X]) y : S[X]))
            ((C : (a : S) → S[X]) z : S[X]))
⊢ HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X])
          (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := w, b := w * -(x + y + z), c := w * (x * y + x * z + y * z), d := w * -(x * y * z) }.toPoly

Tactic:
simp only [toPoly, C_neg, C_add, C_mul]

Premises used: Cubic.toPoly, Polynomial.C_mul, Polynomial.C_neg, Polynomial.C_add
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
S : Type u_2
inst : CommRing S
w x y z : S
⊢ HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X])
          (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X]) (HPow.hPow (α := S[X]) (β := ℕ) X 3) +
          HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X])
              (-HAdd.hAdd (β := S[X])
                  (HAdd.hAdd (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) ((C : (a : S) → S[X]) y : S[X]))
                  ((C : (a : S) → S[X]) z : S[X])) *
            HPow.hPow (α := S[X]) (β := ℕ) X 2 +
        HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X])
            (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) ((C : (a : S) → S[X]) y : S[X]) +
                HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) ((C : (a : S) → S[X]) z : S[X]) +
              HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) y : S[X]) ((C : (a : S) → S[X]) z : S[X])) *
          X +
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X])
        (-HMul.hMul (β := S[X])
            (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) ((C : (a : S) → S[X]) y : S[X]))
            ((C : (a : S) → S[X]) z : S[X]))

Tactic:
ring1
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
S : Type u_2
inst : CommRing S
x y z : S
rw :
  1 * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
rw₁ :
  (C : (a : S) → S[X]) 1 * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
rw₂ :
  Eq (α := S[X]) { a := 1, b := 1 * -(x + y + z), c := 1 * (x * y + x * z + y * z), d := 1 * -(x * y * z) }.toPoly
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
rw₃ :
  Eq (α := S[X]) { a := 1, b := -(x + y + z), c := 1 * (x * y + x * z + y * z), d := 1 * -(x * y * z) }.toPoly
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
rw₄ :
  Eq (α := S[X]) { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := 1 * -(x * y * z) }.toPoly
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
rw₅ rw₆ :
  Eq (α := S[X]) { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
⊢ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly

Tactic:
rw [← one_mul <| X - C x, ← C_1, C_mul_prod_X_sub_C_eq, one_mul, one_mul, one_mul]

Premises used: Polynomial.C, Polynomial.C_1, Polynomial.X, Cubic.C_mul_prod_X_sub_C_eq, DFunLike.coe, one_mul
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
simp :
  (∀ n > 3,
      ((((if n = 3 then P.a else 0) + if n = 2 then P.b else 0) + if n = 1 then P.c else 0) +
          if n = 0 then P.d else 0) =
        0) ∧
    ((((if True then P.a else 0) + if Eq (α := ℕ) 3 2 then P.b else 0) + if Eq (α := ℕ) 3 1 then P.c else 0) +
          if Eq (α := ℕ) 3 0 then P.d else 0) =
        P.a ∧
      ((((if Eq (α := ℕ) 2 3 then P.a else 0) + if True then P.b else 0) + if Eq (α := ℕ) 2 1 then P.c else 0) +
            if Eq (α := ℕ) 2 0 then P.d else 0) =
          P.b ∧
        ((((if Eq (α := ℕ) 1 3 then P.a else 0) + if Eq (α := ℕ) 1 2 then P.b else 0) + if True then P.c else 0) +
              if Eq (α := ℕ) 1 0 then P.d else 0) =
            P.c ∧
          ((((if Eq (α := ℕ) 0 3 then P.a else 0) + if Eq (α := ℕ) 0 2 then P.b else 0) +
                if Eq (α := ℕ) 0 1 then P.c else 0) +
              if True then P.d else 0) =
            P.d
⊢ (∀ n > 3, coeff P.toPoly n = 0) ∧
    coeff P.toPoly 3 = P.a ∧ coeff P.toPoly 2 = P.b ∧ coeff P.toPoly 1 = P.c ∧ coeff P.toPoly 0 = P.d

Tactic:
simp only [Cubic.toPoly, Polynomial.coeff_add, Polynomial.coeff_C, Polynomial.coeff_C_mul_X,
    Polynomial.coeff_C_mul_X_pow]

Premises used: Polynomial.coeff_C_mul_X, Cubic.toPoly, Polynomial.coeff_add, Polynomial.coeff_C, Polynomial.coeff_C_mul_X_pow
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
⊢ (∀ n > 3,
      ((((if n = 3 then P.a else 0) + if n = 2 then P.b else 0) + if n = 1 then P.c else 0) +
          if n = 0 then P.d else 0) =
        0) ∧
    ((((if True then P.a else 0) + if Eq (α := ℕ) 3 2 then P.b else 0) + if Eq (α := ℕ) 3 1 then P.c else 0) +
          if Eq (α := ℕ) 3 0 then P.d else 0) =
        P.a ∧
      ((((if Eq (α := ℕ) 2 3 then P.a else 0) + if True then P.b else 0) + if Eq (α := ℕ) 2 1 then P.c else 0) +
            if Eq (α := ℕ) 2 0 then P.d else 0) =
          P.b ∧
        ((((if Eq (α := ℕ) 1 3 then P.a else 0) + if Eq (α := ℕ) 1 2 then P.b else 0) + if True then P.c else 0) +
              if Eq (α := ℕ) 1 0 then P.d else 0) =
            P.c ∧
          ((((if Eq (α := ℕ) 0 3 then P.a else 0) + if Eq (α := ℕ) 0 2 then P.b else 0) +
                if Eq (α := ℕ) 0 1 then P.c else 0) +
              if True then P.d else 0) =
            P.d

Tactic:
grind [zero_add]

Premises used: zero_add
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
n : ℕ
hn : 3 < n
⊢ coeff P.toPoly n = 0

Tactic:
coeffs.1 n hn

Premises used: _private.0.Cubic.coeffs, And.left
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
⊢ coeff P.toPoly 3 = P.a

Tactic:
coeffs.2.1

Premises used: _private.0.Cubic.coeffs, And.right, And.left
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
⊢ coeff P.toPoly 2 = P.b

Tactic:
coeffs.2.2.1

Premises used: _private.0.Cubic.coeffs, And.right, And.left
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
⊢ coeff P.toPoly 1 = P.c

Tactic:
coeffs.2.2.2.1

Premises used: _private.0.Cubic.coeffs, And.right, And.left
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
⊢ coeff P.toPoly 0 = P.d

Tactic:
coeffs.2.2.2.2

Premises used: _private.0.Cubic.coeffs, And.right
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P Q : Cubic R
inst : Semiring R
h : Eq (α := R[X]) P.toPoly Q.toPoly
rw : coeff P.toPoly 3 = Q.a
rw₁ : coeff Q.toPoly 3 = Q.a
rw₂ rw₃ : Q.a = Q.a
⊢ P.a = Q.a

Tactic:
rw [← coeff_eq_a, h, coeff_eq_a]

Premises used: Cubic.coeff_eq_a
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P Q : Cubic R
inst : Semiring R
h : Eq (α := R[X]) P.toPoly Q.toPoly
rw : coeff P.toPoly 2 = Q.b
rw₁ : coeff Q.toPoly 2 = Q.b
rw₂ rw₃ : Q.b = Q.b
⊢ P.b = Q.b

Tactic:
rw [← coeff_eq_b, h, coeff_eq_b]

Premises used: Cubic.coeff_eq_b
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P Q : Cubic R
inst : Semiring R
h : Eq (α := R[X]) P.toPoly Q.toPoly
rw : coeff P.toPoly 1 = Q.c
rw₁ : coeff Q.toPoly 1 = Q.c
rw₂ rw₃ : Q.c = Q.c
⊢ P.c = Q.c

Tactic:
rw [← coeff_eq_c, h, coeff_eq_c]

Premises used: Cubic.coeff_eq_c
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P Q : Cubic R
inst : Semiring R
h : Eq (α := R[X]) P.toPoly Q.toPoly
rw : coeff P.toPoly 0 = Q.d
rw₁ : coeff Q.toPoly 0 = Q.d
rw₂ rw₃ : Q.d = Q.d
⊢ P.d = Q.d

Tactic:
rw [← coeff_eq_d, h, coeff_eq_d]

Premises used: Cubic.coeff_eq_d
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
inst : Semiring R
P Q : Cubic R
⊢ Eq (α := R[X]) P.toPoly Q.toPoly ↔ P = Q

Tactic:
⟨fun h ↦ Cubic.ext (a_of_eq h) (b_of_eq h) (c_of_eq h) (d_of_eq h), congr_arg toPoly⟩

Premises used: Cubic.d_of_eq, Cubic.a_of_eq, Cubic.toPoly, congr_arg, Iff.intro, Cubic.b_of_eq, Cubic.c_of_eq, Cubic.ext
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
b c d : R
inst : Semiring R
⊢ { a := 0, b := b, c := c, d := d }.toPoly =
    HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
      ((C : (a : R) → R[X]) d : R[X])

Tactic:
of_a_eq_zero rfl

Premises used: Cubic.of_a_eq_zero, rfl
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 0
hb : P.b = 0
rw :
  HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) P.b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) P.c : R[X]) X)
      ((C : (a : R) → R[X]) P.d : R[X]) =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) P.c : R[X]) X)
      ((C : (a : R) → R[X]) P.d : R[X])
rw₁ :
  HAdd.hAdd (β := R[X])
      ((C : (a : R) → R[X]) 0 * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) P.c : R[X]) X)
      ((C : (a : R) → R[X]) P.d : R[X]) =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) P.c : R[X]) X)
      ((C : (a : R) → R[X]) P.d : R[X])
rw₂ :
  HAdd.hAdd (β := R[X])
      (0 * HPow.hPow (α := R[X]) (β := ℕ) X 2 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) P.c : R[X]) X)
      ((C : (a : R) → R[X]) P.d : R[X]) =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) P.c : R[X]) X)
      ((C : (a : R) → R[X]) P.d : R[X])
rw₃ :
  HAdd.hAdd (β := R[X]) (0 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) P.c : R[X]) X)
      ((C : (a : R) → R[X]) P.d : R[X]) =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) P.c : R[X]) X)
      ((C : (a : R) → R[X]) P.d : R[X])
rw₄ rw₅ :
  HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) P.c : R[X]) X)
      ((C : (a : R) → R[X]) P.d : R[X]) =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) P.c : R[X]) X)
      ((C : (a : R) → R[X]) P.d : R[X])
⊢ P.toPoly =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) P.c : R[X]) X)
      ((C : (a : R) → R[X]) P.d : R[X])

Tactic:
rw [of_a_eq_zero ha, hb, C_0, zero_mul, zero_add]

Premises used: Polynomial.C_0, MulZeroClass.zero_mul, Cubic.of_a_eq_zero, zero_add
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
c d : R
inst : Semiring R
⊢ { a := 0, b := 0, c := c, d := d }.toPoly =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X)
      ((C : (a : R) → R[X]) d : R[X])

Tactic:
of_b_eq_zero rfl rfl

Premises used: Cubic.of_b_eq_zero, rfl
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
rw :
  HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) P.c : R[X]) X)
      ((C : (a : R) → R[X]) P.d : R[X]) =
    (C : (a : R) → R[X]) P.d
rw₁ :
  HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 0) X) ((C : (a : R) → R[X]) P.d : R[X]) =
    (C : (a : R) → R[X]) P.d
rw₂ : HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) 0 X) ((C : (a : R) → R[X]) P.d : R[X]) = (C : (a : R) → R[X]) P.d
rw₃ : HAdd.hAdd (α := R[X]) (β := R[X]) (0 : R[X]) ((C : (a : R) → R[X]) P.d : R[X]) = (C : (a : R) → R[X]) P.d
rw₄ rw₅ : Eq (α := R[X]) ((C : (a : R) → R[X]) P.d : R[X]) ((C : (a : R) → R[X]) P.d : R[X])
⊢ Eq (α := R[X]) P.toPoly ((C : (a : R) → R[X]) P.d)

Tactic:
rw [of_b_eq_zero ha hb, hc, C_0, zero_mul, zero_add]

Premises used: Polynomial.C_0, MulZeroClass.zero_mul, Cubic.of_b_eq_zero, zero_add
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
d : R
inst : Semiring R
⊢ Eq (α := R[X]) { a := 0, b := 0, c := 0, d := d }.toPoly ((C : (a : R) → R[X]) d)

Tactic:
of_c_eq_zero rfl rfl rfl

Premises used: Cubic.of_c_eq_zero, rfl
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d = 0
rw : Eq (α := R[X]) ((C : (a : R) → R[X]) P.d : R[X]) (0 : R[X])
rw₁ : Eq.{u_1 + 1} (α := R[X]) ((C : (a : R) → R[X]) 0) 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ Eq (α := R[X]) P.toPoly 0

Tactic:
rw [of_c_eq_zero ha hb hc, hd, C_0]

Premises used: Polynomial.C_0, Cubic.of_c_eq_zero
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[X]) (toPoly { a := 0, b := 0, c := 0, d := 0 }) 0

Tactic:
of_d_eq_zero rfl rfl rfl rfl

Premises used: Cubic.of_d_eq_zero, rfl
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[X]) (toPoly 0) 0

Tactic:
of_d_eq_zero'

Premises used: Cubic.of_d_eq_zero'
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
inst : Semiring R
P : Cubic R
rw : Eq (α := R[X]) P.toPoly (toPoly 0) ↔ P = 0
rw₁ rw₂ : P = 0 ↔ P = 0
⊢ Eq (α := R[X]) P.toPoly 0 ↔ P = 0

Tactic:
rw [← zero, toPoly_injective]

Premises used: Cubic.toPoly_injective, Cubic.zero
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
h0 : P.a ≠ 0 ∨ P.b ≠ 0 ∨ P.c ≠ 0 ∨ P.d ≠ 0
contrapose! : ∀ (h0 : Eq (α := R[X]) P.toPoly 0), P.a = 0 ∧ P.b = 0 ∧ P.c = 0 ∧ P.d = 0
⊢ Ne (α := R[X]) P.toPoly 0

Tactic:
contrapose! h0
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
h0 : Eq (α := R[X]) P.toPoly 0
rw :
  Eq.{u_1 + 1} (α := R) (a 0) 0 ∧
    Eq.{u_1 + 1} (α := R) (b 0) 0 ∧ Eq.{u_1 + 1} (α := R) (c 0) 0 ∧ Eq.{u_1 + 1} (α := R) (d 0) 0
⊢ P.a = 0 ∧ P.b = 0 ∧ P.c = 0 ∧ P.d = 0

Tactic:
rw [(toPoly_eq_zero_iff P).mp h0]

Premises used: Iff.mp, Cubic.toPoly_eq_zero_iff
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
h0 : Eq (α := R[X]) P.toPoly 0
⊢ Eq.{u_1 + 1} (α := R) (a 0) 0 ∧
    Eq.{u_1 + 1} (α := R) (b 0) 0 ∧ Eq.{u_1 + 1} (α := R) (c 0) 0 ∧ Eq.{u_1 + 1} (α := R) (d 0) 0

Tactic:
⟨rfl, rfl, rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
h0 : Eq (α := R[X]) P.toPoly 0
⊢ Eq.{u_1 + 1} (α := R) (a 0) 0 ∧
    Eq.{u_1 + 1} (α := R) (b 0) 0 ∧ Eq.{u_1 + 1} (α := R) (c 0) 0 ∧ Eq.{u_1 + 1} (α := R) (d 0) 0

Tactic:
exact ⟨rfl, rfl, rfl, rfl⟩
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a ≠ 0
⊢ Ne (α := R[X]) P.toPoly 0

Tactic:
(or_imp.mp ne_zero).1 ha

Premises used: _private.0.Cubic.ne_zero, or_imp, And.left, Iff.mp
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
hb : P.b ≠ 0
⊢ Ne (α := R[X]) P.toPoly 0

Tactic:
(or_imp.mp (or_imp.mp ne_zero).2).1 hb

Premises used: _private.0.Cubic.ne_zero, or_imp, And.right, And.left, Iff.mp
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
hc : P.c ≠ 0
⊢ Ne (α := R[X]) P.toPoly 0

Tactic:
(or_imp.mp (or_imp.mp (or_imp.mp ne_zero).2).2).1 hc

Premises used: _private.0.Cubic.ne_zero, or_imp, And.right, And.left, Iff.mp
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
hd : P.d ≠ 0
⊢ Ne (α := R[X]) P.toPoly 0

Tactic:
(or_imp.mp (or_imp.mp (or_imp.mp ne_zero).2).2).2 hd

Premises used: _private.0.Cubic.ne_zero, or_imp, And.right, Iff.mp
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a ≠ 0
⊢ leadingCoeff P.toPoly = P.a

Tactic:
leadingCoeff_cubic ha

Premises used: Polynomial.leadingCoeff_cubic, Cubic.toPoly
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
a b c d : R
inst : Semiring R
ha : a ≠ 0
⊢ leadingCoeff { a := a, b := b, c := c, d := d : Cubic R }.toPoly = a

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 0
hb : P.b ≠ 0
rw :
  (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) P.b : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) P.c : R[X]) X)
        ((C : (a : R) → R[X]) P.d : R[X])).leadingCoeff =
    P.b
rw₁ rw₂ : P.b = P.b
⊢ leadingCoeff P.toPoly = P.b

Tactic:
rw [of_a_eq_zero ha, leadingCoeff_quadratic hb]

Premises used: Polynomial.leadingCoeff_quadratic, Cubic.of_a_eq_zero
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
b c d : R
inst : Semiring R
hb : b ≠ 0
⊢ leadingCoeff { a := 0, b := b, c := c, d := d : Cubic R }.toPoly = b

Tactic:
simp [hb]
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
rw :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) P.c : R[X]) X)
        ((C : (a : R) → R[X]) P.d : R[X])).leadingCoeff =
    P.c
rw₁ rw₂ : P.c = P.c
⊢ leadingCoeff P.toPoly = P.c

Tactic:
rw [of_b_eq_zero ha hb, leadingCoeff_linear hc]

Premises used: Polynomial.leadingCoeff_linear, Cubic.of_b_eq_zero
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
c d : R
inst : Semiring R
hc : c ≠ 0
⊢ leadingCoeff { a := 0, b := 0, c := c, d := d : Cubic R }.toPoly = c

Tactic:
simp [hc]
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
rw : leadingCoeff ((C : (a : R) → R[X]) P.d) = P.d
rw₁ rw₂ : P.d = P.d
⊢ leadingCoeff P.toPoly = P.d

Tactic:
rw [of_c_eq_zero ha hb hc, leadingCoeff_C]

Premises used: Polynomial.leadingCoeff_C, Cubic.of_c_eq_zero
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
d : R
inst : Semiring R
⊢ leadingCoeff { a := 0, b := 0, c := 0, d := d : Cubic R }.toPoly = d

Tactic:
leadingCoeff_of_c_eq_zero rfl rfl rfl

Premises used: Cubic.leadingCoeff_of_c_eq_zero, rfl
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 1
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 1
h : Nontrivial R
rw : leadingCoeff P.toPoly = 1
rw₁ : P.a = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Monic P.toPoly

Tactic:
rw [Monic, leadingCoeff_of_a_ne_zero (ha ▸ one_ne_zero), ha]

Premises used: Cubic.leadingCoeff_of_a_ne_zero, Polynomial.Monic
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
b c d : R
inst : Semiring R
⊢ Monic { a := 1, b := b, c := c, d := d }.toPoly

Tactic:
monic_of_a_eq_one rfl

Premises used: Cubic.monic_of_a_eq_one, rfl
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 0
hb : P.b = 1
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 0
hb : P.b = 1
h : Nontrivial R
rw : leadingCoeff P.toPoly = 1
rw₁ : P.b = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Monic P.toPoly

Tactic:
rw [Monic, leadingCoeff_of_b_ne_zero ha (hb ▸ one_ne_zero), hb]

Premises used: Eq.rec, Polynomial.Monic, Cubic.leadingCoeff_of_b_ne_zero, one_ne_zero, Eq.symm
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
c d : R
inst : Semiring R
⊢ Monic { a := 0, b := 1, c := c, d := d }.toPoly

Tactic:
monic_of_b_eq_one rfl rfl

Premises used: Cubic.monic_of_b_eq_one, rfl