awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
rw :
  Eq (α := R[X])
    (sum
      (map
        (fun (p : Multiset R × Multiset R) ↦
          HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2)))
        s.antidiagonal))
    (∑ 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)))
rw₁ :
  Eq (α := R[X])
    (sum
      (map
        (fun (p : Multiset R × Multiset R) ↦
          HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2)))
        (map (fun (t : Multiset R) ↦ (s - t, t)) s.powerset)))
    (∑ 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)))
⊢ Eq (α := R[X]) (prod (map (fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) s))
    (∑ 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)))
have rw₂ : Eq (α := R[X])
  (sum
    (map
      ((fun (p : Multiset R × Multiset R) ↦
          HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
        fun (t : Multiset R) ↦ (s - t, t))
      s.powerset))
  (∑ 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)))
Tactic: classical
    rw [prod_map_add, antidiagonal_eq_map_powerset, map_map, ← bind_powerset_len,
      map_bind, sum_bind, Finset.sum_eq_multiset_sum, Finset.range_val, map_congr (Eq.refl _)]
    intro _ _
    rw [esymm, ← sum_hom', ← sum_map_mul_right, map_congr (Eq.refl _)]
    intro s ht
    rw [mem_powersetCard] at ht
    dsimp
    rw [prod_hom' s (Polynomial.C : R →+* R[X])]
    simp [ht, prod_replicate, map_id', card_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
rw :
  Eq (α := R[X])
    (sum
      (map
        (fun (p : Multiset R × Multiset R) ↦
          HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2)))
        s.antidiagonal))
    (∑ 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)))
rw₁ :
  Eq (α := R[X])
    (sum
      (map
        (fun (p : Multiset R × Multiset R) ↦
          HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2)))
        (map (fun (t : Multiset R) ↦ (s - t, t)) s.powerset)))
    (∑ 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)))
rw₂ :
  Eq (α := R[X])
    (sum
      (map
        ((fun (p : Multiset R × Multiset R) ↦
            HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
          fun (t : Multiset R) ↦ (s - t, t))
        s.powerset))
    (∑ 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)))
⊢ Eq (α := R[X]) (prod (map (fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) s))
    (∑ 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)))
have rw₃ : Eq.{u_1 + 1} (α := R[X])
  (sum
    (map (α := Multiset R)
      ((fun (p : Multiset R × Multiset R) ↦
          HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
        fun (t : Multiset R) ↦ (s - t, t))
      ((range (s.card + 1)).bind fun (k : ℕ) ↦ powersetCard k s)))
  (∑ 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)))
Tactic: classical
    rw [prod_map_add, antidiagonal_eq_map_powerset, map_map, ← bind_powerset_len,
      map_bind, sum_bind, Finset.sum_eq_multiset_sum, Finset.range_val, map_congr (Eq.refl _)]
    intro _ _
    rw [esymm, ← sum_hom', ← sum_map_mul_right, map_congr (Eq.refl _)]
    intro s ht
    rw [mem_powersetCard] at ht
    dsimp
    rw [prod_hom' s (Polynomial.C : R →+* R[X])]
    simp [ht, prod_replicate, map_id', card_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
rw :
  Eq (α := R[X])
    (sum
      (map
        (fun (p : Multiset R × Multiset R) ↦
          HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2)))
        s.antidiagonal))
    (∑ 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)))
rw₁ :
  Eq (α := R[X])
    (sum
      (map
        (fun (p : Multiset R × Multiset R) ↦
          HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2)))
        (map (fun (t : Multiset R) ↦ (s - t, t)) s.powerset)))
    (∑ 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)))
rw₂ :
  Eq (α := R[X])
    (sum
      (map
        ((fun (p : Multiset R × Multiset R) ↦
            HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
          fun (t : Multiset R) ↦ (s - t, t))
        s.powerset))
    (∑ 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)))
rw₃ :
  Eq.{u_1 + 1} (α := R[X])
    (sum
      (map (α := Multiset R)
        ((fun (p : Multiset R × Multiset R) ↦
            HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
          fun (t : Multiset R) ↦ (s - t, t))
        ((range (s.card + 1)).bind fun (k : ℕ) ↦ powersetCard k s)))
    (∑ 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)))
⊢ Eq (α := R[X]) (prod (map (fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) s))
    (∑ 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)))
have rw₄ : Eq.{u_1 + 1} (α := R[X])
  (sum
    ((range (s.card + 1)).bind fun (a : ℕ) ↦
      map
        ((fun (p : Multiset R × Multiset R) ↦
            HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
          fun (t : Multiset R) ↦ (s - t, t))
        (powersetCard a s)))
  (∑ 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)))
Tactic: classical
    rw [prod_map_add, antidiagonal_eq_map_powerset, map_map, ← bind_powerset_len,
      map_bind, sum_bind, Finset.sum_eq_multiset_sum, Finset.range_val, map_congr (Eq.refl _)]
    intro _ _
    rw [esymm, ← sum_hom', ← sum_map_mul_right, map_congr (Eq.refl _)]
    intro s ht
    rw [mem_powersetCard] at ht
    dsimp
    rw [prod_hom' s (Polynomial.C : R →+* R[X])]
    simp [ht, prod_replicate, map_id', card_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ 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)
have 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
Tactic: convert! Polynomial.ext_iff.mp (prod_X_add_C_eq_sum_esymm s) k using 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ 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
have h₁ : s.esymm (s.card - k) = ∑ x ∈ Finset.range (s.card + 1), if k = s.card - x then s.esymm x else 0
Tactic: simp_rw [finsetSum_coeff, coeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ s.card
⊢ s.esymm (s.card - k) = ∑ x ∈ Finset.range (s.card + 1), if k = s.card - x then s.esymm x else 0
have h₁ : s.esymm (s.card - k) = if k = s.card - (s.card - k) then s.esymm (s.card - k) else 0
Tactic: rw [Finset.sum_eq_single_of_mem (Multiset.card s - k) _]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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
⊢ s.esymm (s.card - k) = ∑ x ∈ Finset.range (s.card + 1), if k = s.card - x then s.esymm x else 0
have h₂ : ∀ b ∈ Finset.range (s.card + 1), b ≠ s.card - k → (if k = s.card - b then s.esymm b else 0) = 0
Tactic: rw [Finset.sum_eq_single_of_mem (Multiset.card s - k) _]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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
⊢ s.esymm (s.card - k) = ∑ x ∈ Finset.range (s.card + 1), if k = s.card - x then s.esymm x else 0
have rw : s.card - k ∈ Finset.range (s.card + 1)
Tactic: rw [Finset.sum_eq_single_of_mem (Multiset.card s - k) _]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ 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)
have rw : (map r s).esymm ((map r s).card - 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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)
⊢ 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)
have h₁ : k ≤ (map r s).card
Tactic: rw [← Function.comp_def (f := fun r => X + C r) (g := r), ← map_map, prod_X_add_C_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
⊢ (map r s).esymm ((map r s).card - k) = (map r s).esymm (s.card - k)
have rw : (map r s).esymm (s.card - k) = (map r s).esymm (s.card - k)
Tactic: rw [s.card_map r]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommSemiring R
σ : Type u_2
s : Finset σ
r : σ → R
k : ℕ
h : k ≤ #s
⊢ 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)
have 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)
Tactic: rw [Finset.prod, prod_X_add_C_coeff' _ r h, Finset.esymm_map_val]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
⊢ (map Neg.neg s).esymm k = HPow.hPow (α := R) (-1) k * s.esymm k
have rw : ∀ x ∈ powersetCard k s, (prod ∘ map Neg.neg) x = HPow.hPow (α := R) (-1) k * x.prod
Tactic: rw [esymm, esymm, ← Multiset.sum_map_mul_left, Multiset.powersetCard_map, Multiset.map_map,
    map_congr rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = HPow.hPow (α := R) (-1) k * x.prod
have rw : (prod ∘ map Neg.neg) x = prod (map (Function.const R (-1)) x) * x.prod
Tactic: rw [(mem_powersetCard.mp hx).right.symm, ← prod_replicate, ← Multiset.map_const]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = prod (map (Function.const R (-1)) x) * x.prod
have nth_rw : (prod ∘ map Neg.neg) x = HMul.hMul (α := R) (prod (map (Function.const R (-1)) x)) (prod (map (fun (x : R) ↦ x) x))
Tactic: nth_rw 3 [← map_id' x]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = HMul.hMul (α := R) (prod (map (Function.const R (-1)) x)) (prod (map (fun (x : R) ↦ x) x))
have rw : ∀ x_1 ∈ x, Function.const R (-1) x_1 * x_1 = -x_1
Tactic: rw [← prod_map_mul, map_congr rfl, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
| prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)
have a : map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
| map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s
have a : fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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])
| map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s
have a₁ : s
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
| fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])
have a : ∀ (x : R), HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
x : R
| HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) x : R[X])
have a : HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])
Tactic: rw [← map_neg C x]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
| prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)
have a : ∀ (x : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])
Tactic: congr
    congr
    ext x
    rw [sub_eq_add_neg]
    rw [← map_neg C x]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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])
| prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)
have a₁ : s
Tactic: congr
    congr
    ext x
    rw [sub_eq_add_neg]
    rw [← map_neg C x]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
Goal:
R : Type u_1
inst : CommRing R
s : Multiset R
⊢ 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)))
have 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)))
Tactic: conv_lhs =>
    congr
    congr
    ext x
    rw [sub_eq_add_neg]
    rw [← map_neg C x]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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))
    (∑ 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)))
have 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)))
Tactic: convert! prod_X_add_C_eq_sum_esymm (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
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)))
⊢ 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)))
have 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))
Tactic: convert! prod_X_add_C_eq_sum_esymm (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
⊢ 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)))
have 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))
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
| coeff (prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)) k
have a : prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)
Tactic: congr
-- 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
a : prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)
| coeff (prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)) k
have a₁ : k
Tactic: congr
-- 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
| prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)
have a : map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s
Tactic: congr
-- 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
| map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s
have a : fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])
Tactic: congr
-- 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
a : fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])
| map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s
have a₁ : s
Tactic: congr
-- 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
| fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])
have a : ∀ (x : R), HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])
Tactic: ext x
-- 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
x : R
| HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) x : R[X])
have a : HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])
Tactic: rw [← map_neg C x]
-- 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
| coeff (prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)) k
have a : ∀ (x : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])
Tactic: congr
    congr
    congr
    ext x
    rw [sub_eq_add_neg]
    rw [← map_neg C x]
-- 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
a : ∀ (x : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])
| coeff (prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)) k
have a₁ : s
Tactic: congr
    congr
    congr
    ext x
    rw [sub_eq_add_neg]
    rw [← map_neg C x]
-- 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
a : ∀ (x : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-x) : R[X])
a₁ : s
| coeff (prod (map (fun (t : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) s)) k
have a₂ : k
Tactic: congr
    congr
    congr
    ext x
    rw [sub_eq_add_neg]
    rw [← map_neg C x]
-- 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
⊢ 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)
have 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)
Tactic: conv_lhs =>
    congr
    congr
    congr
    ext x
    rw [sub_eq_add_neg]
    rw [← map_neg C x]
-- 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
⊢ 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₁ : 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: convert! prod_X_add_C_coeff (map (fun t => -t) s) _ using 1