refine ⟨⟨⟨hJ_indep, hJX⟩, ?_⟩, hX⟩
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
⊢ ((M.Indep J ∧ J ⊆ X) ∧ ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ X → J ⊆ b → b ⊆ J) ∧ X ⊆ M.E
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