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

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

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