simp only [mem_iUnion, exists_prop] at hi' hj'
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 : ι
hi' : e ∈ (fun i => ⋃ (_ : i ∈ A), Xs i) i
j : ι
hj' : e ∈ (fun i => ⋃ (_ : i ∈ Aᶜ), Xs i) j
⊢ e ∈ M.cl ∅
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 ∅