-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
lemma pow_smul_esymm {S : Type*} [Monoid S] [DistribMulAction S R] [IsScalarTower S R R]
    [SMulCommClass S R R] (s : S) (n : ℕ) (m : Multiset R) :
    s ^ n • m.esymm n = (m.map (s • ·)).esymm n

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ s ^ n • m.esymm n = (map (fun x => s • x) m).esymm n

Tactic:
rw [esymm, smul_sum, map_map]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ (map ((fun x => s ^ n • x) ∘ prod) (powersetCard n m)).sum = (map (fun x => s • x) m).esymm n

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ (map ((fun x => s ^ n • x) ∘ prod) (powersetCard n m)).sum =
    (map (fun x => s ^ x.card • x.prod) (powersetCard n m)).sum

Tactic:
refine congr_arg _ (map_congr rfl (fun x hx ↦ ?_))

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
s : S
n : ℕ
m x : Multiset R
hx : x ∈ powersetCard n m
⊢ ((fun x => s ^ n • x) ∘ prod) x = s ^ x.card • x.prod

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ (map ((fun x => s ^ n • x) ∘ prod) (powersetCard n m)).sum = (map (fun x => s • x) m).esymm n

Tactic:
trans ((powersetCard n m).map (fun x : Multiset R ↦ s ^ card x • x.prod)).sum

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ (map ((fun x => s ^ n • x) ∘ prod) (powersetCard n m)).sum =
    (map (fun x => s ^ x.card • x.prod) (powersetCard n m)).sum

R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ (map (fun x => s ^ x.card • x.prod) (powersetCard n m)).sum = (map (fun x => s • x) m).esymm n

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
s : S
n : ℕ
m : Multiset R
⊢ (map (fun x => s ^ x.card • x.prod) (powersetCard n m)).sum = (map (fun x => s • x) m).esymm n

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

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Monoid S
inst✝² : DistribMulAction S R
inst✝¹ : IsScalarTower S R R
inst✝ : SMulCommClass S R R
s : S
n : ℕ
m x : Multiset R
hx : x ∈ powersetCard n m
⊢ ((fun x => s ^ n • x) ∘ prod) x = s ^ x.card • x.prod

Tactic:
rw [Function.comp_apply, (mem_powersetCard.1 hx).2]

Result:
no goals