obtain ⟨i₀, e, hei₀, heJ⟩ := ex_i
case intro
ι : 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
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
ex_i : ∃ i e, e ∈ Js i \ J
⊢ False
case intro.intro.intro.intro
ι : 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
hIX : ∀ (i : ι), Is i ⊆ Xs i
hIs : ∀ (i : ι), M.Indep (Is i)
Js : ι → Set α
hJs : ∀ (i : ι), M.Basis (Js i) (Xs i) ∧ Is i ⊆ Js i
J : Set α
hJ : M.Basis J (⋃ i, Js i)
hcon : ¬M.Indep (⋃ i, Js i)
i₀ : ι
e : α
hei₀ : e ∈ Js i₀
heJ : e ∉ J
⊢ False