awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
h₁ :
  s.esymm (s.card - k) =
    coeff
      (∑ j ∈ Finset.range (s.card + 1),
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
      k
⊢ coeff (prod (map (fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) s)) k =
    s.esymm (s.card - k)

Tactic:
convert! Polynomial.ext_iff.mp (prod_X_add_C_eq_sum_esymm s) k using 1

Premises used: Polynomial.ext_iff, Iff.mp, Multiset.prod_X_add_C_eq_sum_esymm
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
h₁ : s.esymm (s.card - k) = ∑ x ∈ Finset.range (s.card + 1), if k = s.card - x then s.esymm x else 0
⊢ s.esymm (s.card - k) =
    coeff
      (∑ j ∈ Finset.range (s.card + 1),
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
      k

Tactic:
simp_rw [finsetSum_coeff, coeff_C_mul_X_pow]

Premises used: Polynomial.finsetSum_coeff, Polynomial.coeff_C_mul_X_pow
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
h₁ : s.esymm (s.card - k) = if k = s.card - (s.card - k) then s.esymm (s.card - k) else 0
h₂ : ∀ b ∈ Finset.range (s.card + 1), b ≠ s.card - k → (if k = s.card - b then s.esymm b else 0) = 0
rw : s.card - k ∈ Finset.range (s.card + 1)
⊢ s.esymm (s.card - k) = ∑ x ∈ Finset.range (s.card + 1), if k = s.card - x then s.esymm x else 0

Tactic:
rw [Finset.sum_eq_single_of_mem (Multiset.card s - k) _]

Premises used: Finset.sum_eq_single_of_mem, HSub.hSub, Multiset.card
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.esymm (s.card - k) = if k = s.card - (s.card - k) then s.esymm (s.card - k) else 0

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ ∀ b ∈ Finset.range (s.card + 1), b ≠ s.card - k → (if k = s.card - b then s.esymm b else 0) = 0

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.card - k ∈ Finset.range (s.card + 1)

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
rw : (map r s).esymm ((map r s).card - k) = (map r s).esymm (s.card - k)
h₁ : k ≤ (map r s).card
⊢ coeff (prod (map (fun (i : σ) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r i) : R[X])) s)) k =
    (map r s).esymm (s.card - k)

Tactic:
rw [← Function.comp_def (f := fun r => X + C r) (g := r), ← map_map, prod_X_add_C_coeff]

Premises used: Polynomial.C, Multiset.prod_X_add_C_coeff, Function.comp_def, HAdd.hAdd, Multiset.map_map, Polynomial.X, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
rw rw₁ : (map r s).esymm (s.card - k) = (map r s).esymm (s.card - k)
⊢ (map r s).esymm ((map r s).card - k) = (map r s).esymm (s.card - k)

Tactic:
rw [s.card_map r]

Premises used: Multiset.card_map
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h h₁ : k ≤ s.card
⊢ k ≤ (map r s).card

Tactic:
rw [s.card_map r]

Premises used: Multiset.card_map
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
⊢ k ≤ s.card

Tactic:
assumption
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
σ : Type u_2
s : Finset σ
r : σ → R
k : ℕ
h : k ≤ #s
rw :
  Eq.{u_1 + 1} (α := R) (∑ t ∈ Finset.powersetCard (s.val.card - k) s, t.prod r)
    (∑ t ∈ Finset.powersetCard (#s - k) s, ∏ i ∈ t, r i)
⊢ Eq.{u_1 + 1} (α := R) (coeff (∏ i ∈ s, HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r i) : R[X])) k)
    (∑ t ∈ Finset.powersetCard (#s - k) s, ∏ i ∈ t, r i)

Tactic:
rw [Finset.prod, prod_X_add_C_coeff' _ r h, Finset.esymm_map_val]

Premises used: Finset.prod, Finset.esymm_map_val, Multiset.prod_X_add_C_coeff'
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
σ : Type u_2
s : Finset σ
r : σ → R
k : ℕ
h : k ≤ #s
⊢ Eq.{u_1 + 1} (α := R) (∑ t ∈ Finset.powersetCard (s.val.card - k) s, t.prod r)
    (∑ t ∈ Finset.powersetCard (#s - k) s, ∏ i ∈ t, r i)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
rw : ∀ x ∈ powersetCard k s, (prod ∘ map Neg.neg) x = HPow.hPow (α := R) (-1) k * x.prod
⊢ (map Neg.neg s).esymm k = HPow.hPow (α := R) (-1) k * s.esymm k

Tactic:
rw [esymm, esymm, ← Multiset.sum_map_mul_left, Multiset.powersetCard_map, Multiset.map_map,
    map_congr rfl]

Premises used: Multiset.map_congr, Multiset.powersetCard_map, Multiset.map_map, Multiset.esymm, rfl, Multiset.sum_map_mul_left
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
rw : (prod ∘ map Neg.neg) x = prod (map (Function.const R (-1)) x) * x.prod
⊢ (prod ∘ map Neg.neg) x = HPow.hPow (α := R) (-1) k * x.prod

Tactic:
rw [(mem_powersetCard.mp hx).right.symm, ← prod_replicate, ← Multiset.map_const]

Premises used: Multiset.prod_replicate, Multiset.mem_powersetCard, Multiset.map_const, And.right, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
nth_rw :
  (prod ∘ map Neg.neg) x = HMul.hMul (α := R) (prod (map (Function.const R (-1)) x)) (prod (map (fun (x : R) ↦ x) x))
⊢ (prod ∘ map Neg.neg) x = prod (map (Function.const R (-1)) x) * x.prod

Tactic:
nth_rw 3 [← map_id' x]

Premises used: Multiset.map_id'
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
rw : ∀ x_1 ∈ x, Function.const R (-1) x_1 * x_1 = -x_1
⊢ (prod ∘ map Neg.neg) x = HMul.hMul (α := R) (prod (map (Function.const R (-1)) x)) (prod (map (fun (x : R) ↦ x) x))

Tactic:
rw [← prod_map_mul, map_congr rfl, Function.comp_apply]

Premises used: Multiset.prod_map_mul, Multiset.map_congr, Function.comp_apply, rfl
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ ∀ x_1 ∈ x, Function.const R (-1) x_1 * x_1 = -x_1

Tactic:
fun z _ => neg_one_mul z

Premises used: neg_one_mul
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ ∀ x_1 ∈ x, Function.const R (-1) x_1 * x_1 = -x_1

Tactic:
exact fun z _ => neg_one_mul z

Premises used: neg_one_mul
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
a : map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s
| prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
a : fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])
a₁ : s
| map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
a : ∀ (x : R), HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])
| fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])

Tactic:
ext x
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
x : R
a : HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])
| HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) x : R[X])

Tactic:
rw [← map_neg C x]

Premises used: Polynomial.C, map_neg
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
a : ∀ (x : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])
a₁ : s
| prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)

Tactic:
congr
    congr
    ext x
    rw [sub_eq_add_neg]
    rw [← map_neg C x]

Premises used: sub_eq_add_neg
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
conv_lhs :
  Eq (α := R[X]) (prod (map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])) s))
    (∑ j ∈ Finset.range (s.card + 1),
      HPow.hPow (α := R[X]) (-1) j *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
⊢ Eq (α := R[X]) (prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s))
    (∑ j ∈ Finset.range (s.card + 1),
      HPow.hPow (α := R[X]) (-1) j *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))

Tactic:
conv_lhs =>
    congr
    congr
    ext x
    rw [sub_eq_add_neg]
    rw [← map_neg C x]

Premises used: sub_eq_add_neg
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
⊢ Eq (α := R[X])
    (prod
      (map (fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
        (map (fun (t : R) ↦ -t) s)))
    (∑ j ∈ Finset.range (card (α := R) (map (fun (t : R) ↦ -t) s) + 1),
      (C : (a : R) → R[X]) (esymm (map (fun (t : R) ↦ -t) s) j) *
        HPow.hPow (α := R[X]) X (card (α := R) (map (fun (t : R) ↦ -t) s) - j))

Tactic:
prod_X_add_C_eq_sum_esymm (map (fun t => -t) s)

Premises used: Multiset.map, Multiset.prod_X_add_C_eq_sum_esymm, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
h :
  Eq (α := R[X]) (prod (map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])) s))
    (prod
      (map (fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
        (map (fun (t : R) ↦ -t) s)))
h₁ :
  Eq.{u_1 + 1} (α := R[X])
    (∑ j ∈ Finset.range (s.card + 1),
      HPow.hPow (α := R[X]) (-1) j *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
    (∑ j ∈ Finset.range (card (α := R) (map (fun (t : R) ↦ -t) s) + 1),
      (C : (a : R) → R[X]) (esymm (map (fun (t : R) ↦ -t) s) j) *
        HPow.hPow (α := R[X]) X (card (α := R) (map (fun (t : R) ↦ -t) s) - j))
⊢ Eq (α := R[X]) (prod (map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])) s))
    (∑ j ∈ Finset.range (s.card + 1),
      HPow.hPow (α := R[X]) (-1) j *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))

Tactic:
convert! prod_X_add_C_eq_sum_esymm (map (fun t => -t) s) using 1

Premises used: Multiset.map, Multiset.prod_X_add_C_eq_sum_esymm, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
h :
  Eq (α := R[X]) (prod (map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])) s))
    (prod
      (map ((fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) ∘ fun (t : R) ↦ -t) s))
⊢ Eq (α := R[X]) (prod (map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])) s))
    (prod
      (map (fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
        (map (fun (t : R) ↦ -t) s)))

Tactic:
rw [map_map]

Premises used: Multiset.map_map
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
⊢ Eq (α := R[X]) (prod (map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])) s))
    (prod
      (map ((fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) ∘ fun (t : R) ↦ -t) s))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
⊢ Eq.{u_1 + 1} (α := R[X])
    (∑ j ∈ Finset.range (s.card + 1),
      HPow.hPow (α := R[X]) (-1) j *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
    (∑ j ∈ Finset.range (card (α := R) (map (fun (t : R) ↦ -t) s) + 1),
      (C : (a : R) → R[X]) (esymm (map (fun (t : R) ↦ -t) s) j) *
        HPow.hPow (α := R[X]) X (card (α := R) (map (fun (t : R) ↦ -t) s) - j))

Tactic:
simp only [esymm_neg, card_map, mul_assoc, map_mul, map_pow, map_neg, map_one]

Premises used: mul_assoc, map_neg, map_pow, map_mul, map_one, Multiset.esymm_neg, Multiset.card_map
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
a : prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)
a₁ : k
| coeff (prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)) k

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
a : map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s
| prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
a : fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])
a₁ : s
| map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
a : ∀ (x : R), HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])
| fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])

Tactic:
ext x
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
x : R
a : HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])
| HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) x : R[X])

Tactic:
rw [← map_neg C x]

Premises used: Polynomial.C, map_neg
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
a : ∀ (x : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])
a₁ : s
a₂ : k
| coeff (prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)) k

Tactic:
congr
    congr
    congr
    ext x
    rw [sub_eq_add_neg]
    rw [← map_neg C x]

Premises used: sub_eq_add_neg
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
conv_lhs :
  coeff (prod (map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])) s)) k =
    HPow.hPow (α := R) (-1) (s.card - k) * s.esymm (s.card - k)
⊢ coeff (prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)) k =
    HPow.hPow (α := R) (-1) (s.card - k) * s.esymm (s.card - k)

Tactic:
conv_lhs =>
    congr
    congr
    congr
    ext x
    rw [sub_eq_add_neg]
    rw [← map_neg C x]

Premises used: sub_eq_add_neg
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ Eq (α := R)
    (coeff
      (prod
        (map (fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
          (map (fun (t : R) ↦ -t) s)))
      k)
    (esymm (map (fun (t : R) ↦ -t) s) (card (α := R) (map (fun (t : R) ↦ -t) s) - k))

Tactic:
prod_X_add_C_coeff (map (fun t => -t) s) _

Premises used: Multiset.prod_X_add_C_coeff, Multiset.map, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
h₁ :
  Eq (α := R)
    (coeff (prod (map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])) s)) k)
    (coeff
      (prod
        (map (fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
          (map (fun (t : R) ↦ -t) s)))
      k)
h₂ :
  HPow.hPow (α := R) (-1) (s.card - k) * s.esymm (s.card - k) =
    esymm (map (fun (t : R) ↦ -t) s) (card (α := R) (map (fun (t : R) ↦ -t) s) - k)
convert_1 : ℕ
convert_2 : k ≤ card (α := R) (map (fun (t : R) ↦ -t) s)
⊢ coeff (prod (map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])) s)) k =
    HPow.hPow (α := R) (-1) (s.card - k) * s.esymm (s.card - k)

Tactic:
convert! prod_X_add_C_coeff (map (fun t => -t) s) _ using 1

Premises used: Multiset.prod_X_add_C_coeff, Multiset.map, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
h₁ :
  Eq (α := R)
    (coeff (prod (map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])) s)) k)
    (coeff
      (prod
        (map ((fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) ∘ fun (t : R) ↦ -t)
          s))
      k)
⊢ Eq (α := R)
    (coeff (prod (map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])) s)) k)
    (coeff
      (prod
        (map (fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
          (map (fun (t : R) ↦ -t) s)))
      k)

Tactic:
rw [map_map]

Premises used: Multiset.map_map
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ Eq (α := R)
    (coeff (prod (map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])) s)) k)
    (coeff
      (prod
        (map ((fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) ∘ fun (t : R) ↦ -t)
          s))
      k)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
h₁ :
  HPow.hPow (α := R) (-1) (s.card - k) * s.esymm (s.card - k) =
    HPow.hPow (α := R) (-1) (card (α := R) (map (fun (t : R) ↦ -t) s) - k) *
      s.esymm (card (α := R) (map (fun (t : R) ↦ -t) s) - k)
h₂ h₃ :
  HPow.hPow (α := R) (-1) (s.card - k) * s.esymm (s.card - k) =
    HPow.hPow (α := R) (-1) (s.card - k) * s.esymm (s.card - k)
⊢ HPow.hPow (α := R) (-1) (s.card - k) * s.esymm (s.card - k) =
    esymm (map (fun (t : R) ↦ -t) s) (card (α := R) (map (fun (t : R) ↦ -t) s) - k)

Tactic:
rw [esymm_neg, card_map]

Premises used: Multiset.esymm_neg, Multiset.card_map
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
h convert_2 convert_2₁ convert_2₂ convert_2₃ : k ≤ s.card
⊢ k ≤ card (α := R) (map (fun (t : R) ↦ -t) s)

Tactic:
rwa [card_map]

Premises used: Multiset.card_map
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
rw :
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
        (prod (map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) :
          R[X])).coeff
    k
| p.coeff k

Tactic:
rw [← C_leadingCoeff_mul_prod_multiset_X_sub_C hroots]

Premises used: Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
conv_lhs :
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (prod (map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) :
            R[X])).coeff
      k =
    p.leadingCoeff * HPow.hPow (α := R) (-1) (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
⊢ p.coeff k = p.leadingCoeff * HPow.hPow (α := R) (-1) (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Tactic:
conv_lhs => rw [← C_leadingCoeff_mul_prod_multiset_X_sub_C hroots]

Premises used: Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
rw :
  p.leadingCoeff *
      coeff (prod (map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots)) k =
    p.leadingCoeff * (HPow.hPow (α := R) (-1) (p.natDegree - k) * p.roots.esymm (p.natDegree - k))
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (prod (map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots) :
            R[X])).coeff
      k =
    p.leadingCoeff * HPow.hPow (α := R) (-1) (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Tactic:
rw [coeff_C_mul, mul_assoc]

Premises used: mul_assoc, Polynomial.coeff_C_mul
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
e_a :
  coeff (prod (map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots)) k =
    HPow.hPow (α := R) (-1) (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
⊢ p.leadingCoeff *
      coeff (prod (map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots)) k =
    p.leadingCoeff * (HPow.hPow (α := R) (-1) (p.natDegree - k) * p.roots.esymm (p.natDegree - k))

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h rw : k ≤ p.natDegree
⊢ k ≤ p.roots.card

Tactic:
rw [hroots]
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ k ≤ p.natDegree

Tactic:
h
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ k ≤ p.natDegree

Tactic:
exact h
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ k ≤ p.roots.card

Tactic:
have : k ≤ card (roots p) := by rw [hroots]; exact h
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
this : k ≤ p.roots.card
⊢ coeff (prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) p.roots)) k =
    HPow.hPow (α := R) (-1) (p.roots.card - k) * p.roots.esymm (p.roots.card - k)

Tactic:
p.roots.prod_X_sub_C_coeff this

Premises used: Polynomial.roots, Multiset.prod_X_sub_C_coeff
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
this : k ≤ p.roots.card
h₁ h₂ : p.natDegree - k = p.roots.card - k
⊢ coeff (prod (map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p.roots)) k =
    HPow.hPow (α := R) (-1) (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Tactic:
convert! p.roots.prod_X_sub_C_coeff this using 3

Premises used: Polynomial.roots, Multiset.prod_X_sub_C_coeff