exact h.loop_of_mem_inter (show i ≠ j from fun hij ↦ hj'.1 <| hij ▸ hi'.1) ⟨hi'.2, hj'.2⟩
case intro.intro.intro.intro.refl.intro.intro.intro.refl
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i✝ j✝ : ι
e✝ f : α
h : M.SkewFamily Xs
A : Set ι
e : α
i j : ι
hi' : i ∈ A ∧ e ∈ Xs i
hj' : j ∈ Aᶜ ∧ e ∈ Xs j
⊢ e ∈ M.cl ∅
no goals