simp only [pair]
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
ht : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k * w k = a k * w k
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
ht : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k * w k = a k * w k
⊢ ∑ j_1 : Fin (Nat.succ n), Weight.comp a (Equiv.swap i j) j_1 * w j_1 ≤ ∑ j : Fin (Nat.succ n), a j * w j