awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k ∧ ¬0 < a.1,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
⊢ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}
have h₁ : ∀ (a : ℕ × ℕ),
  a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k ∧ ¬0 < a.1} ↔ Membership.mem (γ := Finset (ℕ × ℕ)) {(0, k)} a
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k ∧ ¬0 < a.1,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
⊢ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k ∧ ¬0 < a.1} ↔ Membership.mem (γ := Finset (ℕ × ℕ)) {(0, k)} a
have h₁ : a.1 + a.2 = k ∧ a.1 < k ∧ ¬0 < a.1 ↔ a = (0, k)
Tactic: rw [mem_filter, mem_antidiagonal, mem_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k ∧ ¬0 < a.1,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
⊢ a.1 + a.2 = k ∧ a.1 < k ∧ ¬0 < a.1 ↔ a = (0, k)
have h₁ : a.1 + a.2 = k ∧ a.1 < k ∧ ¬0 < a.1 → a = (0, k)
Tactic: refine ⟨?_, by rintro rfl; lia⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k ∧ ¬0 < a.1,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
ha : a.1 + a.2 = k
left : a.1 < k
ha0 : ¬0 < a.1
⊢ a = (0, k)
have h₁ : a = (0, a.1 + a.2)
Tactic: rw [← ha, Nat.eq_zero_of_not_pos ha0, zero_add, ← Nat.eq_zero_of_not_pos ha0]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k ∧ ¬0 < a.1,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
ha : a.1 + a.2 = k
left : a.1 < k
ha0 : ¬0 < a.1
h₁ : a = (0, a.1 + a.2)
⊢ a = (0, k)
have h₂ : a = (0, 0 + a.2)
Tactic: rw [← ha, Nat.eq_zero_of_not_pos ha0, zero_add, ← Nat.eq_zero_of_not_pos ha0]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k ∧ ¬0 < a.1,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
ha : a.1 + a.2 = k
left : a.1 < k
ha0 : ¬0 < a.1
h₁ : a = (0, a.1 + a.2)
h₂ : a = (0, 0 + a.2)
⊢ a = (0, k)
have h₃ : a = (0, a.2)
Tactic: rw [← ha, Nat.eq_zero_of_not_pos ha0, zero_add, ← Nat.eq_zero_of_not_pos ha0]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k ∧ ¬0 < a.1,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
ha : a.1 + a.2 = k
left : a.1 < k
ha0 : ¬0 < a.1
h₁ : a = (0, a.1 + a.2)
h₂ : a = (0, 0 + a.2)
h₃ : a = (0, a.2)
⊢ a = (0, k)
have h₄ : a = (a.1, a.2)
Tactic: rw [← ha, Nat.eq_zero_of_not_pos ha0, zero_add, ← Nat.eq_zero_of_not_pos ha0]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (hypothesis)
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k ∧ ¬0 < a.1,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
⊢ psum σ R k =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ x ∈ @antidiagonal _ instAddMonoid _ k with x.1 < k ∧ 0 < x.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2
have this : {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}
Tactic: have : {a ∈ antidiagonal k | a.fst < k ∧ ¬0 < a.fst} = {(0, k)} := by
    ext a
    rw [mem_filter, mem_antidiagonal, mem_singleton]
    refine ⟨?_, by rintro rfl; lia⟩
    rintro ⟨ha, ⟨_, ha0⟩⟩
    rw [← ha, Nat.eq_zero_of_not_pos ha0, zero_add, ← Nat.eq_zero_of_not_pos ha0]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (hypothesis)
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k ∧ ¬0 < a.1,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
this : {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}
⊢ psum σ R k =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ x ∈ @antidiagonal _ instAddMonoid _ k with x.1 < k ∧ 0 < x.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2
have sub_both_sides₁ : HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
    ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
  HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (-1) (0, k).1 * esymm σ R (0, k).1 * psum σ R (0, k).2
Tactic: rw [this, sum_singleton] at sub_both_sides
Cleared hypotheses: sub_both_sides, this
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (hypothesis)
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (-1) (0, k).1 * esymm σ R (0, k).1 * psum σ R (0, k).2
this : {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}
⊢ psum σ R k =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ x ∈ @antidiagonal _ instAddMonoid _ k with x.1 < k ∧ 0 < x.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2
have sub_both_sides₁ : HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
    ∑ x ∈ @antidiagonal _ instAddMonoid _ k with x.1 < k ∧ 0 < x.1,
      HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2 =
  psum σ R k
Tactic: simp only [_root_.pow_zero, esymm_zero, mul_one, one_mul, filter_filter] at sub_both_sides
Cleared hypotheses: sub_both_sides
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : σ → B
p : MvPolynomial σ R
⊢ Eq.{u_3 + 1} (α := B)
    ((aeval x : (a : MvPolynomial σ A) → B)
        ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) p : MvPolynomial σ A) :
      B)
    ((aeval x : (a : MvPolynomial σ R) → B) p : B)
have rw : eval₂ (algebraMap A B) x ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) p) =
  (aeval x : (a : MvPolynomial σ R) → B) p
Tactic: rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : σ → B
p : MvPolynomial σ R
rw :
  eval₂ (algebraMap A B) x ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) p) =
    (aeval x : (a : MvPolynomial σ R) → B) p
⊢ Eq.{u_3 + 1} (α := B)
    ((aeval x : (a : MvPolynomial σ A) → B)
        ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) p : MvPolynomial σ A) :
      B)
    ((aeval x : (a : MvPolynomial σ R) → B) p : B)
have rw₁ : eval₂ (algebraMap A B) x ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) p) =
  eval₂ (algebraMap R B) x p
Tactic: rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : σ → B
p : MvPolynomial σ R
rw :
  eval₂ (algebraMap A B) x ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) p) =
    (aeval x : (a : MvPolynomial σ R) → B) p
rw₁ :
  eval₂ (algebraMap A B) x ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) p) =
    eval₂ (algebraMap R B) x p
⊢ Eq.{u_3 + 1} (α := B)
    ((aeval x : (a : MvPolynomial σ A) → B)
        ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) p : MvPolynomial σ A) :
      B)
    ((aeval x : (a : MvPolynomial σ R) → B) p : B)
have rw₂ : eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) x p =
  eval₂ (algebraMap R B) x p
Tactic: rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : σ → B
p : MvPolynomial σ R
rw :
  eval₂ (algebraMap A B) x ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) p) =
    (aeval x : (a : MvPolynomial σ R) → B) p
rw₁ :
  eval₂ (algebraMap A B) x ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) p) =
    eval₂ (algebraMap R B) x p
rw₂ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) x p =
    eval₂ (algebraMap R B) x p
⊢ Eq.{u_3 + 1} (α := B)
    ((aeval x : (a : MvPolynomial σ A) → B)
        ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) p : MvPolynomial σ A) :
      B)
    ((aeval x : (a : MvPolynomial σ R) → B) p : B)
have rw₃ : eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) x p =
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) x p
Tactic: rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]