simp only [matroidOnUniv_E, mem_univ, matroidOnUniv_Indep, true_and]
case intro.refine_2
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ x ∈ M.cl X, x ∈ (M.matroidOnUniv hM).E ∧ ((M.matroidOnUniv hM).Indep (insert x I) → x ∈ I)
case intro.refine_2
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ x ∈ M.cl X, x ∈ (M.indepMatroidOnUniv hM).E ∧ ((M.indepMatroidOnUniv hM).Indep (insert x I) → x ∈ I)