intro J' hJ'_indep hJ'X hJJ'
case intro.intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
⊢ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ X → J ⊆ b → b ⊆ J
case intro.intro.intro
α : Type u_1
I✝ : Set α
M : Matroid α
I X J : Set α
hX : X ⊆ M.E
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → I ⊆ b → b ⊆ X → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hIJ : I ⊆ J
hJX : J ⊆ X
J' : Set α
hJ'_indep : M.Indep J'
hJ'X : J' ⊆ X
hJJ' : J ⊆ J'
⊢ J' ⊆ J