exact ⟨hss hfi, fun (h : f = e) ↦ heJ <| h ▸ hf⟩
case intro.inl.a
ι : 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
Ks : ι → Set α
hdj : Pairwise (Disjoint on Ks)
hKs : M.Basis (⋃ i, Ks i) (⋃ i, Xs i)
huKs : ∀ (i : ι), M.Basis (Ks i) (Xs i)
hssE : Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i ⊆ M.E
K' : Set α
hK' : M.Basis K' (Js i₀ ∪ ⋃ i ∈ {i₀}ᶜ, Ks i)
hss : Js i₀ ⊆ K'
hK'' : ∀ (i : ι), i ≠ i₀ → Ks i ⊆ K'
f : α
hf : f ∈ J
hfi : f ∈ Js i₀
⊢ f ∈ K' \ {e}
no goals