awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ_1 : Type u_1
τ : Type u_2
R_1 : Type u_3
S : Type u_4
σ : Type u_5
R : Type u_6
inst : CommSemiring R
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) (setOf IsSymmetric) a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) (setOf IsSymmetric) b
e : Perm σ
rw :
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) b : MvPolynomial σ R) =
    a * b
⊢ (rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) (a * b) = a * b
have rw₁ : HMul.hMul (β := MvPolynomial σ R) a
    ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) b : MvPolynomial σ R) =
  a * b
Tactic: rw [map_mul, ha, hb]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ_1 : Type u_1
τ : Type u_2
R_1 : Type u_3
S : Type u_4
σ : Type u_5
R : Type u_6
inst : CommSemiring R
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) (setOf IsSymmetric) a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) (setOf IsSymmetric) b
e : Perm σ
rw :
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) b : MvPolynomial σ R) =
    a * b
rw₁ :
  HMul.hMul (β := MvPolynomial σ R) a
      ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) b : MvPolynomial σ R) =
    a * b
⊢ (rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) (a * b) = a * b
have rw₂ : a * b = a * b
Tactic: rw [map_mul, ha, hb]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ_1 : Type u_1
τ : Type u_2
R_1 : Type u_3
S : Type u_4
σ : Type u_5
R : Type u_6
inst : CommSemiring R
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) (setOf IsSymmetric) a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) (setOf IsSymmetric) b
e : Perm σ
⊢ (rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) (a + b) = a + b
have rw : HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) b : MvPolynomial σ R) =
  a + b
Tactic: rw [map_add, ha, hb]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ_1 : Type u_1
τ : Type u_2
R_1 : Type u_3
S : Type u_4
σ : Type u_5
R : Type u_6
inst : CommSemiring R
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) (setOf IsSymmetric) a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) (setOf IsSymmetric) b
e : Perm σ
rw :
  HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) b : MvPolynomial σ R) =
    a + b
⊢ (rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) (a + b) = a + b
have rw₁ : HAdd.hAdd (β := MvPolynomial σ R) a
    ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) b : MvPolynomial σ R) =
  a + b
Tactic: rw [map_add, ha, hb]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ_1 : Type u_1
τ : Type u_2
R_1 : Type u_3
S : Type u_4
σ : Type u_5
R : Type u_6
inst : CommSemiring R
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) (setOf IsSymmetric) a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) (setOf IsSymmetric) b
e : Perm σ
rw :
  HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) b : MvPolynomial σ R) =
    a + b
rw₁ :
  HAdd.hAdd (β := MvPolynomial σ R) a
      ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) b : MvPolynomial σ R) =
    a + b
⊢ (rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) (a + b) = a + b
have rw₂ : a + b = a + b
Tactic: rw [map_add, ha, hb]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
hφ : φ.IsSymmetric
f : R →+* S
e : Perm σ
⊢ Eq (α := MvPolynomial σ S)
    ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ) :
      MvPolynomial σ S)
    ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ : MvPolynomial σ S)
have rw : Eq (α := MvPolynomial σ S)
  ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S)
      ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) :
    MvPolynomial σ S)
  ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ : MvPolynomial σ S)
Tactic: rw [← map_rename, hφ]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
hφ : φ.IsSymmetric
f : R →+* S
e : Perm σ
rw :
  Eq (α := MvPolynomial σ S)
    ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ) :
      MvPolynomial σ S)
    ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ : MvPolynomial σ S)
⊢ Eq (α := MvPolynomial σ S)
    ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ S) → MvPolynomial σ S)
        ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ) :
      MvPolynomial σ S)
    ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ : MvPolynomial σ S)
have rw₁ : Eq (α := MvPolynomial σ S) ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ : MvPolynomial σ S)
  ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ : MvPolynomial σ S)
Tactic: rw [← map_rename, hφ]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
hφ : φ.IsSymmetric
e : σ ≃ τ
x : Perm τ
⊢ Eq (α := MvPolynomial τ R)
    ((rename (⇑x : (a : τ) → τ) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) :
      MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) φ : MvPolynomial τ R)
have a : Eq (α := MvPolynomial σ R)
  ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R)
      ((rename (⇑x : (a : τ) → τ) : (a : MvPolynomial τ R) → MvPolynomial τ R)
        ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) :
    MvPolynomial σ R)
  ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R)
      ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) :
    MvPolynomial σ R)
Tactic: apply rename_injective _ e.symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
hφ : φ.IsSymmetric
e : σ ≃ τ
x : Perm τ
⊢ Eq (α := MvPolynomial σ R)
    ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((rename (⇑x : (a : τ) → τ) : (a : MvPolynomial τ R) → MvPolynomial τ R)
          ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) :
      MvPolynomial σ R)
    ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) :
      MvPolynomial σ R)
have a : (rename (⇑((e.trans x).trans e.symm) : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
Tactic: simp_rw [rename_rename, ← Equiv.coe_trans, Equiv.self_trans_symm, Equiv.coe_refl, rename_id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
hφ : φ.IsSymmetric
e : σ ≃ τ
x : Perm τ
⊢ (rename (⇑((e.trans x).trans e.symm) : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
have a : φ = φ
Tactic: rw [hφ]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
S : Type u_4
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Fintype σ
inst_3 : Algebra R S
n : ℕ
f : σ → S
⊢ (aeval f : (a : MvPolynomial σ R) → S) (esymm σ R n) = (Multiset.map f (val univ)).esymm n
have simp_rw : (aeval f : (a : MvPolynomial σ R) → S) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i) = (Multiset.map f (val univ)).esymm n
Tactic: simp_rw [esymm, aeval_sum, aeval_prod, aeval_X, esymm_map_val]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
S : Type u_4
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Fintype σ
inst_3 : Algebra R S
n : ℕ
f : σ → S
simp_rw :
  (aeval f : (a : MvPolynomial σ R) → S) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i) = (Multiset.map f (val univ)).esymm n
⊢ (aeval f : (a : MvPolynomial σ R) → S) (esymm σ R n) = (Multiset.map f (val univ)).esymm n
have simp_rw₁ : ∑ i ∈ powersetCard n univ, (aeval f : (a : MvPolynomial σ R) → S) (∏ i ∈ i, X i) = (Multiset.map f (val univ)).esymm n
Tactic: simp_rw [esymm, aeval_sum, aeval_prod, aeval_X, esymm_map_val]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
S : Type u_4
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Fintype σ
inst_3 : Algebra R S
n : ℕ
f : σ → S
simp_rw :
  (aeval f : (a : MvPolynomial σ R) → S) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i) = (Multiset.map f (val univ)).esymm n
simp_rw₁ :
  ∑ i ∈ powersetCard n univ, (aeval f : (a : MvPolynomial σ R) → S) (∏ i ∈ i, X i) = (Multiset.map f (val univ)).esymm n
⊢ (aeval f : (a : MvPolynomial σ R) → S) (esymm σ R n) = (Multiset.map f (val univ)).esymm n
have simp_rw₂ : ∑ x ∈ powersetCard n univ, ∏ i ∈ x, (aeval f : (a : MvPolynomial σ R) → S) (X i) = (Multiset.map f (val univ)).esymm n
Tactic: simp_rw [esymm, aeval_sum, aeval_prod, aeval_X, esymm_map_val]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
S : Type u_4
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Fintype σ
inst_3 : Algebra R S
n : ℕ
f : σ → S
simp_rw :
  (aeval f : (a : MvPolynomial σ R) → S) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i) = (Multiset.map f (val univ)).esymm n
simp_rw₁ :
  ∑ i ∈ powersetCard n univ, (aeval f : (a : MvPolynomial σ R) → S) (∏ i ∈ i, X i) = (Multiset.map f (val univ)).esymm n
simp_rw₂ :
  ∑ x ∈ powersetCard n univ, ∏ i ∈ x, (aeval f : (a : MvPolynomial σ R) → S) (X i) = (Multiset.map f (val univ)).esymm n
⊢ (aeval f : (a : MvPolynomial σ R) → S) (esymm σ R n) = (Multiset.map f (val univ)).esymm n
have simp_rw₃ : ∑ x ∈ powersetCard n univ, ∏ x ∈ x, f x = (Multiset.map f (val univ)).esymm n
Tactic: simp_rw [esymm, aeval_sum, aeval_prod, aeval_X, esymm_map_val]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
n : ℕ
⊢ Eq (α := MvPolynomial σ R) (esymm σ R n)
    (∑ t ∈ powersetCard n univ, (monomial (∑ i ∈ t, Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
have simp_rw : Eq (α := MvPolynomial σ R) (esymm σ R n)
  (∑ x ∈ powersetCard n univ, ∏ i ∈ x, (monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
Tactic: simp_rw [monomial_sum_one, esymm, ← X_pow_eq_monomial, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
n : ℕ
simp_rw :
  Eq (α := MvPolynomial σ R) (esymm σ R n)
    (∑ x ∈ powersetCard n univ, ∏ i ∈ x, (monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
⊢ Eq (α := MvPolynomial σ R) (esymm σ R n)
    (∑ t ∈ powersetCard n univ, (monomial (∑ i ∈ t, Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
have simp_rw₁ : Eq (α := MvPolynomial σ R) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i)
  (∑ x ∈ powersetCard n univ, ∏ i ∈ x, (monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
Tactic: simp_rw [monomial_sum_one, esymm, ← X_pow_eq_monomial, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
n : ℕ
simp_rw :
  Eq (α := MvPolynomial σ R) (esymm σ R n)
    (∑ x ∈ powersetCard n univ, ∏ i ∈ x, (monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
simp_rw₁ :
  Eq (α := MvPolynomial σ R) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i)
    (∑ x ∈ powersetCard n univ, ∏ i ∈ x, (monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
⊢ Eq (α := MvPolynomial σ R) (esymm σ R n)
    (∑ t ∈ powersetCard n univ, (monomial (∑ i ∈ t, Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
have simp_rw₂ : Eq (α := MvPolynomial σ R) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i)
  (∑ x ∈ powersetCard n univ, ∏ x ∈ x, HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X x) 1)
Tactic: simp_rw [monomial_sum_one, esymm, ← X_pow_eq_monomial, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
n : ℕ
⊢ Eq (α := MvPolynomial σ R) (esymmPart σ R (Nat.Partition.indiscrete n)) (esymm σ R n)
have zero : Eq (α := MvPolynomial σ R) (esymmPart σ R (n := 0) (Nat.Partition.indiscrete 0)) (esymm σ R 0)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
n : ℕ
zero : Eq (α := MvPolynomial σ R) (esymmPart σ R (n := 0) (Nat.Partition.indiscrete 0)) (esymm σ R 0)
⊢ Eq (α := MvPolynomial σ R) (esymmPart σ R (Nat.Partition.indiscrete n)) (esymm σ R n)
have succ : ∀ (n : ℕ),
  Eq (α := MvPolynomial σ R) (esymmPart σ R (n := n + 1) (Nat.Partition.indiscrete (n + 1))) (esymm σ R (n + 1))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
S : Type u_4
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Fintype σ
n : ℕ
f : R →+* S
⊢ Eq (α := MvPolynomial σ S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) (esymm σ R n) : MvPolynomial σ S)
    (esymm σ S n : MvPolynomial σ S)
have simp_rw : Eq (α := MvPolynomial σ S)
  ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i))
  (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i)
Tactic: simp_rw [esymm, map_sum, map_prod, map_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
S : Type u_4
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Fintype σ
n : ℕ
f : R →+* S
simp_rw :
  Eq (α := MvPolynomial σ S)
    ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i))
    (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i)
⊢ Eq (α := MvPolynomial σ S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) (esymm σ R n) : MvPolynomial σ S)
    (esymm σ S n : MvPolynomial σ S)
have simp_rw₁ : Eq (α := MvPolynomial σ S)
  (∑ x ∈ powersetCard n univ, (map f : (a : MvPolynomial σ R) → MvPolynomial σ S) (∏ i ∈ x, X i))
  (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i)
Tactic: simp_rw [esymm, map_sum, map_prod, map_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
S : Type u_4
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Fintype σ
n : ℕ
f : R →+* S
simp_rw :
  Eq (α := MvPolynomial σ S)
    ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i))
    (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i)
simp_rw₁ :
  Eq (α := MvPolynomial σ S)
    (∑ x ∈ powersetCard n univ, (map f : (a : MvPolynomial σ R) → MvPolynomial σ S) (∏ i ∈ x, X i))
    (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i)
⊢ Eq (α := MvPolynomial σ S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) (esymm σ R n) : MvPolynomial σ S)
    (esymm σ S n : MvPolynomial σ S)
have simp_rw₂ : Eq (α := MvPolynomial σ S)
  (∑ x ∈ powersetCard n univ, ∏ x ∈ x, (map f : (a : MvPolynomial σ R) → MvPolynomial σ S) (X x))
  (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i)
Tactic: simp_rw [esymm, map_sum, map_prod, map_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (esymm σ R n) : MvPolynomial τ R)
    (∑ x ∈ powersetCard n univ, ∏ i ∈ x, X ((e : (a : σ) → τ) i) : MvPolynomial τ R)
have simp_rw : Eq (α := MvPolynomial τ R)
  ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i))
  (∑ x ∈ powersetCard n univ, ∏ i ∈ x, X ((e : (a : σ) → τ) i))
Tactic: simp_rw [esymm, map_sum, map_prod, rename_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
n : ℕ
e : σ ≃ τ
simp_rw :
  Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i))
    (∑ x ∈ powersetCard n univ, ∏ i ∈ x, X ((e : (a : σ) → τ) i))
⊢ Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (esymm σ R n) : MvPolynomial τ R)
    (∑ x ∈ powersetCard n univ, ∏ i ∈ x, X ((e : (a : σ) → τ) i) : MvPolynomial τ R)
have simp_rw₁ : Eq (α := MvPolynomial τ R)
  (∑ x ∈ powersetCard n univ, (rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (∏ i ∈ x, X i))
  (∑ x ∈ powersetCard n univ, ∏ i ∈ x, X ((e : (a : σ) → τ) i))
Tactic: simp_rw [esymm, map_sum, map_prod, rename_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
n : ℕ
e : σ ≃ τ
simp_rw :
  Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i))
    (∑ x ∈ powersetCard n univ, ∏ i ∈ x, X ((e : (a : σ) → τ) i))
simp_rw₁ :
  Eq (α := MvPolynomial τ R)
    (∑ x ∈ powersetCard n univ, (rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (∏ i ∈ x, X i))
    (∑ x ∈ powersetCard n univ, ∏ i ∈ x, X ((e : (a : σ) → τ) i))
⊢ Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (esymm σ R n) : MvPolynomial τ R)
    (∑ x ∈ powersetCard n univ, ∏ i ∈ x, X ((e : (a : σ) → τ) i) : MvPolynomial τ R)
have simp_rw₂ : Eq (α := MvPolynomial τ R)
  (∑ x ∈ powersetCard n univ, ∏ x ∈ x, (rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X x))
  (∑ x ∈ powersetCard n univ, ∏ i ∈ x, X ((e : (a : σ) → τ) i))
Tactic: simp_rw [esymm, map_sum, map_prod, rename_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ Eq (α := MvPolynomial τ R) (∑ t ∈ powersetCard n (Finset.map e.toEmbedding univ), ∏ i ∈ t, X i)
    (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i)
have rw : Eq (α := MvPolynomial τ R) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i)
Tactic: rw [map_univ_equiv]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
n : ℕ
e : Perm σ
⊢ Eq (α := MvPolynomial σ R)
    ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) (esymm σ R n) : MvPolynomial σ R)
    (esymm σ R n : MvPolynomial σ R)
have rw : Eq (α := MvPolynomial σ R) (esymm σ R n) (esymm σ R n)
Tactic: rw [rename_esymm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
⊢ support (esymm σ R n) =
    Finset.biUnion (powersetCard n univ) fun (t : Finset σ) ↦
      Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1)
have rw : Eq.{u_5 + 1} (α := Finset (σ →₀ ℕ))
  (support.{u_6, u_5} (R := R)
    (∑ t ∈ powersetCard n univ, (monomial (∑ i ∈ t, Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))
  (Finset.biUnion (powersetCard n univ) fun (t : Finset σ) ↦
    Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1))
Tactic: rw [esymm_eq_sum_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
⊢ Eq.{u_5 + 1} (α := Finset (σ →₀ ℕ))
    (support.{u_6, u_5} (R := R)
      (∑ t ∈ powersetCard n univ, (monomial (∑ i ∈ t, Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))
    (Finset.biUnion (powersetCard n univ) fun (t : Finset σ) ↦
      Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1))
have simp : Eq.{u_5 + 1} (α := Finset (σ →₀ ℕ))
  (support.{u_6, u_5} (R := R) (∑ x ∈ powersetCard n univ, Finsupp.single (∑ i ∈ x, Finsupp.single i 1) 1))
  (Finset.biUnion (powersetCard n univ) fun (t : Finset σ) ↦
    Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1))
Tactic: simp only [← single_eq_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
⊢ Eq.{u_5 + 1} (α := Finset (σ →₀ ℕ))
    (support.{u_6, u_5} (R := R) (∑ x ∈ powersetCard n univ, Finsupp.single (∑ i ∈ x, Finsupp.single i 1) 1))
    (Finset.biUnion (powersetCard n univ) fun (t : Finset σ) ↦
      Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1))
have refine : ∀ (i₁ i₂ : Finset σ),
  i₁ ≠ i₂ →
    Disjoint (α := Finset (σ →₀ ℕ))
      (Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ i₁, Finsupp.single i 1) 1))
      (Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ i₂, Finsupp.single i 1) 1))
Tactic: refine Finsupp.support_sum_eq_biUnion (powersetCard n (univ : Finset σ)) ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
s t : Finset σ
hst : s ≠ t
⊢ Disjoint (α := Finset (σ →₀ ℕ)) (Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ s, Finsupp.single i 1) 1))
    (Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1))
have rw : ∀ ⦃a : σ →₀ ℕ⦄,
  Membership.mem (γ := Finset (σ →₀ ℕ)) {∑ i ∈ s, Finsupp.single i 1} a →
    a ∉ Finsupp.support.{u_5, u_6} (M := R) (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1)
Tactic: rw [disjoint_left, Finsupp.support_single _ one_ne_zero]