exact hJI.subset
α : Type u_1
ι : Type u_2
M : Matroid α
F I J✝ X Y B C R : Set α
e✝ f✝ x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.Basis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.Basis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.Basis (insert f (J \ {e})) (insert e I)
⊢ J ⊆ insert e I
no goals