Theorem: Weight.E_perm (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ E (Weight.comp w σ) = E w
Tactic:
simp only [E, sum_perm]
State after:
no goals