awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Monoid S
inst_2 : DistribMulAction S R
inst_3 : IsScalarTower S R R
inst_4 : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
simp_rw :
  Eq (α := R) (sum (map (fun (x : Multiset R) ↦ prod (map (fun (x : R) ↦ s • x) x)) (powersetCard n m)))
    (esymm (map (fun (x : R) ↦ s • x) m) n)
simp_rw₁ :
  Eq (α := R) (sum (map (fun (x : Multiset R) ↦ prod (map (fun (x : R) ↦ s • x) x)) (powersetCard n m)))
    (sum (map prod (powersetCard n (map (fun (x : R) ↦ s • x) m))))
simp_rw₂ :
  Eq (α := R) (sum (map (fun (x : Multiset R) ↦ prod (map (fun (x : R) ↦ s • x) x)) (powersetCard n m)))
    (sum (map (fun (x : Multiset R) ↦ x.prod) (map (map fun (x : R) ↦ s • x) (powersetCard n m))))
simp_rw₃ :
  Eq (α := R) (sum (map (fun (x : Multiset R) ↦ prod (map (fun (x : R) ↦ s • x) x)) (powersetCard n m)))
    (sum (map ((fun (x : Multiset R) ↦ x.prod) ∘ map fun (x : R) ↦ s • x) (powersetCard n m)))
⊢ Eq (α := R) (sum (map (fun (x : Multiset R) ↦ s ^ x.card • x.prod) (powersetCard n m)))
    (esymm (map (fun (x : R) ↦ s • x) m) n)

Tactic:
simp_rw [smul_prod, esymm, powersetCard_map, map_map, Function.comp_def]

Premises used: Function.comp_def, Multiset.powersetCard_map, Multiset.map_map, Multiset.esymm, Multiset.smul_prod
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
⊢ (x ::ₘ {y}).esymm 1 = x + y

Tactic:
simp [esymm, powersetCard_one, add_comm]

Premises used: Multiset.powersetCard_one, add_comm, Multiset.esymm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
⊢ (x ::ₘ {y}).esymm 2 = x * y

Tactic:
simp [esymm, powersetCard_one]

Premises used: Multiset.powersetCard_one, Multiset.esymm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
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
rw₂ rw₃ : a * b = a * b
⊢ (rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) (a * b) = a * b

Tactic:
rw [map_mul, ha, hb]

Premises used: map_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
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
rw₂ rw₃ : a + b = a + b
⊢ (rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) (a + b) = a + b

Tactic:
rw [map_add, ha, hb]

Premises used: map_add
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
p : MvPolynomial σ R
⊢ Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) p ↔ p.IsSymmetric

Tactic:
Iff.rfl

Premises used: MvPolynomial.IsSymmetric, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
r : R
⊢ IsSymmetric.{u_1, u_3} (σ := σ) (R := R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r)

Tactic:
(symmetricSubalgebra σ R).algebraMap_mem r

Premises used: MvPolynomial.IsSymmetric, Set.Mem, setOf, MvPolynomial.symmetricSubalgebra, Subalgebra.algebraMap_mem
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ IsSymmetric.{u_1, u_3} (σ := σ) (R := R) 0

Tactic:
(symmetricSubalgebra σ R).zero_mem

Premises used: MvPolynomial.IsSymmetric, Set.Mem, Subalgebra.zero_mem, setOf, MvPolynomial.symmetricSubalgebra
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ IsSymmetric.{u_1, u_3} (σ := σ) (R := R) 1

Tactic:
(symmetricSubalgebra σ R).one_mem

Premises used: MvPolynomial.IsSymmetric, Set.Mem, setOf, MvPolynomial.symmetricSubalgebra, Subalgebra.one_mem
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ ψ : MvPolynomial σ R
hφ : φ.IsSymmetric
hψ : ψ.IsSymmetric
⊢ (φ + ψ).IsSymmetric

Tactic:
(symmetricSubalgebra σ R).add_mem hφ hψ

Premises used: MvPolynomial.IsSymmetric, Set.Mem, Subalgebra.add_mem, setOf, MvPolynomial.symmetricSubalgebra
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ ψ : MvPolynomial σ R
hφ : φ.IsSymmetric
hψ : ψ.IsSymmetric
⊢ (φ * ψ).IsSymmetric

Tactic:
(symmetricSubalgebra σ R).mul_mem hφ hψ

Premises used: MvPolynomial.IsSymmetric, Subalgebra.mul_mem, Set.Mem, setOf, MvPolynomial.symmetricSubalgebra
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
r : R
hφ : φ.IsSymmetric
⊢ (r • φ).IsSymmetric

Tactic:
(symmetricSubalgebra σ R).smul_mem hφ r

Premises used: MvPolynomial.IsSymmetric, Set.Mem, setOf, Subalgebra.smul_mem, MvPolynomial.symmetricSubalgebra
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
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)
rw₁ rw₂ :
  Eq (α := MvPolynomial σ S) ((MvPolynomial.map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ : 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)

Tactic:
rw [← map_rename, hφ]

Premises used: MvPolynomial.map_rename
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
hφ : φ.IsSymmetric
e : σ ≃ τ
x : Perm τ
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)
⊢ 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)

Tactic:
apply rename_injective _ e.symm.injective

Premises used: MvPolynomial.rename_injective, Equiv.injective, Equiv.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
hφ : φ.IsSymmetric
e : σ ≃ τ
x : Perm τ
a : (rename (⇑((e.trans x).trans e.symm) : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ
⊢ 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:
simp_rw [rename_rename, ← Equiv.coe_trans, Equiv.self_trans_symm, Equiv.coe_refl, rename_id_apply]

Premises used: MvPolynomial.rename_rename, MvPolynomial.rename_id_apply, Equiv.coe_refl, Equiv.self_trans_symm, Equiv.coe_trans
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
hφ : φ.IsSymmetric
e : σ ≃ τ
x : Perm τ
a a₁ : φ = φ
⊢ (rename (⇑((e.trans x).trans e.symm) : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) φ = φ

Tactic:
rw [hφ]
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
e : σ ≃ τ
h : IsSymmetric.{u_2, u_3} (σ := τ) (R := R) ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)
⊢ φ.IsSymmetric

Tactic:
simpa using (IsSymmetric.rename (R := R) h e.symm)

Premises used: MvPolynomial.IsSymmetric.rename, Equiv.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
φ : MvPolynomial σ R
hφ : φ.IsSymmetric
⊢ (-φ).IsSymmetric

Tactic:
(symmetricSubalgebra σ R).neg_mem hφ

Premises used: MvPolynomial.IsSymmetric, Set.Mem, setOf, Subalgebra.neg_mem, MvPolynomial.symmetricSubalgebra
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
φ ψ : MvPolynomial σ R
hφ : φ.IsSymmetric
hψ : ψ.IsSymmetric
⊢ (φ - ψ).IsSymmetric

Tactic:
(symmetricSubalgebra σ R).sub_mem hφ hψ

Premises used: MvPolynomial.IsSymmetric, Set.Mem, setOf, Subalgebra.sub_mem, MvPolynomial.symmetricSubalgebra
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
e : σ ≃ τ
p : ↥(symmetricSubalgebra τ R)
⊢ Eq (α := MvPolynomial τ R)
    (↑((AlgHom.comp (B := ↥(symmetricSubalgebra σ R))
              (AlgHom.codRestrict (AlgHom.comp (rename (⇑e : (a : σ) → τ)) (Subalgebra.val (symmetricSubalgebra σ R)))
                (symmetricSubalgebra τ R) ⋯)
              (AlgHom.codRestrict
                (AlgHom.comp (rename (⇑e.symm : (a : τ) → σ)) (Subalgebra.val (symmetricSubalgebra τ R)))
                (symmetricSubalgebra σ R) ⋯) :
            (a : ↥(symmetricSubalgebra τ R)) → ↥(symmetricSubalgebra τ R))
          p) :
      MvPolynomial τ R)
    (↑((AlgHom.id R ↥(symmetricSubalgebra τ R) : (a : ↥(symmetricSubalgebra τ R)) → ↥(symmetricSubalgebra τ R)) p) :
      MvPolynomial τ R)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
e : σ ≃ τ
p : ↥(symmetricSubalgebra σ R)
⊢ Eq (α := MvPolynomial σ R)
    (↑((AlgHom.comp (B := ↥(symmetricSubalgebra τ R))
              (AlgHom.codRestrict
                (AlgHom.comp (rename (⇑e.symm : (a : τ) → σ)) (Subalgebra.val (symmetricSubalgebra τ R)))
                (symmetricSubalgebra σ R) ⋯)
              (AlgHom.codRestrict (AlgHom.comp (rename (⇑e : (a : σ) → τ)) (Subalgebra.val (symmetricSubalgebra σ R)))
                (symmetricSubalgebra τ R) ⋯) :
            (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra σ R))
          p) :
      MvPolynomial σ R)
    (↑((AlgHom.id R ↥(symmetricSubalgebra σ R) : (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra σ R)) p) :
      MvPolynomial σ R)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
⊢ Eq (α := (n : ℕ) → MvPolynomial σ R) (esymm σ R) (Multiset.esymm (Multiset.map X (val univ)))

Tactic:
funext fun n => (esymm_map_val X _ n).symm

Premises used: Finset.univ, MvPolynomial.X, funext, Finset.esymm_map_val, Eq.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
⊢ Eq (α := (n : ℕ) → MvPolynomial σ R) (esymm σ R) (Multiset.esymm (Multiset.map X (val univ)))

Tactic:
exact funext fun n => (esymm_map_val X _ n).symm

Premises used: MvPolynomial.X, funext, Finset.esymm_map_val, Eq.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
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
simp_rw₃ : ∑ x ∈ powersetCard n univ, ∏ x ∈ x, f x = (Multiset.map f (val univ)).esymm n
⊢ (aeval f : (a : MvPolynomial σ R) → S) (esymm σ R n) = (Multiset.map f (val univ)).esymm n

Tactic:
simp_rw [esymm, aeval_sum, aeval_prod, aeval_X, esymm_map_val]

Premises used: MvPolynomial.aeval_sum, MvPolynomial.aeval_X, MvPolynomial.esymm, Finset.esymm_map_val, MvPolynomial.aeval_prod
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
n : ℕ
⊢ Eq (α := MvPolynomial σ R) (esymm σ R n) (∑ t : { s : Finset σ // #s = n }, ∏ i ∈ (↑t : Finset σ), X i)

Tactic:
sum_subtype _ (fun _ => mem_powersetCard_univ) _

Premises used: Finset.sum_subtype, MvPolynomial.esymm, Finset.mem_powersetCard_univ
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
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)
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)
⊢ Eq (α := MvPolynomial σ R) (esymm σ R n)
    (∑ t ∈ powersetCard n univ, (monomial (∑ i ∈ t, Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)

Tactic:
simp_rw [monomial_sum_one, esymm, ← X_pow_eq_monomial, pow_one]

Premises used: MvPolynomial.X_pow_eq_monomial, MvPolynomial.esymm, pow_one, MvPolynomial.monomial_sum_one
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
⊢ Eq (α := MvPolynomial σ R) (esymm σ R 0) 1

Tactic:
simp only [esymm, powersetCard_zero, sum_singleton, prod_empty]

Premises used: Finset.prod_empty, MvPolynomial.esymm, Finset.sum_singleton, Finset.powersetCard_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
⊢ Eq (α := MvPolynomial σ R) (esymm σ R 1) (∑ i : σ, X i)

Tactic:
simp [esymm, powersetCard_one]

Premises used: MvPolynomial.esymm, Finset.powersetCard_one
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
⊢ Eq (α := MvPolynomial σ R) (esymmPart σ R (n := 0) (Nat.Partition.indiscrete 0)) 1

Tactic:
simp [esymmPart]

Premises used: MvPolynomial.esymmPart
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
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)
succ :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial σ R) (esymmPart σ R (n := n + 1) (Nat.Partition.indiscrete (n + 1))) (esymm σ R (n + 1))
⊢ Eq (α := MvPolynomial σ R) (esymmPart σ R (Nat.Partition.indiscrete n)) (esymm σ R n)

Tactic:
cases n
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
⊢ Eq (α := MvPolynomial σ R) (esymmPart σ R (n := 0) (Nat.Partition.indiscrete 0)) (esymm σ R 0)

Tactic:
simp [esymmPart]

Premises used: MvPolynomial.esymmPart
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
n : ℕ
⊢ Eq (α := MvPolynomial σ R) (esymmPart σ R (n := n + 1) (Nat.Partition.indiscrete (n + 1))) (esymm σ R (n + 1))

Tactic:
simp [esymmPart]

Premises used: MvPolynomial.esymmPart
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
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)
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)
⊢ Eq (α := MvPolynomial σ S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) (esymm σ R n) : MvPolynomial σ S)
    (esymm σ S n : MvPolynomial σ S)

Tactic:
simp_rw [esymm, map_sum, map_prod, map_X]

Premises used: MvPolynomial.esymm, map_sum, map_prod, MvPolynomial.map_X
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
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))
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))
⊢ 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)

Tactic:
simp_rw [esymm, map_sum, map_prod, rename_X]

Premises used: MvPolynomial.esymm, map_sum, map_prod, MvPolynomial.rename_X
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
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) (∑ x ∈ powersetCard n univ, ∏ i ∈ x, X ((e : (a : σ) → τ) i))
    (∑ t ∈ powersetCard n (Finset.map e.toEmbedding univ), ∏ i ∈ t, X i)

Tactic:
simp [powersetCard_map, -map_univ_equiv, (mapEmbedding_apply)]

Premises used: Finset.map_univ_equiv, Finset.powersetCard_map, Finset.mapEmbedding_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
n : ℕ
e : σ ≃ τ
rw rw₁ : Eq (α := MvPolynomial τ R) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i) (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i)
⊢ Eq (α := MvPolynomial τ R) (∑ t ∈ powersetCard n (Finset.map e.toEmbedding univ), ∏ i ∈ t, X i)
    (∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i)

Tactic:
rw [map_univ_equiv]

Premises used: Finset.map_univ_equiv
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
n : ℕ
e : Perm σ
rw rw₁ : Eq (α := MvPolynomial σ R) (esymm σ R n) (esymm σ R n)
⊢ Eq (α := MvPolynomial σ R)
    ((rename (⇑e : (a : σ) → σ) : (a : MvPolynomial σ R) → MvPolynomial σ R) (esymm σ R n) : MvPolynomial σ R)
    (esymm σ R n : MvPolynomial σ R)

Tactic:
rw [rename_esymm]

Premises used: MvPolynomial.rename_esymm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
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))
⊢ 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)

Tactic:
rw [esymm_eq_sum_monomial]

Premises used: MvPolynomial.esymm_eq_sum_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
inst_3 : Nontrivial R
n : ℕ
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))
⊢ 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:
simp only [← single_eq_monomial]

Premises used: MvPolynomial.single_eq_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
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))

Tactic:
Finsupp.support_sum_eq_biUnion (powersetCard n (univ : Finset σ)) ?_

Premises used: Finset.univ, MvPolynomial.support, Finset.powersetCard, AddMonoidAlgebra, Finsupp.support_sum_eq_biUnion