-- Mathlib/Algebra/CubicDiscriminant.lean
theorem coeffs : (∀ n > 3, P.toPoly.coeff n = 0) ∧ P.toPoly.coeff 3 = P.a ∧
    P.toPoly.coeff 2 = P.b ∧ P.toPoly.coeff 1 = P.c ∧ P.toPoly.coeff 0 = P.d

Proof state:
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 3 = 2 then P.b else 0) + if 3 = 1 then P.c else 0) + if 3 = 0 then P.d else 0) =
        P.a ∧
      ((((if 2 = 3 then P.a else 0) + if True then P.b else 0) + if 2 = 1 then P.c else 0) + if 2 = 0 then P.d else 0) =
          P.b ∧
        ((((if 1 = 3 then P.a else 0) + if 1 = 2 then P.b else 0) + if True then P.c else 0) +
              if 1 = 0 then P.d else 0) =
            P.c ∧
          ((((if 0 = 3 then P.a else 0) + if 0 = 2 then P.b else 0) + if 0 = 1 then P.c else 0) +
              if True then P.d else 0) =
            P.d

Tactic:
norm_num

Result:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
⊢ ∀ (n : ℕ),
    3 < n →
      ((((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

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ((((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

Tactic:
repeat' rw [if_neg]

Result:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ 0 + 0 + 0 + 0 = 0

case hnc
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 0

case hnc
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 1

case hnc
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 2

case hnc
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 3

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ 0 + 0 = 0

Tactic:
rw [zero_add]

Result:
no goals

Proof state:
case hnc
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 3

Tactic:
omega

Result:
no goals

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
⊢ ∀ (n : ℕ),
    3 < n →
      ((((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

Tactic:
intro n hn

Result:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ((((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

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ (0 + 0 + 0 + if n = 0 then P.d else 0) = 0

Tactic:
rw [if_neg]

Result:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ 0 + 0 + 0 + 0 = 0

case hnc
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 0

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ 0 + 0 + 0 + 0 = 0

case hnc
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 0

case hnc
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 1

case hnc
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 2

case hnc
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ ¬n = 3

Tactic:
any_goals omega

Result:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ 0 + 0 + 0 + 0 = 0

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
n : ℕ
hn : 3 < n
⊢ 0 + 0 + 0 + 0 = 0

Tactic:
repeat' rw [zero_add]

Result:
no goals

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
⊢ (∀ n > 3, P.toPoly.coeff n = 0) ∧
    P.toPoly.coeff 3 = P.a ∧ P.toPoly.coeff 2 = P.b ∧ P.toPoly.coeff 1 = P.c ∧ P.toPoly.coeff 0 = P.d

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

Result:
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 3 = 2 then P.b else 0) + if 3 = 1 then P.c else 0) + if 3 = 0 then P.d else 0) =
        P.a ∧
      ((((if 2 = 3 then P.a else 0) + if True then P.b else 0) + if 2 = 1 then P.c else 0) + if 2 = 0 then P.d else 0) =
          P.b ∧
        ((((if 1 = 3 then P.a else 0) + if 1 = 2 then P.b else 0) + if True then P.c else 0) +
              if 1 = 0 then P.d else 0) =
            P.c ∧
          ((((if 0 = 3 then P.a else 0) + if 0 = 2 then P.b else 0) + if 0 = 1 then P.c else 0) +
              if True then P.d else 0) =
            P.d