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 : ℕ
rw :
  HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
rw₁ :
  HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t
rw₂ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t
⊢ HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
have rw₃ : HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t -
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
  0
Tactic: classical
  rw [NewtonIdentities.esymm_to_weight σ R k, NewtonIdentities.esymm_mul_psum_to_weight σ R k,
    eq_comm, ← sub_eq_zero, sub_eq_add_neg, neg_mul_eq_neg_mul,
    neg_eq_neg_one_mul ((-1 : MvPolynomial σ R) ^ k)]
  nth_rw 2 [← pow_one (-1 : MvPolynomial σ R)]
  rw [← pow_add, add_comm 1 k, ← left_distrib,
    ← sum_disjUnion (NewtonIdentities.disjoint_filter_pairs_lt_filter_pairs_eq σ k),
    NewtonIdentities.disjUnion_filter_pairs_eq_pairs σ k, NewtonIdentities.weight_sum σ R k,
    neg_one_pow_mul_eq_zero_iff.mpr rfl]
-- 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 : ℕ
rw :
  HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
rw₁ :
  HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t
rw₂ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t
rw₃ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t -
      HPow.hPow (α := MvPolynomial σ R) (-1) k *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    0
⊢ HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
have rw₄ : HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
    -(HPow.hPow (α := MvPolynomial σ R) (-1) k *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t) =
  0
Tactic: classical
  rw [NewtonIdentities.esymm_to_weight σ R k, NewtonIdentities.esymm_mul_psum_to_weight σ R k,
    eq_comm, ← sub_eq_zero, sub_eq_add_neg, neg_mul_eq_neg_mul,
    neg_eq_neg_one_mul ((-1 : MvPolynomial σ R) ^ k)]
  nth_rw 2 [← pow_one (-1 : MvPolynomial σ R)]
  rw [← pow_add, add_comm 1 k, ← left_distrib,
    ← sum_disjUnion (NewtonIdentities.disjoint_filter_pairs_lt_filter_pairs_eq σ k),
    NewtonIdentities.disjUnion_filter_pairs_eq_pairs σ k, NewtonIdentities.weight_sum σ R k,
    neg_one_pow_mul_eq_zero_iff.mpr rfl]
-- 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 : ℕ
rw :
  HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
rw₁ :
  HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t
rw₂ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t
rw₃ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t -
      HPow.hPow (α := MvPolynomial σ R) (-1) k *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    0
rw₄ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
      -(HPow.hPow (α := MvPolynomial σ R) (-1) k *
          ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t) =
    0
⊢ HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
have rw₅ : HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
    -HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
  0
Tactic: classical
  rw [NewtonIdentities.esymm_to_weight σ R k, NewtonIdentities.esymm_mul_psum_to_weight σ R k,
    eq_comm, ← sub_eq_zero, sub_eq_add_neg, neg_mul_eq_neg_mul,
    neg_eq_neg_one_mul ((-1 : MvPolynomial σ R) ^ k)]
  nth_rw 2 [← pow_one (-1 : MvPolynomial σ R)]
  rw [← pow_add, add_comm 1 k, ← left_distrib,
    ← sum_disjUnion (NewtonIdentities.disjoint_filter_pairs_lt_filter_pairs_eq σ k),
    NewtonIdentities.disjUnion_filter_pairs_eq_pairs σ k, NewtonIdentities.weight_sum σ R k,
    neg_one_pow_mul_eq_zero_iff.mpr rfl]
-- 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 : ℕ
rw :
  HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
rw₁ :
  HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t
rw₂ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t
rw₃ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t -
      HPow.hPow (α := MvPolynomial σ R) (-1) k *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    0
rw₄ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
      -(HPow.hPow (α := MvPolynomial σ R) (-1) k *
          ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t) =
    0
rw₅ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
      -HPow.hPow (α := MvPolynomial σ R) (-1) k *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    0
⊢ HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
have rw₆ : HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
    -1 * HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
  0
Tactic: classical
  rw [NewtonIdentities.esymm_to_weight σ R k, NewtonIdentities.esymm_mul_psum_to_weight σ R k,
    eq_comm, ← sub_eq_zero, sub_eq_add_neg, neg_mul_eq_neg_mul,
    neg_eq_neg_one_mul ((-1 : MvPolynomial σ R) ^ k)]
  nth_rw 2 [← pow_one (-1 : MvPolynomial σ R)]
  rw [← pow_add, add_comm 1 k, ← left_distrib,
    ← sum_disjUnion (NewtonIdentities.disjoint_filter_pairs_lt_filter_pairs_eq σ k),
    NewtonIdentities.disjUnion_filter_pairs_eq_pairs σ k, NewtonIdentities.weight_sum σ R k,
    neg_one_pow_mul_eq_zero_iff.mpr rfl]
-- 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 : ℕ := Fintype.card σ
⊢ Eq (α := MvPolynomial σ R)
    (∑ a ∈ @antidiagonal _ instAddMonoid _ (Fintype.card σ),
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2)
    0
have suffices : HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
    ∑ a ∈ @antidiagonal _ instAddMonoid _ k, HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
  0
Tactic: suffices (-1 : MvPolynomial σ R) ^ (k + 1) *
      ∑ a ∈ antidiagonal k, (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd = 0 by
    simpa using this
-- 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
⊢ psum σ R k =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 ∈ Set.Ioo 0 k,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
have simp : 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
Tactic: simp only [Set.Ioo, Set.mem_setOf_eq, and_comm]
-- 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
⊢ 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 hesymm : HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
    ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
Tactic: have hesymm := mul_esymm_eq_sum σ R k
-- 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) *
      ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k,
        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 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)
Tactic: rw [← (sum_filter_add_sum_filter_not {a ∈ antidiagonal k | a.fst < k}
    (fun a ↦ 0 < a.fst) (fun a ↦ (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd))] at hesymm
Cleared hypotheses: hesymm
-- 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)
⊢ 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 : Eq (α := MvPolynomial σ R)
  ((fun (x : MvPolynomial σ R) ↦
      x -
        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)
    (HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k)))
  ((fun (x : MvPolynomial σ R) ↦
      x -
        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) *
      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)))
Tactic: have sub_both_sides := congrArg (· - (-1 : MvPolynomial σ R) ^ (k + 1) *
    ∑ a ∈ {a ∈ antidiagonal k | a.fst < k} with 0 < a.fst,
    (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd) hesymm
-- 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 :
  Eq (α := MvPolynomial σ R)
    ((fun (x : MvPolynomial σ R) ↦
        x -
          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)
      (HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k)))
    ((fun (x : MvPolynomial σ R) ↦
        x -
          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) *
        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)))
⊢ 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₁ : 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
Tactic: simp only [left_distrib, add_sub_cancel_left] at sub_both_sides
Cleared hypotheses: sub_both_sides
-- 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 :
  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
⊢ 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₁ : Eq (α := MvPolynomial σ R)
  ((fun (x : MvPolynomial σ R) ↦ HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * x)
    (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))
  ((fun (x : MvPolynomial σ R) ↦ HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * x)
    (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))
Tactic: have sub_both_sides := congrArg ((-1 : MvPolynomial σ R) ^ (k + 1) * ·) sub_both_sides
-- 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 :
  Eq (α := MvPolynomial σ R)
    ((fun (x : MvPolynomial σ R) ↦ HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * x)
      (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))
    ((fun (x : MvPolynomial σ R) ↦ HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * x)
      (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))
⊢ 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 =
  ∑ 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
Tactic: simp only [mul_sub_left_distrib, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k + 1, rfl⟩, one_mul,
    filter_filter (fun a : ℕ × ℕ ↦ a.fst < k) (fun a ↦ ¬0 < a.fst)]
    at sub_both_sides
Cleared hypotheses: sub_both_sides