simp only [pair_swap_eq g' a, hgg']
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
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
ham' : a' i ≤ a' j
⊢ pair g' a' = pair g a
no goals