simp only [Weight.comp, Function.comp_apply, Equiv.swap_apply_self]
case hgg'.h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
i✝ : Fin (Nat.succ n)
⊢ Weight.comp g' (Equiv.swap i j) i✝ = g i✝
no goals