exact fun j j_mem ↦ ⟨(J_sub_X j_mem).1, M_ind.subset_ground j_mem⟩
case ex_basis.inl
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
e : α
X : Set α
C : M.ModularCut
he : e ∉ M.E
heX : e ∉ X
I : Set α
hX : M.cl I ∉ C
hI : M.Indep I ∧ I ⊆ X ∩ M.E ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X ∩ M.E → I = J
sub_inter : I ⊆ X ∧ I ⊆ M.E
J : Set α
J_ind : (C.extension e).Indep J
I_sub_J : I ⊆ J
J_sub_X : J ⊆ X ∩ insert e M.E
M_ind : M.Indep J
⊢ J ⊆ X ∩ M.E
no goals