-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem rename_msymm (μ : n.Partition) (e : σ ≃ τ) :
    rename e (msymm σ R μ) = msymm τ R μ

Proof state:
case h
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
x✝ : { x // Nat.Partition.ofSym x = μ }
⊢ (rename ⇑e) (Multiset.map X ↑↑x✝).prod = (Multiset.map X ↑↑((μ.ofSymShapeEquiv e) x✝)).prod

Tactic:
rw [← Multiset.prod_hom, Multiset.map_map, Nat.Partition.ofSymShapeEquiv]

Result:
case h
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
x✝ : { x // Nat.Partition.ofSym x = μ }
⊢ (Multiset.map (⇑(rename ⇑e) ∘ X) ↑↑x✝).prod =
    (Multiset.map X
        ↑↑({ toFun := fun x => ⟨(Sym.equivCongr e) ↑x, ⋯⟩, invFun := fun x => ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩,
                left_inv := ⋯, right_inv := ⋯ }
              x✝)).prod

Proof state:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
⊢ (rename ⇑e) (msymm σ R μ) = msymm τ R μ

Tactic:
rw [msymm, map_sum]

Result:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
⊢ ∑ x : { a // Nat.Partition.ofSym a = μ }, (rename ⇑e) (Multiset.map X ↑↑x).prod = msymm τ R μ

Proof state:
case h
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
⊢ ∀ (x : { x // Nat.Partition.ofSym x = μ }),
    (rename ⇑e) (Multiset.map X ↑↑x).prod = (Multiset.map X ↑↑((μ.ofSymShapeEquiv e) x)).prod

Tactic:
intro

Result:
case h
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
x✝ : { x // Nat.Partition.ofSym x = μ }
⊢ (rename ⇑e) (Multiset.map X ↑↑x✝).prod = (Multiset.map X ↑↑((μ.ofSymShapeEquiv e) x✝)).prod

Proof state:
case h
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
x✝ : { x // Nat.Partition.ofSym x = μ }
⊢ (Multiset.map (⇑(rename ⇑e) ∘ X) ↑↑x✝).prod =
    (Multiset.map X
        ↑↑({ toFun := fun x => ⟨(Sym.equivCongr e) ↑x, ⋯⟩, invFun := fun x => ⟨(Sym.equivCongr e.symm) ↑x, ⋯⟩,
                left_inv := ⋯, right_inv := ⋯ }
              x✝)).prod

Tactic:
simp

Result:
no goals

Proof state:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
⊢ ∑ x : { a // Nat.Partition.ofSym a = μ }, (rename ⇑e) (Multiset.map X ↑↑x).prod = msymm τ R μ

Tactic:
apply Fintype.sum_equiv (Nat.Partition.ofSymShapeEquiv μ e)

Result:
case h
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
⊢ ∀ (x : { x // Nat.Partition.ofSym x = μ }),
    (rename ⇑e) (Multiset.map X ↑↑x).prod = (Multiset.map X ↑↑((μ.ofSymShapeEquiv e) x)).prod