awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ leadingCoeff P.toPoly = P.b
have rw₁ : P.b = P.b
Tactic: rw [of_a_eq_zero ha, leadingCoeff_quadratic hb]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ leadingCoeff P.toPoly = P.c
have 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
Tactic: rw [of_b_eq_zero ha hb, leadingCoeff_linear hc]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ leadingCoeff P.toPoly = P.c
have rw₁ : P.c = P.c
Tactic: rw [of_b_eq_zero ha hb, leadingCoeff_linear hc]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ leadingCoeff P.toPoly = P.d
have rw : leadingCoeff ((C : (a : R) → R[X]) P.d) = P.d
Tactic: rw [of_c_eq_zero ha hb hc, leadingCoeff_C]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ leadingCoeff P.toPoly = P.d
have rw₁ : P.d = P.d
Tactic: rw [of_c_eq_zero ha hb hc, leadingCoeff_C]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (hypothesis)
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 1
⊢ Monic P.toPoly
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 1
h : Nontrivial R
⊢ Monic P.toPoly
have rw : leadingCoeff P.toPoly = 1
Tactic: rw [Monic, leadingCoeff_of_a_ne_zero (ha ▸ one_ne_zero), ha]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ Monic P.toPoly
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [Monic, leadingCoeff_of_a_ne_zero (ha ▸ one_ne_zero), ha]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (hypothesis)
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 0
hb : P.b = 1
⊢ Monic P.toPoly
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 0
hb : P.b = 1
h : Nontrivial R
⊢ Monic P.toPoly
have rw : leadingCoeff P.toPoly = 1
Tactic: rw [Monic, leadingCoeff_of_b_ne_zero ha (hb ▸ one_ne_zero), hb]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ Monic P.toPoly
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [Monic, leadingCoeff_of_b_ne_zero ha (hb ▸ one_ne_zero), hb]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (hypothesis)
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 1
⊢ Monic P.toPoly
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ Monic P.toPoly
have rw : leadingCoeff P.toPoly = 1
Tactic: rw [Monic, leadingCoeff_of_c_ne_zero ha hb (hc ▸ one_ne_zero), hc]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ Monic P.toPoly
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [Monic, leadingCoeff_of_c_ne_zero ha hb (hc ▸ one_ne_zero), hc]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ Monic P.toPoly
have rw : leadingCoeff P.toPoly = 1
Tactic: rw [Monic, leadingCoeff_of_c_eq_zero ha hb hc, hd]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ Monic P.toPoly
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [Monic, leadingCoeff_of_c_eq_zero ha hb hc, hd]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ (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
have 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 sorry : { p : R[X] // p.degree ≤ 3 }))
        P)) =
  P.a
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ (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
have 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 sorry : { p : R[X] // p.degree ≤ 3 }))
        P)) =
  P.b
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ (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
have 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 sorry : { p : R[X] // p.degree ≤ 3 }))
        P)) =
  P.c
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ (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
have 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 sorry : { p : R[X] // p.degree ≤ 3 }))
        P)) =
  P.d
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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 }
⊢ (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
have a₁ : ∀ (n : ℕ),
  coeff
      (↑((fun (P : Cubic R) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly sorry : { 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: ext n
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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 : ℕ
⊢ 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
have a₁ : ∀ (hn : n ≤ 3),
  coeff
      (↑((fun (P : Cubic R) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly sorry : { 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
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ 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
have a₂ : ∀ (hn : 3 < n),
  coeff
      (↑((fun (P : Cubic R) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly sorry : { 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
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ 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
have a₁ : ∀ (hn : LE.le (α := ℕ) 0 3),
  coeff
      (↑((fun (P : Cubic R) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly sorry : { 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: interval_cases n
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ 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
have a₂ : ∀ (hn : LE.le (α := ℕ) 1 3),
  coeff
      (↑((fun (P : Cubic R) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly sorry : { 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: interval_cases n
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ 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
have a₃ : ∀ (hn : LE.le (α := ℕ) 2 3),
  coeff
      (↑((fun (P : Cubic R) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly sorry : { 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: interval_cases n
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
⊢ 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
have a₄ : ∀ (hn : LE.le (α := ℕ) 3 3),
  coeff
      (↑((fun (P : Cubic R) ↦
              (Subtype.mk (p := fun (p : R[X]) ↦ p.degree ≤ 3) P.toPoly sorry : { 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: interval_cases n
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
      (↑((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
have 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
Tactic: simp only
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
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
      (↑((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
have 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
Tactic: simp only