awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a b c x1 x2 : R
hroots :
  (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).roots =
    {x1, x2}
p : R[X] :=
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
    ((C : (a : R) → R[X]) c : R[X])
hp_natDegree : p.natDegree = 2
hp_roots_card : p.roots.card = p.natDegree
⊢ b = -a * (x1 + x2)

Tactic:
simpa [leadingCoeff, hp_natDegree, p, hroots, mul_assoc, add_comm x1] using
    coeff_eq_esymm_roots_of_card hp_roots_card (k := 1) (by simp [hp_natDegree])

Premises used: mul_assoc, Polynomial.leadingCoeff, add_comm, Polynomial.coeff_eq_esymm_roots_of_card
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a b c x1 x2 : R
hroots :
  (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).roots =
    {x1, x2}
p : R[X] :=
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
    ((C : (a : R) → R[X]) c : R[X])
hp_natDegree : p.natDegree = 2
hp_roots_card : p.roots.card = p.natDegree
⊢ 0 ≤ p.natDegree

Tactic:
simp [hp_natDegree]
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a b c x1 x2 : R
hroots :
  (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).roots =
    {x1, x2}
p : R[X] :=
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
    ((C : (a : R) → R[X]) c : R[X])
hp_natDegree : p.natDegree = 2
hp_roots_card : p.roots.card = p.natDegree
⊢ c = a * x1 * x2

Tactic:
simpa [leadingCoeff, hp_natDegree, p, hroots, mul_assoc, add_comm x1] using
    coeff_eq_esymm_roots_of_card hp_roots_card (k := 0) (by simp [hp_natDegree])

Premises used: mul_assoc, Polynomial.leadingCoeff, add_comm, Polynomial.coeff_eq_esymm_roots_of_card
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
T : Type u_2
S : Type u_3
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a b c : T
x1 x2 : S
haroots :
  roots
      (map (algebraMap T S)
        (HAdd.hAdd (β := T[X])
          (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) (HPow.hPow (α := T[X]) (β := ℕ) X 2) +
            HMul.hMul (α := T[X]) (β := T[X]) ((C : (a : T) → T[X]) b : T[X]) X)
          ((C : (a : T) → T[X]) c : T[X]))) =
    {x1, x2}
⊢ map (algebraMap T S)
      (HAdd.hAdd (β := T[X])
        (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) (HPow.hPow (α := T[X]) (β := ℕ) X 2) +
          HMul.hMul (α := T[X]) (β := T[X]) ((C : (a : T) → T[X]) b : T[X]) X)
        ((C : (a : T) → T[X]) c : T[X])) =
    HAdd.hAdd (β := S[X])
      (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a) : S[X])
          (HPow.hPow (α := S[X]) (β := ℕ) X 2) +
        HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) b) : S[X]) X)
      ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) c) : S[X])

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
T : Type u_2
S : Type u_3
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a b c : T
x1 x2 : S
haroots :
  (HAdd.hAdd (β := T[X])
          (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) (HPow.hPow (α := T[X]) (β := ℕ) X 2) +
            HMul.hMul (α := T[X]) (β := T[X]) ((C : (a : T) → T[X]) b : T[X]) X)
          ((C : (a : T) → T[X]) c : T[X])).aroots
      S =
    {x1, x2}
⊢ (HAdd.hAdd (β := S[X])
        (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a) : S[X])
            (HPow.hPow (α := S[X]) (β := ℕ) X 2) +
          HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) b) : S[X]) X)
        ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) c) : S[X])).roots =
    {x1, x2}

Tactic:
rw [aroots_def, show map (algebraMap T S) (C a * X ^ 2 + C b * X + C c) = C ((algebraMap T S) a) *
    X ^ 2 + C ((algebraMap T S) b) * X + C ((algebraMap T S) c) by simp] at haroots

Premises used: Polynomial.aroots_def
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
T : Type u_2
S : Type u_3
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a b c : T
x1 x2 : S
haroots :
  (HAdd.hAdd (β := S[X])
        (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a) : S[X])
            (HPow.hPow (α := S[X]) (β := ℕ) X 2) +
          HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) b) : S[X]) X)
        ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) c) : S[X])).roots =
    {x1, x2}
⊢ (algebraMap T S : (a : T) → S) b = HMul.hMul (α := S) (-(algebraMap T S : (a : T) → S) a : S) (x1 + x2)

Tactic:
eq_neg_mul_add_of_roots_quadratic_eq_pair haroots

Premises used: Polynomial.eq_neg_mul_add_of_roots_quadratic_eq_pair
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
T : Type u_2
S : Type u_3
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a b c : T
x1 x2 : S
haroots :
  (HAdd.hAdd (β := S[X])
        (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a) : S[X])
            (HPow.hPow (α := S[X]) (β := ℕ) X 2) +
          HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) b) : S[X]) X)
        ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) c) : S[X])).roots =
    {x1, x2}
⊢ (algebraMap T S : (a : T) → S) b = HMul.hMul (α := S) (-(algebraMap T S : (a : T) → S) a : S) (x1 + x2)

Tactic:
exact eq_neg_mul_add_of_roots_quadratic_eq_pair haroots

Premises used: Polynomial.eq_neg_mul_add_of_roots_quadratic_eq_pair
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
T : Type u_2
S : Type u_3
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a b c : T
x1 x2 : S
haroots :
  (HAdd.hAdd (β := S[X])
        (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a) : S[X])
            (HPow.hPow (α := S[X]) (β := ℕ) X 2) +
          HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) b) : S[X]) X)
        ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) c) : S[X])).roots =
    {x1, x2}
⊢ (algebraMap T S : (a : T) → S) c = HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) a : S) x1 * x2

Tactic:
eq_mul_mul_of_roots_quadratic_eq_pair haroots

Premises used: Polynomial.eq_mul_mul_of_roots_quadratic_eq_pair
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
T : Type u_2
S : Type u_3
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a b c : T
x1 x2 : S
haroots :
  (HAdd.hAdd (β := S[X])
        (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a) : S[X])
            (HPow.hPow (α := S[X]) (β := ℕ) X 2) +
          HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) b) : S[X]) X)
        ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) c) : S[X])).roots =
    {x1, x2}
⊢ (algebraMap T S : (a : T) → S) c = HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) a : S) x1 * x2

Tactic:
exact eq_mul_mul_of_roots_quadratic_eq_pair haroots

Premises used: Polynomial.eq_mul_mul_of_roots_quadratic_eq_pair
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
this :
  HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
      ((C : (a : R) → R[X]) c : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x1 : R[X])) *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x2 : R[X])
⊢ Ne (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X])

Tactic:
simpa
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
this :
  HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
      ((C : (a : R) → R[X]) c : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x1 : R[X])) *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x2 : R[X])
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x1 : R[X])) ≠
    0

Tactic:
have h1 : C a * (X - C x1) ≠ 0 := mul_ne_zero (by simpa) (Polynomial.X_sub_C_ne_zero _)
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
this :
  HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
      ((C : (a : R) → R[X]) c : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x1 : R[X])) *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x2 : R[X])
h1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x1 : R[X])) ≠
    0
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x1 : R[X])) *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x2 : R[X]) ≠
    0

Tactic:
have h2 : C a * (X - C x1) * (X - C x2) ≠ 0 := mul_ne_zero h1 (Polynomial.X_sub_C_ne_zero _)
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
this :
  HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
      ((C : (a : R) → R[X]) c : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x1 : R[X])) *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x2 : R[X])
h1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x1 : R[X])) ≠
    0
h2 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x1 : R[X])) *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x2 : R[X]) ≠
    0
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).roots =
    {x1, x2}

Tactic:
simp [this, Polynomial.roots_mul h2, Polynomial.roots_mul h1]

Premises used: Polynomial.roots_mul
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
suffices :
  HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
      ((C : (a : R) → R[X]) c : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x1 : R[X])) *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x2 : R[X])
⊢ (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).roots =
    {x1, x2}

Tactic:
suffices C a * X ^ 2 + C b * X + C c = C a * (X - C x1) * (X - C x2) by
      have h1 : C a * (X - C x1) ≠ 0 := mul_ne_zero (by simpa) (Polynomial.X_sub_C_ne_zero _)
      have h2 : C a * (X - C x1) * (X - C x2) ≠ 0 := mul_ne_zero h1 (Polynomial.X_sub_C_ne_zero _)
      simp [this, Polynomial.roots_mul h2, Polynomial.roots_mul h1]
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
simp :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
              (HAdd.hAdd (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) x1 : R[X]) ((C : (a : R) → R[X]) x2 : R[X])) *
            X) +
      HMul.hMul (β := R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) x1 : R[X]))
        ((C : (a : R) → R[X]) x2 : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x1 : R[X])) *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x2 : R[X])
⊢ HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
      ((C : (a : R) → R[X]) c : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x1 : R[X])) *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x2 : R[X])

Tactic:
simp [hvieta.1, hvieta.2]

Premises used: And.right, And.left
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        -(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
              (HAdd.hAdd (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) x1 : R[X]) ((C : (a : R) → R[X]) x2 : R[X])) *
            X) +
      HMul.hMul (β := R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) x1 : R[X]))
        ((C : (a : R) → R[X]) x2 : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x1 : R[X])) *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x2 : R[X])

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
T : Type u_2
S : Type u_3
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a b c : T
x1 x2 : S
ha : Ne.{u_3 + 1} (α := S) ((algebraMap T S : (a : T) → S) a : S) (0 : S)
⊢ map (algebraMap T S)
      (HAdd.hAdd (β := T[X])
        (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) (HPow.hPow (α := T[X]) (β := ℕ) X 2) +
          HMul.hMul (α := T[X]) (β := T[X]) ((C : (a : T) → T[X]) b : T[X]) X)
        ((C : (a : T) → T[X]) c : T[X])) =
    HAdd.hAdd (β := S[X])
      (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a) : S[X])
          (HPow.hPow (α := S[X]) (β := ℕ) X 2) +
        HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) b) : S[X]) X)
      ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) c) : S[X])

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
T : Type u_2
S : Type u_3
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a b c : T
x1 x2 : S
ha : Ne.{u_3 + 1} (α := S) ((algebraMap T S : (a : T) → S) a : S) (0 : S)
rw :
  (HAdd.hAdd (β := S[X])
          (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a) : S[X])
              (HPow.hPow (α := S[X]) (β := ℕ) X 2) +
            HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) b) : S[X]) X)
          ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) c) : S[X])).roots =
      {x1, x2} ↔
    (algebraMap T S : (a : T) → S) b = HMul.hMul (α := S) (-(algebraMap T S : (a : T) → S) a : S) (x1 + x2) ∧
      (algebraMap T S : (a : T) → S) c = HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) a : S) x1 * x2
⊢ (HAdd.hAdd (β := T[X])
            (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) (HPow.hPow (α := T[X]) (β := ℕ) X 2) +
              HMul.hMul (α := T[X]) (β := T[X]) ((C : (a : T) → T[X]) b : T[X]) X)
            ((C : (a : T) → T[X]) c : T[X])).aroots
        S =
      {x1, x2} ↔
    (algebraMap T S : (a : T) → S) b = HMul.hMul (α := S) (-(algebraMap T S : (a : T) → S) a : S) (x1 + x2) ∧
      (algebraMap T S : (a : T) → S) c = HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) a : S) x1 * x2

Tactic:
rw [aroots_def, show map (algebraMap T S) (C a * X ^ 2 + C b * X + C c) = C ((algebraMap T S) a) *
    X ^ 2 + C ((algebraMap T S) b) * X + C ((algebraMap T S) c) by simp]

Premises used: Polynomial.aroots_def
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
T : Type u_2
S : Type u_3
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a b c : T
x1 x2 : S
ha : Ne.{u_3 + 1} (α := S) ((algebraMap T S : (a : T) → S) a : S) (0 : S)
⊢ (HAdd.hAdd (β := S[X])
          (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a) : S[X])
              (HPow.hPow (α := S[X]) (β := ℕ) X 2) +
            HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) b) : S[X]) X)
          ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) c) : S[X])).roots =
      {x1, x2} ↔
    (algebraMap T S : (a : T) → S) b = HMul.hMul (α := S) (-(algebraMap T S : (a : T) → S) a : S) (x1 + x2) ∧
      (algebraMap T S : (a : T) → S) c = HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) a : S) x1 * x2

Tactic:
roots_quadratic_eq_pair_iff_of_ne_zero ha

Premises used: Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
T : Type u_2
S : Type u_3
inst : CommRing T
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra T S
a b c : T
x1 x2 : S
ha : Ne.{u_3 + 1} (α := S) ((algebraMap T S : (a : T) → S) a : S) (0 : S)
⊢ (HAdd.hAdd (β := S[X])
          (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a) : S[X])
              (HPow.hPow (α := S[X]) (β := ℕ) X 2) +
            HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) b) : S[X]) X)
          ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) c) : S[X])).roots =
      {x1, x2} ↔
    (algebraMap T S : (a : T) → S) b = HMul.hMul (α := S) (-(algebraMap T S : (a : T) → S) a : S) (x1 + x2) ∧
      (algebraMap T S : (a : T) → S) c = HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) a : S) x1 * x2

Tactic:
exact roots_quadratic_eq_pair_iff_of_ne_zero ha

Premises used: Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
R : Type u_1
inst : Field R
a b c x1 x2 : R
ha : a ≠ 0
rw : b = -a * (x1 + x2) ∧ c = a * x1 * x2 ↔ x1 + x2 = -b / a ∧ x1 * x2 = c / a
⊢ (HAdd.hAdd (β := R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
          ((C : (a : R) → R[X]) c : R[X])).roots =
      {x1, x2} ↔
    x1 + x2 = -b / a ∧ x1 * x2 = c / a

Tactic:
rw [roots_quadratic_eq_pair_iff_of_ne_zero ha]

Premises used: Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
R : Type u_1
inst : Field R
a b c x1 x2 : R
ha : a ≠ 0
⊢ b = -a * (x1 + x2) ∧ c = a * x1 * x2 ↔ x1 + x2 = -b / a ∧ x1 * x2 = c / a

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
T : Type u_2
S : Type u_3
inst : CommRing T
inst_1 : Field S
inst_2 : Algebra T S
a b c : T
x1 x2 : S
ha : Ne.{u_3 + 1} (α := S) ((algebraMap T S : (a : T) → S) a : S) (0 : S)
⊢ map (algebraMap T S)
      (HAdd.hAdd (β := T[X])
        (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) (HPow.hPow (α := T[X]) (β := ℕ) X 2) +
          HMul.hMul (α := T[X]) (β := T[X]) ((C : (a : T) → T[X]) b : T[X]) X)
        ((C : (a : T) → T[X]) c : T[X])) =
    HAdd.hAdd (β := S[X])
      (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a) : S[X])
          (HPow.hPow (α := S[X]) (β := ℕ) X 2) +
        HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) b) : S[X]) X)
      ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) c) : S[X])

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
T : Type u_2
S : Type u_3
inst : CommRing T
inst_1 : Field S
inst_2 : Algebra T S
a b c : T
x1 x2 : S
ha : Ne.{u_3 + 1} (α := S) ((algebraMap T S : (a : T) → S) a : S) (0 : S)
rw :
  (HAdd.hAdd (β := S[X])
          (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) a) : S[X])
              (HPow.hPow (α := S[X]) (β := ℕ) X 2) +
            HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) b) : S[X]) X)
          ((C : (a : S) → S[X]) ((algebraMap T S : (a : T) → S) c) : S[X])).roots =
      {x1, x2} ↔
    x1 + x2 =
        HDiv.hDiv (α := S) (β := S) (-(algebraMap T S : (a : T) → S) b : S) ((algebraMap T S : (a : T) → S) a : S) ∧
      x1 * x2 =
        HDiv.hDiv (α := S) (β := S) ((algebraMap T S : (a : T) → S) c : S) ((algebraMap T S : (a : T) → S) a : S)
⊢ (HAdd.hAdd (β := T[X])
            (HMul.hMul (α := T[X]) ((C : (a : T) → T[X]) a : T[X]) (HPow.hPow (α := T[X]) (β := ℕ) X 2) +
              HMul.hMul (α := T[X]) (β := T[X]) ((C : (a : T) → T[X]) b : T[X]) X)
            ((C : (a : T) → T[X]) c : T[X])).aroots
        S =
      {x1, x2} ↔
    x1 + x2 =
        HDiv.hDiv (α := S) (β := S) (-(algebraMap T S : (a : T) → S) b : S) ((algebraMap T S : (a : T) → S) a : S) ∧
      x1 * x2 =
        HDiv.hDiv (α := S) (β := S) ((algebraMap T S : (a : T) → S) c : S) ((algebraMap T S : (a : T) → S) a : S)

Tactic:
rw [aroots_def, show map (algebraMap T S) (C a * X ^ 2 + C b * X + C c) = C ((algebraMap T S) a) *
    X ^ 2 + C ((algebraMap T S) b) * X + C ((algebraMap T S) c) by simp]

Premises used: Polynomial.aroots_def