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

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ Weight.sum (Weight.comp w σ) = Weight.sum w
Tactic:
simp only [Weight.sum, Function.comp_apply]
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ ∑ j : Fin (Nat.succ n), Weight.comp w σ j = ∑ j : Fin (Nat.succ n), w j

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ ∑ j : Fin (Nat.succ n), Weight.comp w σ j = ∑ j : Fin (Nat.succ n), w j
Tactic:
exact Fintype.sum_bijective σ (Equiv.bijective σ) _ _ (fun i ↦ rfl)
State after:
no goals