awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
irred : Irreducible f
hprime : Nat.Prime q
hchar : CharP F q
n : ℕ
g : F[X]
hgs : g.Separable
hge : (expand F (q ^ n) : (a : F[X]) → F[X]) g = f
⊢ HasSeparableContraction q f

Tactic:
⟨g, hgs, n, hge⟩

Premises used: And.intro, Exists.intro, Polynomial.HasSeparableContraction
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
irred : Irreducible f
hprime : Nat.Prime q
hchar : CharP F q
n : ℕ
g : F[X]
hgs : g.Separable
hge : (expand F (q ^ n) : (a : F[X]) → F[X]) g = f
⊢ HasSeparableContraction q f

Tactic:
exact ⟨g, hgs, n, hge⟩
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
q : ℕ
hq : NeZero q
inst_1 : CharP F q
g g' : F[X]
m m' : ℕ
h_expand :
  Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X]) ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X])
hg : g.Separable
hg' : g'.Separable
inr :
  ∀
    (this :
      ∀ {F : Type u_1} [inst : Field F] (q : ℕ) [hq : NeZero q] [CharP F q] (g g' : F[X]) (m m' : ℕ)
        (h_expand :
          Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X])
            ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X]))
        (hg : g.Separable) (hg' : g'.Separable) (hm : m ≤ m'), g.natDegree = g'.natDegree)
    (hm : ¬m ≤ m'), g.natDegree = g'.natDegree
wlog :
  ∀ {F : Type u_1} [inst : Field F] (q : ℕ) [hq : NeZero q] [CharP F q] (g g' : F[X]) (m m' : ℕ)
    (h_expand :
      Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X])
        ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X]))
    (hg : g.Separable) (hg' : g'.Separable) (hm : m ≤ m'), g.natDegree = g'.natDegree
⊢ g.natDegree = g'.natDegree

Tactic:
wlog hm : m ≤ m'
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
q : ℕ
hq : NeZero q
inst_1 : CharP F q
g g' : F[X]
m m' : ℕ
h_expand :
  Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X]) ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X])
hg : g.Separable
hg' : g'.Separable
this :
  ∀ {F : Type u_1} [inst : Field F] (q : ℕ) [hq : NeZero q] [CharP F q] (g g' : F[X]) (m m' : ℕ)
    (h_expand :
      Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X])
        ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X]))
    (hg : g.Separable) (hg' : g'.Separable) (hm : m ≤ m'), g.natDegree = g'.natDegree
hm : ¬m ≤ m'
⊢ g.natDegree = g'.natDegree

Tactic:
(this q g' g m' m h_expand.symm hg' hg (le_of_not_ge hm)).symm

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
q : ℕ
hq : NeZero q
inst_1 : CharP F q
g g' : F[X]
m m' : ℕ
h_expand :
  Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X]) ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X])
hg : g.Separable
hg' : g'.Separable
this :
  ∀ {F : Type u_1} [inst : Field F] (q : ℕ) [hq : NeZero q] [CharP F q] (g g' : F[X]) (m m' : ℕ)
    (h_expand :
      Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X])
        ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X]))
    (hg : g.Separable) (hg' : g'.Separable) (hm : m ≤ m'), g.natDegree = g'.natDegree
hm : ¬m ≤ m'
⊢ g.natDegree = g'.natDegree

Tactic:
exact (this q g' g m' m h_expand.symm hg' hg (le_of_not_ge hm)).symm

Premises used: le_of_not_ge, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g g' : F[X]
m m' : ℕ
h_expand :
  Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X]) ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X])
hg : g.Separable
hg' : g'.Separable
hm : m ≤ m'
obtain :
  ∀ (s : ℕ)
    (h_expand :
      Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X])
        ((expand F (q ^ (m + s)) : (a : F[X]) → F[X]) g' : F[X]))
    (hm : m ≤ m + s), g.natDegree = g'.natDegree
⊢ g.natDegree = g'.natDegree

Tactic:
obtain ⟨s, rfl⟩ := exists_add_of_le hm

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g g' : F[X]
m : ℕ
hg : g.Separable
hg' : g'.Separable
s : ℕ
h_expand :
  Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X])
    ((expand F (q ^ (m + s)) : (a : F[X]) → F[X]) g' : F[X])
hm : m ≤ m + s
⊢ g = (expand F (q ^ s) : (a : F[X]) → F[X]) g'

Tactic:
rw [pow_add, expand_mul, expand_inj (pow_pos (NeZero.pos q) m)] at h_expand

Premises used: pow_pos, pow_add, Polynomial.expand_inj, Polynomial.expand_mul, NeZero.pos
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g g' : F[X]
m : ℕ
hg : g.Separable
hg' : g'.Separable
s : ℕ
h_expand :
  Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X])
    ((expand F (q ^ (m + s)) : (a : F[X]) → F[X]) g' : F[X])
hm : m ≤ m + s
h_expand₁ : g = (expand F (q ^ s) : (a : F[X]) → F[X]) g'
⊢ m ≤ m + s

Tactic:
rw [pow_add, expand_mul, expand_inj (pow_pos (NeZero.pos q) m)] at h_expand

Premises used: pow_pos, pow_add, Polynomial.expand_inj, Polynomial.expand_mul, NeZero.pos
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g g' : F[X]
m : ℕ
hg : g.Separable
hg' : g'.Separable
s : ℕ
h_expand : g = (expand F (q ^ s) : (a : F[X]) → F[X]) g'
hm : m ≤ m + s
subst :
  ∀ (hg : Separable.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g')),
    natDegree.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g') = g'.natDegree
⊢ g.natDegree = g'.natDegree

Tactic:
subst h_expand
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
s : ℕ
hm : m ≤ m + s
hg : Separable.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g')
inl : ∀ (h : IsUnit g'), natDegree.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g') = g'.natDegree
inr :
  ∀ (hm : m ≤ m + 0) (hg : Separable.{u_1} (R := F) ((expand F (HPow.hPow (β := ℕ) q 0) : (a : F[X]) → F[X]) g')),
    natDegree.{u_1} (R := F) ((expand F (HPow.hPow (β := ℕ) q 0) : (a : F[X]) → F[X]) g') = g'.natDegree
⊢ natDegree.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g') = g'.natDegree

Tactic:
rcases isUnit_or_eq_zero_of_separable_expand q s (NeZero.pos q) hg with (h | rfl)

Premises used: Polynomial.isUnit_or_eq_zero_of_separable_expand, NeZero.pos, rfl
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
s : ℕ
hm : m ≤ m + s
hg : Separable.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g')
h : IsUnit g'
inl : g'.natDegree * q ^ s = g'.natDegree
inl₁ : 0 * q ^ s = 0
inl₂ inl₃ : Eq (α := ℕ) 0 0
⊢ natDegree.{u_1} (R := F) ((expand F (q ^ s) : (a : F[X]) → F[X]) g') = g'.natDegree

Tactic:
rw [natDegree_expand, natDegree_eq_zero_of_isUnit h, zero_mul]

Premises used: MulZeroClass.zero_mul, Polynomial.natDegree_expand, Polynomial.natDegree_eq_zero_of_isUnit
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F_1 : Type u_1
inst : Field F_1
q_1 : ℕ
F : Type u_1
inst_1 : Field F
q : ℕ
hq : NeZero q
inst_2 : CharP F q
g' : F[X]
m : ℕ
hg' : g'.Separable
hm : m ≤ m + 0
hg : Separable.{u_1} (R := F) ((expand F (HPow.hPow (β := ℕ) q 0) : (a : F[X]) → F[X]) g')
inr : g'.natDegree * HPow.hPow (β := ℕ) q 0 = g'.natDegree
inr₁ : g'.natDegree * 1 = g'.natDegree
inr₂ inr₃ : g'.natDegree = g'.natDegree
⊢ natDegree.{u_1} (R := F) ((expand F (HPow.hPow (β := ℕ) q 0) : (a : F[X]) → F[X]) g') = g'.natDegree

Tactic:
rw [natDegree_expand, pow_zero, mul_one]

Premises used: pow_zero, mul_one, Polynomial.natDegree_expand
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hF : ExpChar F q
g : F[X]
hg : IsSeparableContraction q f g
zero : ∀ [CharZero F] (hf : HasSeparableContraction 1 f) (hg : IsSeparableContraction 1 f g), g.natDegree = hf.degree
prime : Nat.Prime q → ∀ [CharP F q], g.natDegree = hf.degree
⊢ g.natDegree = hf.degree

Tactic:
cases hF
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
f g : F[X]
inst_1 : CharZero F
hf : HasSeparableContraction 1 f
hg : IsSeparableContraction 1 f g
zero :
  g.Separable → ∀ (m : ℕ) (hm : (expand F (HPow.hPow (α := ℕ) 1 m) : (a : F[X]) → F[X]) g = f), g.natDegree = hf.degree
⊢ g.natDegree = hf.degree

Tactic:
rcases hg with ⟨_, m, hm⟩
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
f g : F[X]
inst_1 : CharZero F
hf : HasSeparableContraction 1 f
left : g.Separable
m : ℕ
hm : (expand F (HPow.hPow (α := ℕ) 1 m) : (a : F[X]) → F[X]) g = f
⊢ g = f

Tactic:
rw [one_pow, expand_one] at hm

Premises used: one_pow, Polynomial.expand_one
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
f g : F[X]
inst_1 : CharZero F
hf : HasSeparableContraction 1 f
left : g.Separable
m : ℕ
hm : g = f
zero : g.natDegree = f.natDegree
zero₁ zero₂ : f.natDegree = f.natDegree
⊢ g.natDegree = hf.degree

Tactic:
rw [hf.eq_degree, hm]

Premises used: Polynomial.HasSeparableContraction.eq_degree
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hg : IsSeparableContraction q f g
hprime : Nat.Prime q
hchar : CharP F q
prime : ∀ (hg : g.Separable) (m : ℕ) (hm : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f), g.natDegree = hf.degree
⊢ g.natDegree = hf.degree

Tactic:
rcases hg with ⟨hg, m, hm⟩
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime : Nat.Prime q
hchar : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f
g' : F[X] := Classical.choose (p := IsSeparableContraction q f) hf
prime :
  ∀ (hg' : (Classical.choose (p := IsSeparableContraction q f) hf).Separable) (m' : ℕ)
    (hm' : (expand F (q ^ m') : (a : F[X]) → F[X]) (Classical.choose (p := IsSeparableContraction q f) hf) = f),
    g.natDegree = hf.degree
⊢ g.natDegree = hf.degree

Tactic:
obtain ⟨hg', m', hm'⟩ := Classical.choose_spec hf

Premises used: Classical.choose_spec
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime : Nat.Prime q
hchar : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f
g' : F[X] := Classical.choose (p := IsSeparableContraction q f) hf
hg' : (Classical.choose (p := IsSeparableContraction q f) hf).Separable
m' : ℕ
hm' : (expand F (q ^ m') : (a : F[X]) → F[X]) (Classical.choose (p := IsSeparableContraction q f) hf) = f
⊢ Nat.Prime q

Tactic:
assumption
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime : Nat.Prime q
hchar : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f
g' : F[X] := Classical.choose (p := IsSeparableContraction q f) hf
hg' : (Classical.choose (p := IsSeparableContraction q f) hf).Separable
m' : ℕ
hm' : (expand F (q ^ m') : (a : F[X]) → F[X]) (Classical.choose (p := IsSeparableContraction q f) hf) = f
⊢ Fact (Nat.Prime q)

Tactic:
haveI : Fact q.Prime := ⟨by assumption⟩
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime : Nat.Prime q
hchar : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f
g' : F[X] := Classical.choose (p := IsSeparableContraction q f) hf
hg' : (Classical.choose (p := IsSeparableContraction q f) hf).Separable
m' : ℕ
hm' : (expand F (q ^ m') : (a : F[X]) → F[X]) (Classical.choose (p := IsSeparableContraction q f) hf) = f
this : Fact (Nat.Prime q)
⊢ g.natDegree = hf.degree

Tactic:
contraction_degree_eq_or_insep q g g' m m' ?_ hg hg'

Premises used: Polynomial.contraction_degree_eq_or_insep, Polynomial.HasSeparableContraction.degree, Polynomial.HasSeparableContraction.contraction
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime : Nat.Prime q
hchar : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f
g' : F[X] := Classical.choose (p := IsSeparableContraction q f) hf
hg' : (Classical.choose (p := IsSeparableContraction q f) hf).Separable
m' : ℕ
hm' : (expand F (q ^ m') : (a : F[X]) → F[X]) (Classical.choose (p := IsSeparableContraction q f) hf) = f
this : Fact (Nat.Prime q)
prime :
  Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X]) ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X])
⊢ g.natDegree = hf.degree

Tactic:
refine contraction_degree_eq_or_insep q g g' m m' ?_ hg hg'

Premises used: Polynomial.contraction_degree_eq_or_insep
-- Module: Mathlib.RingTheory.Polynomial.SeparableDegree
Goal:
F : Type u_1
inst : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime : Nat.Prime q
hchar : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m) : (a : F[X]) → F[X]) g = f
g' : F[X] := Classical.choose (p := IsSeparableContraction q f) hf
hg' : (Classical.choose (p := IsSeparableContraction q f) hf).Separable
m' : ℕ
hm' : (expand F (q ^ m') : (a : F[X]) → F[X]) (Classical.choose (p := IsSeparableContraction q f) hf) = f
this : Fact (Nat.Prime q)
prime : f = (expand F (q ^ m') : (a : F[X]) → F[X]) g'
prime₁ prime₂ : f = f
⊢ Eq (α := F[X]) ((expand F (q ^ m) : (a : F[X]) → F[X]) g : F[X]) ((expand F (q ^ m') : (a : F[X]) → F[X]) g' : F[X])

Tactic:
rw [hm, hm']
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : p.degree ≤ 2
rw :
  ∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i) =
    (C : (a : R) → R[X])
            (coeff
              (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i))
              2) *
          HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        HMul.hMul (α := R[X])
          ((C : (a : R) → R[X])
            (coeff
              (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i))
              1))
          X +
      (C : (a : R) → R[X])
        (coeff
          (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i))
          0)
⊢ p =
    HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 2) : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])

Tactic:
rw [p.as_sum_range_C_mul_X_pow'
    (Nat.lt_of_le_of_lt (natDegree_le_iff_degree_le.mpr hp) (Nat.lt_add_one 2))]

Premises used: Iff.mpr, Polynomial.as_sum_range_C_mul_X_pow', Nat.lt_of_le_of_lt, Nat.lt_add_one, OfNat.ofNat, Polynomial.natDegree_le_iff_degree_le
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : p.degree ≤ 2
simp :
  HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 2) : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) =
    HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 2) : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
⊢ ∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i) =
    (C : (a : R) → R[X])
            (coeff
              (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i))
              2) *
          HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        HMul.hMul (α := R[X])
          ((C : (a : R) → R[X])
            (coeff
              (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i))
              1))
          X +
      (C : (a : R) → R[X])
        (coeff
          (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 2 1),
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i))
          0)

Tactic:
simp [Finset.sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : p.degree ≤ 2
⊢ HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 2) : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) =
    HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 2) : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])

Tactic:
abel
-- 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])
⊢ p.roots.card ≤ p.natDegree

Tactic:
p.card_roots'

Premises used: Polynomial.card_roots'
-- 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])
h : 2 = p.roots.card
⊢ 2 ≤ p.natDegree

Tactic:
convert! p.card_roots'

Premises used: Polynomial.card_roots'
-- 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])
h : 2 = Multiset.card (α := R) {x1, x2}
h₁ h₂ : Eq (α := ℕ) 2 2
⊢ 2 = p.roots.card

Tactic:
rw [hroots, Multiset.card_pair]

Premises used: Multiset.card_pair
-- 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])
⊢ 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])
-- 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
rw : p.roots.card = 2
rw₁ : Multiset.card (α := R) {x1, x2} = 2
rw₂ rw₃ : Eq (α := ℕ) 2 2
⊢ p.roots.card = p.natDegree

Tactic:
rw [hp_natDegree, hroots, Multiset.card_pair]

Premises used: Multiset.card_pair
-- 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
⊢ p.roots.card = p.natDegree

Tactic:
have hp_roots_card : p.roots.card = p.natDegree := by
    rw [hp_natDegree, hroots, Multiset.card_pair]
-- 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
⊢ 1 ≤ p.natDegree

Tactic:
simp [hp_natDegree]