refine ⟨fun h a ha ↦ ?_, fun h a ha ↦ h (a.comp σ⁻¹) (testvecs_perm ha σ⁻¹)⟩
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ (∀ a ∈ testvecs n d, E w ≤ E w' - pair w' (Weight.comp a σ⁻¹) + pair w (Weight.comp a σ⁻¹)) ↔
    ∀ a ∈ testvecs n d, E w ≤ E w' - pair w' a + pair w a
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
h : ∀ a ∈ testvecs n d, E w ≤ E w' - pair w' (Weight.comp a σ⁻¹) + pair w (Weight.comp a σ⁻¹)
a : Weight n d
ha : a ∈ testvecs n d
⊢ E w ≤ E w' - pair w' a + pair w a