awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (α := ℕ) 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
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
    2 =
  (↑f : R[X]).coeff 2
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 (α := ℕ) 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
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
    3 =
  (↑f : R[X]).coeff 3
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 : 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₁ : LT.lt (α := WithBot ℕ) 3 (↑n : WithBot ℕ)
Tactic: rw [coeff_eq_zero hn, (degree_le_iff_coeff_zero (f : R[X]) 3).mp f.2]
-- 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
⊢ degree P.toPoly = 2
have 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
Tactic: rw [of_a_eq_zero ha, degree_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
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
⊢ degree P.toPoly = 2
have rw₁ : Eq (α := WithBot ℕ) 2 2
Tactic: rw [of_a_eq_zero ha, degree_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
⊢ degree P.toPoly = 1
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])).degree =
  1
Tactic: rw [of_b_eq_zero ha hb, degree_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])).degree =
    1
⊢ degree P.toPoly = 1
have rw₁ : Eq (α := WithBot ℕ) 1 1
Tactic: rw [of_b_eq_zero ha hb, degree_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
hd : P.d ≠ 0
⊢ degree P.toPoly = 0
have rw : degree.{u_1} (R := R) ((C : (a : R) → R[X]) P.d) = 0
Tactic: rw [of_c_eq_zero ha hb hc, degree_C 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 ≠ 0
rw : degree.{u_1} (R := R) ((C : (a : R) → R[X]) P.d) = 0
⊢ degree P.toPoly = 0
have rw₁ : Eq (α := WithBot ℕ) 0 0
Tactic: rw [of_c_eq_zero ha hb hc, degree_C 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 = 0
⊢ degree P.toPoly = ⊥
have rw : degree.{u_1} (R := R) 0 = ⊥
Tactic: rw [of_d_eq_zero ha hb hc hd, degree_zero]
-- 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 = 0
rw : degree.{u_1} (R := R) 0 = ⊥
⊢ degree P.toPoly = ⊥
have rw₁ : Eq (α := WithBot ℕ) ⊥ ⊥
Tactic: rw [of_d_eq_zero ha hb hc hd, degree_zero]
-- 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
⊢ natDegree P.toPoly = 2
have 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])).natDegree =
  2
Tactic: rw [of_a_eq_zero ha, natDegree_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
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])).natDegree =
    2
⊢ natDegree P.toPoly = 2
have rw₁ : Eq (α := ℕ) 2 2
Tactic: rw [of_a_eq_zero ha, natDegree_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
⊢ natDegree P.toPoly = 1
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])).natDegree =
  1
Tactic: rw [of_b_eq_zero ha hb, natDegree_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])).natDegree =
    1
⊢ natDegree P.toPoly = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [of_b_eq_zero ha hb, natDegree_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
⊢ natDegree P.toPoly = 0
have rw : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) P.d) = 0
Tactic: rw [of_c_eq_zero ha hb hc, natDegree_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 : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) P.d) = 0
⊢ natDegree P.toPoly = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [of_c_eq_zero ha hb hc, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
S : Type u_2
P : Cubic R
inst : CommRing R
inst_1 : CommRing S
φ : R →+* S
inst_2 : IsDomain S
⊢ (map φ P).roots = (Polynomial.map φ P.toPoly).roots
have rw : Polynomial.roots (map φ P).toPoly = (Polynomial.map φ P.toPoly).roots
Tactic: rw [roots, map_toPoly]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
S : Type u_2
P : Cubic R
inst : CommRing R
inst_1 : CommRing S
φ : R →+* S
inst_2 : IsDomain S
rw : Polynomial.roots (map φ P).toPoly = (Polynomial.map φ P.toPoly).roots
⊢ (map φ P).roots = (Polynomial.map φ P.toPoly).roots
have rw₁ : (Polynomial.map φ P.toPoly).roots = (Polynomial.map φ P.toPoly).roots
Tactic: rw [roots, map_toPoly]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P : Cubic R
inst : CommRing R
inst_1 : IsDomain R
h0 : Ne (α := R[X]) P.toPoly 0
x : R
⊢ x ∈ P.roots ↔ P.a * HPow.hPow (β := ℕ) x 3 + P.b * HPow.hPow (β := ℕ) x 2 + P.c * x + P.d = 0
have rw : eval x
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) P.a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
            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])) =
    0 ↔
  P.a * HPow.hPow (β := ℕ) x 3 + P.b * HPow.hPow (β := ℕ) x 2 + P.c * x + P.d = 0
Tactic: rw [roots, mem_roots h0, IsRoot, toPoly]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P : Cubic R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
⊢ P.roots.toFinset.card ≤ 3
have apply : (Polynomial.roots P.toPoly).card ≤ 3
Tactic: apply (toFinset_card_le P.toPoly.roots).trans
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P : Cubic R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
⊢ (Polynomial.roots P.toPoly).card ≤ 3
have pos : ∀ (hP : Eq (α := R[X]) P.toPoly 0), (Polynomial.roots P.toPoly).card ≤ 3
Tactic: by_cases hP : P.toPoly = 0
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P : Cubic R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
pos : ∀ (hP : Eq (α := R[X]) P.toPoly 0), (Polynomial.roots P.toPoly).card ≤ 3
⊢ (Polynomial.roots P.toPoly).card ≤ 3
have neg : ∀ (hP : ¬Eq (α := R[X]) P.toPoly 0), (Polynomial.roots P.toPoly).card ≤ 3
Tactic: by_cases hP : P.toPoly = 0
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (hypothesis)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
⊢ (Polynomial.map φ P.toPoly).Splits ↔ (map φ P).roots.card = 3
have ha₁ : (map φ P).a ≠ 0
Tactic: replace ha : (map φ P).a ≠ 0 := (map_ne_zero φ).mpr ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : (map φ P).a ≠ 0
⊢ (Polynomial.map φ P.toPoly).Splits ↔ (map φ P).roots.card = 3
have rw : (Polynomial.map φ P.toPoly).Splits ↔ (Polynomial.roots (map φ P).toPoly).card = 3
Tactic: rw [roots, ← map_toPoly, Polynomial.splits_iff_card_roots,
    ← ((degree_eq_iff_natDegree_eq <| ne_zero_of_a_ne_zero ha).1 <| degree_of_a_ne_zero ha : _ = 3)]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : (map φ P).a ≠ 0
rw : (Polynomial.map φ P.toPoly).Splits ↔ (Polynomial.roots (map φ P).toPoly).card = 3
⊢ (Polynomial.map φ P.toPoly).Splits ↔ (map φ P).roots.card = 3
have rw₁ : Splits (map φ P).toPoly ↔ (Polynomial.roots (map φ P).toPoly).card = 3
Tactic: rw [roots, ← map_toPoly, Polynomial.splits_iff_card_roots,
    ← ((degree_eq_iff_natDegree_eq <| ne_zero_of_a_ne_zero ha).1 <| degree_of_a_ne_zero ha : _ = 3)]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : (map φ P).a ≠ 0
rw : (Polynomial.map φ P.toPoly).Splits ↔ (Polynomial.roots (map φ P).toPoly).card = 3
rw₁ : Splits (map φ P).toPoly ↔ (Polynomial.roots (map φ P).toPoly).card = 3
⊢ (Polynomial.map φ P.toPoly).Splits ↔ (map φ P).roots.card = 3
have rw₂ : (Polynomial.roots (map φ P).toPoly).card = natDegree (map φ P).toPoly ↔ (Polynomial.roots (map φ P).toPoly).card = 3
Tactic: rw [roots, ← map_toPoly, Polynomial.splits_iff_card_roots,
    ← ((degree_eq_iff_natDegree_eq <| ne_zero_of_a_ne_zero ha).1 <| degree_of_a_ne_zero ha : _ = 3)]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : (map φ P).a ≠ 0
rw : (Polynomial.map φ P.toPoly).Splits ↔ (Polynomial.roots (map φ P).toPoly).card = 3
rw₁ : Splits (map φ P).toPoly ↔ (Polynomial.roots (map φ P).toPoly).card = 3
rw₂ :
  (Polynomial.roots (map φ P).toPoly).card = natDegree (map φ P).toPoly ↔ (Polynomial.roots (map φ P).toPoly).card = 3
⊢ (Polynomial.map φ P.toPoly).Splits ↔ (map φ P).roots.card = 3
have rw₃ : (Polynomial.roots (map φ P).toPoly).card = natDegree (map φ P).toPoly ↔
  (Polynomial.roots (map φ P).toPoly).card = natDegree (map φ P).toPoly
Tactic: rw [roots, ← map_toPoly, Polynomial.splits_iff_card_roots,
    ← ((degree_eq_iff_natDegree_eq <| ne_zero_of_a_ne_zero ha).1 <| degree_of_a_ne_zero ha : _ = 3)]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
⊢ (Polynomial.map φ P.toPoly).Splits ↔ ∃ (x : K) (y : K) (z : K), (map φ P).roots = {x, y, z}
have rw : (map φ P).roots.card = 3 ↔ ∃ (x : K) (y : K) (z : K), (map φ P).roots = {x, y, z}
Tactic: rw [splits_iff_card_roots ha, card_eq_three]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
rw : (map φ P).roots.card = 3 ↔ ∃ (x : K) (y : K) (z : K), (map φ P).roots = {x, y, z}
⊢ (Polynomial.map φ P.toPoly).Splits ↔ ∃ (x : K) (y : K) (z : K), (map φ P).roots = {x, y, z}
have rw₁ : (∃ (x : K) (y : K) (z : K), (map φ P).roots = {x, y, z}) ↔ ∃ (x : K) (y : K) (z : K), (map φ P).roots = {x, y, z}
Tactic: rw [splits_iff_card_roots ha, card_eq_three]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ (map φ P).toPoly =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
          (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
have rw : HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
    (prod (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) {x, y, z}) :
      K[X]) =
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
Tactic: rw [map_toPoly,
    Splits.eq_prod_roots <|
      (splits_iff_roots_eq_three ha).mpr <| Exists.intro x <| Exists.intro y <| Exists.intro z h3,
    leadingCoeff_map, leadingCoeff_of_a_ne_zero ha, ← map_roots, h3]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
      (prod
          (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) {x, y, z}) :
        K[X]) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
          (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
have change : HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
    (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X]) ::ₘ
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) ::ₘ
          {HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])}).prod =
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
Tactic: change C (φ P.a) * ((X - C x) ::ₘ (X - C y) ::ₘ {X - C z}).prod = _
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X]) ::ₘ
          HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) ::ₘ
            {HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])}).prod =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
          (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
have rw : HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
    (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X]) *
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) ::ₘ
          {HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])}).prod) =
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
Tactic: rw [prod_cons, prod_cons, prod_singleton, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
rw :
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X]) *
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) ::ₘ
            {HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])}).prod) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
          (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
⊢ HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X]) ::ₘ
          HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) ::ₘ
            {HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])}).prod =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
          (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
have rw₁ : HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
    (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X]) *
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
        prod {HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])})) =
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
Tactic: rw [prod_cons, prod_cons, prod_singleton, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
rw :
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X]) *
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) ::ₘ
            {HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])}).prod) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
          (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
rw₁ :
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X]) *
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
          prod {HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])})) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
          (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
⊢ HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X]) ::ₘ
          HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) ::ₘ
            {HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])}).prod =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
          (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
have rw₂ : HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
    (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X]) *
      (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X]))) =
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X])
Tactic: rw [prod_cons, prod_cons, prod_singleton, mul_assoc, mul_assoc]