awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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)
⊢ 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)
have 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)
Tactic: convert! prod_X_add_C_coeff (map (fun t => -t) s) _ using 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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 : ℕ
⊢ 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)
have convert_2 : k ≤ card (α := R) (map (fun (t : R) ↦ -t) s)
Tactic: convert! prod_X_add_C_coeff (map (fun t => -t) s) _ using 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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]))
          (map (fun (t : R) ↦ -t) s)))
      k)
have 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)
Tactic: rw [map_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ 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)
have 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)
Tactic: rw [esymm_neg, card_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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)
⊢ 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)
have 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)
Tactic: rw [esymm_neg, card_map]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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
| p.coeff k
have 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
Tactic: rw [← C_leadingCoeff_mul_prod_multiset_X_sub_C hroots]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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
⊢ p.coeff k = p.leadingCoeff * HPow.hPow (α := R) (-1) (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
have 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)
Tactic: conv_lhs => rw [← C_leadingCoeff_mul_prod_multiset_X_sub_C hroots]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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
⊢ (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)
have 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))
Tactic: rw [coeff_C_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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
⊢ 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))
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (hypothesis)
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
⊢ 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)
have this : k ≤ p.roots.card
Tactic: have : k ≤ card (roots p) := by rw [hroots]; exact h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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 (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)
have h₁ : p.natDegree - k = p.roots.card - k
Tactic: convert! p.roots.prod_X_sub_C_coeff this using 3
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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
⊢ p.natDegree - k = p.roots.card - k
have h₁ : p.natDegree - k = p.natDegree - k
Tactic: rw [hroots]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
⊢ Fintype.card σ = s.card
have rw : Fintype.card σ = Multiset.card.{u_2} (α := σ) (val univ)
Tactic: rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
rw : Fintype.card σ = Multiset.card.{u_2} (α := σ) (val univ)
⊢ Fintype.card σ = s.card
have rw₁ : Finset.card.{u_2} (α := σ) univ = Multiset.card.{u_2} (α := σ) (val univ)
Tactic: rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
rw : Fintype.card σ = Multiset.card.{u_2} (α := σ) (val univ)
rw₁ : Finset.card.{u_2} (α := σ) univ = Multiset.card.{u_2} (α := σ) (val univ)
⊢ Fintype.card σ = s.card
have rw₂ : Multiset.card.{u_2} (α := σ) (val univ) = Multiset.card.{u_2} (α := σ) (val univ)
Tactic: rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (hypothesis)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
⊢ Eq (α := (MvPolynomial σ R)[X])
    (∏ i : σ,
      HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
        ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
    (∑ j ∈ range (Fintype.card σ + 1),
      HMul.hMul (α := (MvPolynomial σ R)[X])
        ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (esymm σ R j) : (MvPolynomial σ R)[X])
        (HPow.hPow (α := (MvPolynomial σ R)[X]) Polynomial.X (Fintype.card σ - j)))
have this : Fintype.card σ = s.card
Tactic: have : Fintype.card σ = Multiset.card s := by
    rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
this : Fintype.card σ = s.card
⊢ Eq (α := (MvPolynomial σ R)[X])
    (∏ i : σ,
      HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
        ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
    (∑ j ∈ range (Fintype.card σ + 1),
      HMul.hMul (α := (MvPolynomial σ R)[X])
        ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (esymm σ R j) : (MvPolynomial σ R)[X])
        (HPow.hPow (α := (MvPolynomial σ R)[X]) Polynomial.X (Fintype.card σ - j)))
have simp_rw : Eq (α := (MvPolynomial σ R)[X])
  (Multiset.prod
    (Multiset.map
      (fun (i : σ) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      (val univ)))
  (∑ x ∈ range (s.card + 1),
    HMul.hMul (α := (MvPolynomial σ R)[X])
      ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (Multiset.esymm (Multiset.map X (val univ)) x) :
        (MvPolynomial σ R)[X])
      (HPow.hPow (α := (MvPolynomial σ R)[X]) Polynomial.X (s.card - x)))
Tactic: simp_rw [this, MvPolynomial.esymm_eq_multiset_esymm σ R, Finset.prod_eq_multiset_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
this : Fintype.card σ = s.card
⊢ Eq (α := (MvPolynomial σ R)[X])
    (Multiset.prod
      (Multiset.map
        (fun (i : σ) ↦
          HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
            ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
        (val univ)))
    (∑ x ∈ range (s.card + 1),
      HMul.hMul (α := (MvPolynomial σ R)[X])
        ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X])
            (Multiset.esymm (Multiset.map X (val univ)) x) :
          (MvPolynomial σ R)[X])
        (HPow.hPow (α := (MvPolynomial σ R)[X]) Polynomial.X (s.card - x)))
have h : Eq (α := Multiset (MvPolynomial σ R)[X])
  (Multiset.map
    (fun (i : σ) ↦
      HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
        ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
    (val univ))
  (Multiset.map
    (fun (r : MvPolynomial σ R) ↦
      HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
        ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X]))
    s)
Tactic: convert! Multiset.prod_X_add_C_eq_sum_esymm s
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
this : Fintype.card σ = s.card
h :
  Eq (α := Multiset (MvPolynomial σ R)[X])
    (Multiset.map
      (fun (i : σ) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      (val univ))
    (Multiset.map
      (fun (r : MvPolynomial σ R) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X]))
      (Multiset.map (fun (i : σ) ↦ X i) (val univ)))
⊢ Eq (α := Multiset (MvPolynomial σ R)[X])
    (Multiset.map
      (fun (i : σ) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      (val univ))
    (Multiset.map
      (fun (r : MvPolynomial σ R) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X]))
      s)
have h₁ : Eq (α := Multiset (MvPolynomial σ R)[X])
  (Multiset.map
    (fun (i : σ) ↦
      HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
        ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
    (val univ))
  (Multiset.map (α := σ)
    ((fun (r : MvPolynomial σ R) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X])) ∘
      fun (i : σ) ↦ X i)
    (val univ))
Tactic: simp_rw [s, Multiset.map_map, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
⊢ Fintype.card σ = s.card
have rw : Fintype.card σ = Multiset.card.{u_2} (α := σ) (val univ)
Tactic: rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
rw : Fintype.card σ = Multiset.card.{u_2} (α := σ) (val univ)
⊢ Fintype.card σ = s.card
have rw₁ : Finset.card.{u_2} (α := σ) univ = Multiset.card.{u_2} (α := σ) (val univ)
Tactic: rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
rw : Fintype.card σ = Multiset.card.{u_2} (α := σ) (val univ)
rw₁ : Finset.card.{u_2} (α := σ) univ = Multiset.card.{u_2} (α := σ) (val univ)
⊢ Fintype.card σ = s.card
have rw₂ : Multiset.card.{u_2} (α := σ) (val univ) = Multiset.card.{u_2} (α := σ) (val univ)
Tactic: rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (hypothesis)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
⊢ Eq (α := MvPolynomial σ R)
    (Polynomial.coeff
      (∏ i : σ,
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      k)
    (esymm σ R (Fintype.card σ - k))
have this : Fintype.card σ = s.card
Tactic: have : Fintype.card σ = Multiset.card s := by
    rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
this : Fintype.card σ = s.card
⊢ Eq (α := MvPolynomial σ R)
    (Polynomial.coeff
      (∏ i : σ,
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      k)
    (esymm σ R (Fintype.card σ - k))
have rw : ∀ (h : k ≤ s.card) (this : Fintype.card σ = s.card),
  Eq (α := MvPolynomial σ R)
    (Polynomial.coeff
      (∏ i : σ,
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      k)
    (esymm σ R (s.card - k))
Tactic: rw [this] at h ⊢
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
h : k ≤ s.card
this : Fintype.card σ = s.card
⊢ Eq (α := MvPolynomial σ R)
    (Polynomial.coeff
      (∏ i : σ,
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      k)
    (esymm σ R (s.card - k))
have rw : Eq (α := MvPolynomial σ R)
  (Polynomial.coeff
    (Multiset.prod
      (Multiset.map
        (fun (i : σ) ↦
          HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
            ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
        (val univ)))
    k)
  (Multiset.esymm (Multiset.map X (val univ)) (s.card - k))
Tactic: rw [MvPolynomial.esymm_eq_multiset_esymm σ R, Finset.prod_eq_multiset_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
h : k ≤ s.card
this : Fintype.card σ = s.card
⊢ Eq (α := MvPolynomial σ R)
    (Polynomial.coeff
      (Multiset.prod
        (Multiset.map
          (fun (i : σ) ↦
            HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
              ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
          (val univ)))
      k)
    (Multiset.esymm (Multiset.map X (val univ)) (s.card - k))
have h₁ : Eq (α := Semiring (MvPolynomial σ R)) AddMonoidAlgebra.semiring CommSemiring.toSemiring →
  Eq (α := Multiset (MvPolynomial σ R)[X])
    (Multiset.map
      (fun (i : σ) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      (val univ))
    (Multiset.map
      (fun (r : MvPolynomial σ R) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X]))
      s)
Tactic: convert! Multiset.prod_X_add_C_coeff s h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
h : k ≤ s.card
this : Fintype.card σ = s.card
e_2 : Eq (α := Semiring (MvPolynomial σ R)) AddMonoidAlgebra.semiring CommSemiring.toSemiring
h₁ :
  Eq (α := Multiset (MvPolynomial σ R)[X])
    (Multiset.map
      (fun (i : σ) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      (val univ))
    (Multiset.map
      (fun (r : MvPolynomial σ R) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X]))
      (Multiset.map (fun (i : σ) ↦ X i) (val univ)))
⊢ Eq (α := Multiset (MvPolynomial σ R)[X])
    (Multiset.map
      (fun (i : σ) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      (val univ))
    (Multiset.map
      (fun (r : MvPolynomial σ R) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X]))
      s)
have h₂ : Eq (α := Multiset (MvPolynomial σ R)[X])
  (Multiset.map
    (fun (i : σ) ↦
      HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
        ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
    (val univ))
  (Multiset.map (α := σ)
    ((fun (r : MvPolynomial σ R) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X])) ∘
      fun (i : σ) ↦ X i)
    (val univ))
Tactic: simp_rw [s, Multiset.map_map, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R[X]
⊢ wronskian 0 a = 0
have rw : Eq (α := R[X]) ((0 : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])
Tactic: rw [← wronskianBilin_apply 0 a, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R[X]
⊢ a.wronskian a = 0
have rw : HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) a : R[X]) -
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) a =
  0
Tactic: rw [wronskian, mul_comm, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Wronskian (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R[X]
rw :
  HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) a : R[X]) -
      HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) a =
    0
⊢ a.wronskian a = 0
have rw₁ : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) a -
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) a =
  0
Tactic: rw [wronskian, mul_comm, sub_self]