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
⊢ natDegree P.toPoly ≤ 2

Tactic:
simpa only [of_a_eq_zero ha] using natDegree_quadratic_le

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

Tactic:
natDegree_of_a_eq_zero rfl

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

Tactic:
rw [of_a_eq_zero ha, natDegree_quadratic hb]

Premises used: Cubic.of_a_eq_zero, Polynomial.natDegree_quadratic
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
b c d : R
inst : Semiring R
hb : b ≠ 0
⊢ natDegree { 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
⊢ natDegree P.toPoly ≤ 1

Tactic:
simpa only [of_b_eq_zero ha hb] using natDegree_linear_le

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

Tactic:
natDegree_of_b_eq_zero rfl rfl

Premises used: rfl, Cubic.natDegree_of_b_eq_zero
-- 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])).natDegree =
    1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ natDegree P.toPoly = 1

Tactic:
rw [of_b_eq_zero ha hb, natDegree_linear hc]

Premises used: Cubic.of_b_eq_zero, Polynomial.natDegree_linear
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
c d : R
inst : Semiring R
hc : c ≠ 0
⊢ natDegree { 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
rw : natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) P.d) = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ natDegree P.toPoly = 0

Tactic:
rw [of_c_eq_zero ha hb hc, natDegree_C]

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

Tactic:
natDegree_of_c_eq_zero rfl rfl rfl

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

Tactic:
natDegree_of_c_eq_zero'

Premises used: Cubic.natDegree_of_c_eq_zero'
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
S : Type u_2
P : Cubic R
inst : Semiring R
inst_1 : Semiring S
φ : R →+* S
⊢ (map φ P).toPoly = Polynomial.map φ P.toPoly

Tactic:
simp only [map, toPoly, map_C, map_X, Polynomial.map_add, Polynomial.map_mul, Polynomial.map_pow]

Premises used: Polynomial.map_mul, Cubic.map, Polynomial.map_pow, Polynomial.map_add, Polynomial.map_X, Cubic.toPoly, Polynomial.map_C
-- Module: Mathlib.Algebra.CubicDiscriminant
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
rw₁ rw₂ : (Polynomial.map φ P.toPoly).roots = (Polynomial.map φ P.toPoly).roots
⊢ (map φ P).roots = (Polynomial.map φ P.toPoly).roots

Tactic:
rw [roots, map_toPoly]

Premises used: Cubic.roots, Cubic.map_toPoly
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : CommRing R
inst_1 : IsDomain R
h0 : Ne (α := R[X]) P.toPoly 0
x : R
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
⊢ x ∈ P.roots ↔ 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]

Premises used: Cubic.roots, Polynomial.IsRoot, Cubic.toPoly, Polynomial.mem_roots
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : CommRing R
inst_1 : IsDomain R
h0 : Ne (α := R[X]) P.toPoly 0
x : R
⊢ 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:
simp only [eval_C, eval_X, eval_add, eval_mul, eval_pow]

Premises used: Polynomial.eval_C, Polynomial.eval_X, Polynomial.eval_pow, Polynomial.eval_mul, Polynomial.eval_add
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
apply : (Polynomial.roots P.toPoly).card ≤ 3
⊢ P.roots.toFinset.card ≤ 3

Tactic:
apply (toFinset_card_le P.toPoly.roots).trans

Premises used: Polynomial.roots, Multiset.toFinset_card_le, Cubic.toPoly, LE.le.trans
-- Module: Mathlib.Algebra.CubicDiscriminant
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
neg : ∀ (hP : ¬Eq (α := R[X]) P.toPoly 0), (Polynomial.roots P.toPoly).card ≤ 3
⊢ (Polynomial.roots P.toPoly).card ≤ 3

Tactic:
by_cases hP : P.toPoly = 0

Premises used: Cubic.toPoly
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
hP : Eq (α := R[X]) P.toPoly 0
⊢ (Polynomial.roots P.toPoly).card ≤ 3

Tactic:
simp [hP]
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
hP : ¬Eq (α := R[X]) P.toPoly 0
⊢ (Polynomial.roots P.toPoly).card ≤ 3

Tactic:
WithBot.coe_le_coe.1 ((card_roots hP).trans degree_cubic_le)

Premises used: WithBot.coe_le_coe, Polynomial.card_roots, Iff.mp, Polynomial.degree_cubic_le, LE.le.trans
-- Module: Mathlib.Algebra.CubicDiscriminant
Goal:
R : Type u_1
P : Cubic R
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
hP : ¬Eq (α := R[X]) P.toPoly 0
⊢ (Polynomial.roots P.toPoly).card ≤ 3

Tactic:
exact WithBot.coe_le_coe.1 ((card_roots hP).trans degree_cubic_le)

Premises used: WithBot.coe_le_coe, Polynomial.card_roots, Iff.mp, Polynomial.degree_cubic_le, LE.le.trans
-- Module: Mathlib.Algebra.CubicDiscriminant
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
⊢ (map φ P).a ≠ 0

Tactic:
replace ha : (map φ P).a ≠ 0 := (map_ne_zero φ).mpr ha
-- Module: Mathlib.Algebra.CubicDiscriminant
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
rw₃ rw₄ :
  (Polynomial.roots (map φ P).toPoly).card = natDegree (map φ P).toPoly ↔
    (Polynomial.roots (map φ P).toPoly).card = natDegree (map φ P).toPoly
⊢ (Polynomial.map φ P.toPoly).Splits ↔ (map φ P).roots.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)]

Premises used: Cubic.roots, Polynomial.splits_iff_card_roots, Cubic.ne_zero_of_a_ne_zero, Cubic.degree_of_a_ne_zero, Iff.mp, Cubic.map_toPoly, Polynomial.degree_eq_iff_natDegree_eq
-- Module: Mathlib.Algebra.CubicDiscriminant
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}
rw₁ 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}
⊢ (Polynomial.map φ P.toPoly).Splits ↔ ∃ (x : K) (y : K) (z : K), (map φ P).roots = {x, y, z}

Tactic:
rw [splits_iff_card_roots ha, card_eq_three]

Premises used: Multiset.card_eq_three, Cubic.splits_iff_card_roots
-- Module: Mathlib.Algebra.CubicDiscriminant
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]) (β := 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])
⊢ (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])

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]

Premises used: Iff.mpr, Polynomial.Splits.eq_prod_roots, Cubic.splits_iff_roots_eq_three, Cubic.leadingCoeff_of_a_ne_zero, Exists.intro, Polynomial.leadingCoeff_map, Cubic.map_roots, Cubic.map_toPoly
-- Module: Mathlib.Algebra.CubicDiscriminant
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}
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])
⊢ 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:
change C (φ P.a) * ((X - C x) ::ₘ (X - C y) ::ₘ {X - C z}).prod = _

Premises used: Polynomial.C, Multiset.prod, HSub.hSub, Multiset.cons, Cubic.a, Singleton.singleton, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.CubicDiscriminant
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}
apply_fun :
  Eq (α := K[X]) (map φ P).toPoly
    (toPoly
      { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
        c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
        d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) })
inj : Function.Injective.{u_4 + 1, u_4 + 1} (α := Cubic K) (β := K[X]) toPoly
⊢ map φ P =
    { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
      c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
      d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) }

Tactic:
apply_fun toPoly

Premises used: Cubic.toPoly
-- Module: Mathlib.Algebra.CubicDiscriminant
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]) =
    toPoly
      { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
        c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
        d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) }
rw₁ rw₂ :
  Eq.{u_4 + 1} (α := K[X])
    (toPoly
        { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
          c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
          d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) } :
      K[X])
    (toPoly
        { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
          c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
          d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) } :
      K[X])
⊢ Eq (α := K[X]) (map φ P).toPoly
    (toPoly
      { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
        c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
        d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) })

Tactic:
rw [eq_prod_three_roots ha h3, C_mul_prod_X_sub_C_eq]

Premises used: Cubic.eq_prod_three_roots, Cubic.C_mul_prod_X_sub_C_eq
-- Module: Mathlib.Algebra.CubicDiscriminant
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}
⊢ Function.Injective.{u_4 + 1, u_4 + 1} (α := Cubic K) (β := K[X]) toPoly

Tactic:
fun P Q ↦ (toPoly_injective P Q).mp

Premises used: Cubic.toPoly_injective, Iff.mp, Function.Injective
-- Module: Mathlib.Algebra.CubicDiscriminant
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}
⊢ Function.Injective.{u_4 + 1, u_4 + 1} (α := Cubic K) (β := K[X]) toPoly

Tactic:
exact fun P Q ↦ (toPoly_injective P Q).mp

Premises used: Cubic.toPoly_injective, Iff.mp
-- Module: Mathlib.Algebra.CubicDiscriminant
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}
⊢ (φ : (a : F) → K) P.b = HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z))

Tactic:
injection eq_sum_three_roots ha h3

Premises used: Cubic.eq_sum_three_roots
-- Module: Mathlib.Algebra.CubicDiscriminant
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}
⊢ (φ : (a : F) → K) P.c = HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z)

Tactic:
injection eq_sum_three_roots ha h3

Premises used: Cubic.eq_sum_three_roots
-- Module: Mathlib.Algebra.CubicDiscriminant
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}
⊢ (φ : (a : F) → K) P.d = HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z))

Tactic:
injection eq_sum_three_roots ha h3

Premises used: Cubic.eq_sum_three_roots
-- Module: Mathlib.Algebra.CubicDiscriminant
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}
simp :
  HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.b : K) 2 *
              HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.c : K) 2 -
            HMul.hMul (α := K) (β := K) (4 : K) ((φ : (a : F) → K) P.a : K) *
              HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.c : K) 3 -
          HMul.hMul (β := K) (4 * HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.b : K) 3)
            ((φ : (a : F) → K) P.d : K) -
        27 * HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.a : K) 2 *
          HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.d : K) 2 +
      HMul.hMul (β := K)
        (HMul.hMul (β := K)
          (HMul.hMul (β := K) (HMul.hMul (α := K) (β := K) (18 : K) ((φ : (a : F) → K) P.a : K))
            ((φ : (a : F) → K) P.b : K))
          ((φ : (a : F) → K) P.c : K))
        ((φ : (a : F) → K) P.d : K) =
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) *
        (y - z))
      2
⊢ (φ : (a : F) → K) P.discr =
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) *
        (y - z))
      2

Tactic:
simp only [discr, RingHom.map_add, map_sub, map_mul, map_pow, map_ofNat]

Premises used: map_sub, map_ofNat, map_pow, map_mul, RingHom.map_add, Cubic.discr
-- Module: Mathlib.Algebra.CubicDiscriminant
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 :
  HPow.hPow (β := ℕ) (HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z))) 2 *
              HPow.hPow (β := ℕ) (HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z)) 2 -
            HMul.hMul (α := K) (β := K) (4 : K) ((φ : (a : F) → K) P.a : K) *
              HPow.hPow (β := ℕ) (HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z)) 3 -
          4 * HPow.hPow (β := ℕ) (HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z))) 3 *
            HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) -
        27 * HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.a : K) 2 *
          HPow.hPow (β := ℕ) (HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z))) 2 +
      HMul.hMul (α := K) (β := K) (18 : K) ((φ : (a : F) → K) P.a : K) *
            HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)) *
          HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z) *
        HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) =
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) *
        (y - z))
      2
⊢ HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.b : K) 2 *
              HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.c : K) 2 -
            HMul.hMul (α := K) (β := K) (4 : K) ((φ : (a : F) → K) P.a : K) *
              HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.c : K) 3 -
          HMul.hMul (β := K) (4 * HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.b : K) 3)
            ((φ : (a : F) → K) P.d : K) -
        27 * HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.a : K) 2 *
          HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.d : K) 2 +
      HMul.hMul (β := K)
        (HMul.hMul (β := K)
          (HMul.hMul (β := K) (HMul.hMul (α := K) (β := K) (18 : K) ((φ : (a : F) → K) P.a : K))
            ((φ : (a : F) → K) P.b : K))
          ((φ : (a : F) → K) P.c : K))
        ((φ : (a : F) → K) P.d : K) =
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) *
        (y - z))
      2

Tactic:
rw [b_eq_three_roots ha h3, c_eq_three_roots ha h3, d_eq_three_roots ha h3]

Premises used: Cubic.c_eq_three_roots, Cubic.d_eq_three_roots, Cubic.b_eq_three_roots
-- Module: Mathlib.Algebra.CubicDiscriminant
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}
⊢ HPow.hPow (β := ℕ) (HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z))) 2 *
              HPow.hPow (β := ℕ) (HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z)) 2 -
            HMul.hMul (α := K) (β := K) (4 : K) ((φ : (a : F) → K) P.a : K) *
              HPow.hPow (β := ℕ) (HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z)) 3 -
          4 * HPow.hPow (β := ℕ) (HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z))) 3 *
            HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) -
        27 * HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.a : K) 2 *
          HPow.hPow (β := ℕ) (HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z))) 2 +
      HMul.hMul (α := K) (β := K) (18 : K) ((φ : (a : F) → K) P.a : K) *
            HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)) *
          HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z) *
        HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) =
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) *
        (y - z))
      2

Tactic:
ring1
-- Module: Mathlib.Algebra.CubicDiscriminant
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) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) * (y - z) *
        (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) *
          (y - z)) ≠
      0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
⊢ P.discr ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z

Tactic:
rw [← map_ne_zero φ, discr_eq_prod_three_roots ha h3, pow_two]

Premises used: pow_two, Cubic.discr_eq_prod_three_roots, map_ne_zero