awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (goal)
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])
⊢ 2 ≤ p.natDegree
have h : 2 = p.roots.card
Tactic: convert! p.card_roots'
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (goal)
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])
⊢ 2 = p.roots.card
have h : 2 = Multiset.card (α := R) {x1, x2}
Tactic: rw [hroots, Multiset.card_pair]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (goal)
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])
h : 2 = Multiset.card (α := R) {x1, x2}
⊢ 2 = p.roots.card
have h₁ : Eq (α := ℕ) 2 2
Tactic: rw [hroots, Multiset.card_pair]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (hypothesis)
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])
⊢ b = -a * (x1 + x2)
have hp_natDegree : p.natDegree = 2
Tactic: have hp_natDegree : p.natDegree = 2 := le_antisymm natDegree_quadratic_le
    (by convert! p.card_roots'; rw [hroots, Multiset.card_pair])
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (goal)
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
⊢ p.roots.card = p.natDegree
have rw : p.roots.card = 2
Tactic: rw [hp_natDegree, hroots, Multiset.card_pair]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (goal)
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
rw : p.roots.card = 2
⊢ p.roots.card = p.natDegree
have rw₁ : Multiset.card (α := R) {x1, x2} = 2
Tactic: rw [hp_natDegree, hroots, Multiset.card_pair]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (goal)
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
rw : p.roots.card = 2
rw₁ : Multiset.card (α := R) {x1, x2} = 2
⊢ p.roots.card = p.natDegree
have rw₂ : Eq (α := ℕ) 2 2
Tactic: rw [hp_natDegree, hroots, Multiset.card_pair]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (hypothesis)
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
⊢ b = -a * (x1 + x2)
have hp_roots_card : p.roots.card = p.natDegree
Tactic: have hp_roots_card : p.roots.card = p.natDegree := by
    rw [hp_natDegree, hroots, Multiset.card_pair]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (hypothesis)
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])
⊢ c = a * x1 * x2
have hp_natDegree : p.natDegree = 2
Tactic: have hp_natDegree : p.natDegree = 2 := le_antisymm natDegree_quadratic_le
    (by convert! p.card_roots'; rw [hroots, Multiset.card_pair])
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (hypothesis)
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
⊢ c = a * x1 * x2
have hp_roots_card : p.roots.card = p.natDegree
Tactic: have hp_roots_card : p.roots.card = p.natDegree := by
    rw [hp_natDegree, hroots, Multiset.card_pair]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (hypothesis)
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}
⊢ (algebraMap T S : (a : T) → S) b = HMul.hMul (α := S) (-(algebraMap T S : (a : T) → S) a : S) (x1 + x2)
have 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}
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
Cleared hypotheses: haroots
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (hypothesis)
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}
⊢ (algebraMap T S : (a : T) → S) c = HMul.hMul (α := S) ((algebraMap T S : (a : T) → S) a : S) x1 * x2
have 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}
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
Cleared hypotheses: haroots
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (hypothesis)
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])
⊢ (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}
have 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
Tactic: have h1 : C a * (X - C x1) ≠ 0 := mul_ne_zero (by simpa) (Polynomial.X_sub_C_ne_zero _)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (hypothesis)
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
⊢ (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}
have 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
Tactic: have h2 : C a * (X - C x1) * (X - C x2) ≠ 0 := mul_ne_zero h1 (Polynomial.X_sub_C_ne_zero _)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (goal)
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
⊢ (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}
have 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])
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (goal)
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
⊢ 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])
have 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])
Tactic: simp [hvieta.1, hvieta.2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (goal)
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 (β := 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
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (goal)
Goal:
R : Type u_1
inst : Field R
a b c x1 x2 : R
ha : a ≠ 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} ↔
    x1 + x2 = -b / a ∧ x1 * x2 = c / a
have rw : b = -a * (x1 + x2) ∧ c = a * x1 * x2 ↔ x1 + x2 = -b / a ∧ x1 * x2 = c / a
Tactic: rw [roots_quadratic_eq_pair_iff_of_ne_zero ha]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.SmallDegreeVieta (goal)
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)
⊢ (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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
n : ℕ
⊢ (↑((p.toSubring T hp).coeff n) : R) = p.coeff n
have simp : (↑(if p.coeff n = 0 then 0 else Subtype.mk (p := fun (x : R) ↦ x ∈ T) (p.coeff n) sorry) : R) = p.coeff n
Tactic: simp only [toSubring, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
n : ℕ
⊢ (↑(if p.coeff n = 0 then 0 else Subtype.mk (p := fun (x : R) ↦ x ∈ T) (p.coeff n) ⋯) : R) = p.coeff n
have pos : ∀ (h : p.coeff n = 0), (↑0 : R) = p.coeff n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
n : ℕ
pos : ∀ (h : p.coeff n = 0), (↑0 : R) = p.coeff n
⊢ (↑(if p.coeff n = 0 then 0 else Subtype.mk (p := fun (x : R) ↦ x ∈ T) (p.coeff n) ⋯) : R) = p.coeff n
have neg : ∀ (h : ¬p.coeff n = 0), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ T) (p.coeff n) sorry) : R) = p.coeff n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
n : ℕ
h : p.coeff n = 0
⊢ (↑0 : R) = p.coeff n
have pos : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
n : ℕ
⊢ (↑((p.toSubring T hp).coeff n) : R) = p.coeff n
have simp : (↑(if p.coeff n = 0 then 0 else Subtype.mk (p := fun (x : R) ↦ x ∈ T) (p.coeff n) sorry) : R) = p.coeff n
Tactic: classical
  simp only [toSubring, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]
  split_ifs with h
  · rw [h]
    rfl
  · rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
n : ℕ
simp : (↑(if p.coeff n = 0 then 0 else Subtype.mk (p := fun (x : R) ↦ x ∈ T) (p.coeff n) ⋯) : R) = p.coeff n
⊢ (↑((p.toSubring T hp).coeff n) : R) = p.coeff n
have pos : ∀ (h : p.coeff n = 0), (↑0 : R) = p.coeff n
Tactic: classical
  simp only [toSubring, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]
  split_ifs with h
  · rw [h]
    rfl
  · rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
n : ℕ
simp : (↑(if p.coeff n = 0 then 0 else Subtype.mk (p := fun (x : R) ↦ x ∈ T) (p.coeff n) ⋯) : R) = p.coeff n
pos : ∀ (h : p.coeff n = 0), (↑0 : R) = p.coeff n
⊢ (↑((p.toSubring T hp).coeff n) : R) = p.coeff n
have neg : ∀ (h : ¬p.coeff n = 0), (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ T) (p.coeff n) sorry) : R) = p.coeff n
Tactic: classical
  simp only [toSubring, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]
  split_ifs with h
  · rw [h]
    rfl
  · rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
⊢ (p.toSubring T hp).support = p.support
have h : ∀ (i : ℕ), i ∈ (p.toSubring T hp).support ↔ i ∈ p.support
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
i : ℕ
⊢ i ∈ (p.toSubring T hp).support ↔ i ∈ p.support
have h : (p.toSubring T hp).coeff i = 0 ↔ p.coeff i = 0
Tactic: simp only [mem_support_iff, not_iff_not, Ne]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Subring (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
T : Subring R
hp : (↑p.coeffs : Set R) ⊆ (↑T : Set R)
i : ℕ
| p.coeff i = 0
have rw : (↑((p.toSubring T hp).coeff i) : R) = 0
Tactic: rw [← coeff_toSubring p T hp]