rw [← add_sum_erase _ _ (mem_univ i), ← add_sum_erase _ _ (mem_univ j),
    ← add_sum_erase _ _ (mem_erase.mpr ⟨h.symm, mem_univ _⟩),
    ← add_sum_erase _ _ (mem_erase.mpr ⟨h, mem_univ _⟩),
    erase_right_comm, sum_congr rfl @ht, ← add_assoc, ← add_assoc]
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
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
⊢ Weight.comp a (Equiv.swap i j) i * w i + Weight.comp a (Equiv.swap i j) j * w j +
      ∑ x in erase (erase univ j) i, a x * w x ≤
    a j * w j + a i * w i + ∑ x in erase (erase univ j) i, a x * w x