rw [add_le_add_iff_left]
case inl
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)
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 i ≤ a j
hwg : E w ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w (Weight.comp a (Equiv.swap i j))
⊢ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w (Weight.comp a (Equiv.swap i j)) ≤
    E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w a
case inl
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)
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 i ≤ a j
hwg : E w ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w (Weight.comp a (Equiv.swap i j))
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a