rw [comp_apply,
    Equiv.swap_apply_of_ne_of_ne (ne_of_mem_erase hk)
                                 (ne_of_mem_erase (mem_of_mem_erase hk))]
case haij
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
k : Fin (Nat.succ n)
hk : k ∈ erase (erase univ j) i
⊢ Weight.comp a (Equiv.swap i j) k = a k
no goals