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

State before:
n d : ℕ
inst✝ : NeZero d
a : Weight n d
ha : a ∈ testvecs n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ Weight.comp a σ ∈ testvecs n d
Tactic:
simpa only [testvecs, sum_perm, Set.mem_setOf_eq]
State after:
no goals