awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 = 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 = 0
hc : P.c = 1
h : Nontrivial R
rw : leadingCoeff P.toPoly = 1
rw₁ : P.c = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Monic P.toPoly

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

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

Tactic:
monic_of_c_eq_one rfl rfl rfl

Premises used: Cubic.monic_of_c_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 = 0
hc : P.c = 0
hd : P.d = 1
rw : leadingCoeff P.toPoly = 1
rw₁ : P.d = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Monic P.toPoly

Tactic:
rw [Monic, leadingCoeff_of_c_eq_zero ha hb hc, hd]

Premises used: Polynomial.Monic, Cubic.leadingCoeff_of_c_eq_zero
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
⊢ Monic (R := ℕ) (toPoly { a := 0, b := 0, c := 0, d := 1 })

Tactic:
monic_of_d_eq_one rfl rfl rfl rfl

Premises used: Cubic.monic_of_d_eq_one, rfl
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P_1 Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
P : Cubic R
a₁ :
  Cubic.a
      ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
          { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
            Cubic R })
        ((fun (P : Cubic R) ↦
            (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
          P)) =
    P.a
b₁ :
  Cubic.b
      ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
          { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
            Cubic R })
        ((fun (P : Cubic R) ↦
            (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
          P)) =
    P.b
c₁ :
  Cubic.c
      ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
          { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
            Cubic R })
        ((fun (P : Cubic R) ↦
            (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
          P)) =
    P.c
d₁ :
  Cubic.d
      ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
          { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
            Cubic R })
        ((fun (P : Cubic R) ↦
            (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
          P)) =
    P.d
⊢ (fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
        { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
          Cubic R })
      ((fun (P : Cubic R) ↦ (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
        P) =
    P

Tactic:
ext
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P_1 Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
P : Cubic R
⊢ Cubic.a
      ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
          { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
            Cubic R })
        ((fun (P : Cubic R) ↦
            (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
          P)) =
    P.a

Tactic:
simp only [coeffs]

Premises used: _private.0.Cubic.coeffs
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P_1 Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
P : Cubic R
⊢ Cubic.b
      ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
          { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
            Cubic R })
        ((fun (P : Cubic R) ↦
            (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
          P)) =
    P.b

Tactic:
simp only [coeffs]

Premises used: _private.0.Cubic.coeffs
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P_1 Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
P : Cubic R
⊢ Cubic.c
      ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
          { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
            Cubic R })
        ((fun (P : Cubic R) ↦
            (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
          P)) =
    P.c

Tactic:
simp only [coeffs]

Premises used: _private.0.Cubic.coeffs
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P_1 Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
P : Cubic R
⊢ Cubic.d
      ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
          { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
            Cubic R })
        ((fun (P : Cubic R) ↦
            (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
          P)) =
    P.d

Tactic:
simp only [coeffs]

Premises used: _private.0.Cubic.coeffs
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
a₁ :
  ∀ (n : ℕ),
    coeff
        (↑((fun (P : Cubic R) ↦
                (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
              ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
                  { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1,
                    d := (↑f : R[X]).coeff 0 : Cubic R })
                f)) :
          R[X])
        n =
      (↑f : R[X]).coeff n
⊢ (fun (P : Cubic R) ↦ (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
      ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
          { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
            Cubic R })
        f) =
    f

Tactic:
ext n
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
a₁ :
  ∀ (hn : n ≤ 3),
    coeff
        (↑((fun (P : Cubic R) ↦
                (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
              ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
                  { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1,
                    d := (↑f : R[X]).coeff 0 : Cubic R })
                f)) :
          R[X])
        n =
      (↑f : R[X]).coeff n
a₂ :
  ∀ (hn : 3 < n),
    coeff
        (↑((fun (P : Cubic R) ↦
                (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
              ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
                  { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1,
                    d := (↑f : R[X]).coeff 0 : Cubic R })
                f)) :
          R[X])
        n =
      (↑f : R[X]).coeff n
⊢ coeff
      (↑((fun (P : Cubic R) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
            ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
                { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1,
                  d := (↑f : R[X]).coeff 0 : Cubic R })
              f)) :
        R[X])
      n =
    (↑f : R[X]).coeff n

Tactic:
obtain hn | hn := le_or_gt n 3

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
hn : n ≤ 3
a₁ :
  ∀ (hn : LE.le (α := ℕ) 0 3),
    coeff
        (↑((fun (P : Cubic R) ↦
                (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
              ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
                  { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1,
                    d := (↑f : R[X]).coeff 0 : Cubic R })
                f)) :
          R[X])
        0 =
      (↑f : R[X]).coeff 0
a₂ :
  ∀ (hn : LE.le (α := ℕ) 1 3),
    coeff
        (↑((fun (P : Cubic R) ↦
                (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
              ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
                  { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1,
                    d := (↑f : R[X]).coeff 0 : Cubic R })
                f)) :
          R[X])
        1 =
      (↑f : R[X]).coeff 1
a₃ :
  ∀ (hn : LE.le (α := ℕ) 2 3),
    coeff
        (↑((fun (P : Cubic R) ↦
                (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
              ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
                  { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1,
                    d := (↑f : R[X]).coeff 0 : Cubic R })
                f)) :
          R[X])
        2 =
      (↑f : R[X]).coeff 2
a₄ :
  ∀ (hn : LE.le (α := ℕ) 3 3),
    coeff
        (↑((fun (P : Cubic R) ↦
                (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
              ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
                  { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1,
                    d := (↑f : R[X]).coeff 0 : Cubic R })
                f)) :
          R[X])
        3 =
      (↑f : R[X]).coeff 3
⊢ coeff
      (↑((fun (P : Cubic R) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
            ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
                { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1,
                  d := (↑f : R[X]).coeff 0 : Cubic R })
              f)) :
        R[X])
      n =
    (↑f : R[X]).coeff n

Tactic:
interval_cases n
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
hn : LE.le (α := ℕ) 0 3
a₁ :
  coeff
      { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
          Cubic R }.toPoly
      0 =
    (↑f : R[X]).coeff 0
⊢ coeff
      (↑((fun (P : Cubic R) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
            ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
                { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1,
                  d := (↑f : R[X]).coeff 0 : Cubic R })
              f)) :
        R[X])
      0 =
    (↑f : R[X]).coeff 0

Tactic:
simp only
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
hn : LE.le (α := ℕ) 1 3
a₁ :
  coeff
      { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
          Cubic R }.toPoly
      1 =
    (↑f : R[X]).coeff 1
⊢ coeff
      (↑((fun (P : Cubic R) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
            ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
                { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1,
                  d := (↑f : R[X]).coeff 0 : Cubic R })
              f)) :
        R[X])
      1 =
    (↑f : R[X]).coeff 1

Tactic:
simp only
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
hn : LE.le (α := ℕ) 2 3
a₁ :
  coeff
      { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
          Cubic R }.toPoly
      2 =
    (↑f : R[X]).coeff 2
⊢ coeff
      (↑((fun (P : Cubic R) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
            ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
                { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1,
                  d := (↑f : R[X]).coeff 0 : Cubic R })
              f)) :
        R[X])
      2 =
    (↑f : R[X]).coeff 2

Tactic:
simp only
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
hn : LE.le (α := ℕ) 3 3
a₁ :
  coeff
      { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
          Cubic R }.toPoly
      3 =
    (↑f : R[X]).coeff 3
⊢ coeff
      (↑((fun (P : Cubic R) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
            ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
                { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1,
                  d := (↑f : R[X]).coeff 0 : Cubic R })
              f)) :
        R[X])
      3 =
    (↑f : R[X]).coeff 3

Tactic:
simp only
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
hn : LE.le (α := ℕ) 0 3
⊢ coeff
      { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
          Cubic R }.toPoly
      0 =
    (↑f : R[X]).coeff 0

Tactic:
simp only [coeffs]

Premises used: _private.0.Cubic.coeffs
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
hn : LE.le (α := ℕ) 0 3
⊢ coeff
      { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
          Cubic R }.toPoly
      0 =
    (↑f : R[X]).coeff 0

Tactic:
try simp only [coeffs]

Premises used: _private.0.Cubic.coeffs
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
hn : LE.le (α := ℕ) 1 3
⊢ coeff
      { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
          Cubic R }.toPoly
      1 =
    (↑f : R[X]).coeff 1

Tactic:
simp only [coeffs]

Premises used: _private.0.Cubic.coeffs
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
hn : LE.le (α := ℕ) 1 3
⊢ coeff
      { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
          Cubic R }.toPoly
      1 =
    (↑f : R[X]).coeff 1

Tactic:
try simp only [coeffs]

Premises used: _private.0.Cubic.coeffs
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
hn : LE.le (α := ℕ) 2 3
⊢ coeff
      { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
          Cubic R }.toPoly
      2 =
    (↑f : R[X]).coeff 2

Tactic:
simp only [coeffs]

Premises used: _private.0.Cubic.coeffs
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
hn : LE.le (α := ℕ) 2 3
⊢ coeff
      { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
          Cubic R }.toPoly
      2 =
    (↑f : R[X]).coeff 2

Tactic:
try simp only [coeffs]

Premises used: _private.0.Cubic.coeffs
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
hn : LE.le (α := ℕ) 3 3
⊢ coeff
      { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
          Cubic R }.toPoly
      3 =
    (↑f : R[X]).coeff 3

Tactic:
simp only [coeffs]

Premises used: _private.0.Cubic.coeffs
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
hn : LE.le (α := ℕ) 3 3
⊢ coeff
      { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1, d := (↑f : R[X]).coeff 0 :
          Cubic R }.toPoly
      3 =
    (↑f : R[X]).coeff 3

Tactic:
try simp only [coeffs]

Premises used: _private.0.Cubic.coeffs
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
hn : 3 < n
a₁ : LT.lt (α := WithBot ℕ) 3 (↑n : WithBot ℕ)
⊢ coeff
      (↑((fun (P : Cubic R) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly ⋯ : { p : R[X] // p.degree ≤ 3 }))
            ((fun (f : { p : R[X] // p.degree ≤ 3 }) ↦
                { a := (↑f : R[X]).coeff 3, b := (↑f : R[X]).coeff 2, c := (↑f : R[X]).coeff 1,
                  d := (↑f : R[X]).coeff 0 : Cubic R })
              f)) :
        R[X])
      n =
    (↑f : R[X]).coeff n

Tactic:
rw [coeff_eq_zero hn, (degree_le_iff_coeff_zero (f : R[X]) 3).mp f.2]

Premises used: Cubic.coeff_eq_zero, Polynomial.degree_le_iff_coeff_zero, Iff.mp, OfNat.ofNat, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst : Semiring R
f : { p : R[X] // p.degree ≤ 3 }
n : ℕ
hn : 3 < n
⊢ LT.lt (α := WithBot ℕ) 3 (↑n : WithBot ℕ)

Tactic:
simpa using hn
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a ≠ 0
⊢ degree P.toPoly = 3

Tactic:
degree_cubic ha

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

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 0
⊢ degree P.toPoly ≤ 2

Tactic:
simpa only [of_a_eq_zero ha] using degree_quadratic_le

Premises used: Cubic.of_a_eq_zero, Polynomial.degree_quadratic_le
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
b c d : R
inst : Semiring R
⊢ degree { a := 0, b := b, c := c, d := d : Cubic R }.toPoly ≤ 2

Tactic:
degree_of_a_eq_zero rfl

Premises used: Cubic.degree_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])).degree =
    2
rw₁ rw₂ : Eq (α := WithBot ℕ) 2 2
⊢ degree P.toPoly = 2

Tactic:
rw [of_a_eq_zero ha, degree_quadratic hb]

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

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
⊢ degree P.toPoly ≤ 1

Tactic:
simpa only [of_b_eq_zero ha hb] using degree_linear_le

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

Tactic:
degree_of_b_eq_zero rfl rfl

Premises used: Cubic.degree_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])).degree =
    1
rw₁ rw₂ : Eq (α := WithBot ℕ) 1 1
⊢ degree P.toPoly = 1

Tactic:
rw [of_b_eq_zero ha hb, degree_linear hc]

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

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
⊢ degree P.toPoly ≤ 0

Tactic:
simpa only [of_c_eq_zero ha hb hc] using degree_C_le

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

Tactic:
degree_of_c_eq_zero rfl rfl rfl

Premises used: Cubic.degree_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 : degree.{u_1} (R := R) ((C : (a : R) → R[X]) P.d) = 0
rw₁ rw₂ : Eq (α := WithBot ℕ) 0 0
⊢ degree P.toPoly = 0

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

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

Tactic:
simp [hd]
-- 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 : degree.{u_1} (R := R) 0 = ⊥
rw₁ rw₂ : Eq (α := WithBot ℕ) ⊥ ⊥
⊢ degree P.toPoly = ⊥

Tactic:
rw [of_d_eq_zero ha hb hc hd, degree_zero]

Premises used: Cubic.of_d_eq_zero, Polynomial.degree_zero
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
inst : Semiring R
⊢ degree.{u_1} (R := R) (toPoly { a := 0, b := 0, c := 0, d := 0 : Cubic R }) = ⊥

Tactic:
degree_of_d_eq_zero rfl rfl rfl rfl

Premises used: Cubic.degree_of_d_eq_zero, rfl
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
inst : Semiring R
⊢ degree.{u_1} (R := R) (toPoly 0) = ⊥

Tactic:
degree_of_d_eq_zero'

Premises used: Cubic.degree_of_d_eq_zero'
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a ≠ 0
⊢ natDegree P.toPoly = 3

Tactic:
natDegree_cubic ha

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

Tactic:
simp [ha]