no goals
σ : Type u_1
R : Type u_3
τ : Type u_2
S : Type ?u.127979
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ↑(rename ↑e) (esymm σ R n) = ∑ x in powersetLen n univ, ∏ i in x, X (↑e i)
simp_rw [esymm, map_sum, map_prod, rename_X]
σ : Type u_1
R : Type u_3
τ : Type u_2
S : Type ?u.127979
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x in powersetLen n univ, ∏ x in x, X (↑e x) =
    ∑ x in powersetLen n univ, ∏ i in ↑(mapEmbedding (Equiv.toEmbedding e)) x, X i
σ : Type u_1
R : Type u_3
τ : Type u_2
S : Type ?u.127979
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x in powersetLen n univ, ∏ i in x, X (↑e i) =
    ∑ t in powersetLen n (Finset.map (Equiv.toEmbedding e) univ), ∏ i in t, X i
simp [Finset.powersetLen_map, -Finset.map_univ_equiv]
σ : Type u_1
R : Type u_3
τ : Type u_2
S : Type ?u.127979
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x in powersetLen n univ, ∏ x in x, X (↑e x) =
    ∑ x in powersetLen n univ, ∏ i in Finset.map (Equiv.toEmbedding e) x, X i
σ : Type u_1
R : Type u_3
τ : Type u_2
S : Type ?u.127979
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x in powersetLen n univ, ∏ x in x, X (↑e x) =
    ∑ x in powersetLen n univ, ∏ i in ↑(mapEmbedding (Equiv.toEmbedding e)) x, X i
dsimp [mapEmbedding, OrderEmbedding.ofMapLEIff]
no goals
σ : Type u_1
R : Type u_3
τ : Type u_2
S : Type ?u.127979
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x in powersetLen n univ, ∏ x in x, X (↑e x) =
    ∑ x in powersetLen n univ, ∏ i in Finset.map (Equiv.toEmbedding e) x, X i
simp
no goals
σ : Type u_1
R : Type u_3
τ : Type u_2
S : Type ?u.127979
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ t in powersetLen n (Finset.map (Equiv.toEmbedding e) univ), ∏ i in t, X i = ∑ t in powersetLen n univ, ∏ i in t, X i
rw [Finset.map_univ_equiv]