simp [matroidOnUniv, M.clIndep_iff] at hi
case intro
α : 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.matroidOnUniv hM).Indep I
⊢ (M.matroidOnUniv hM).cl X = M.cl X
case intro
α : 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
⊢ (M.matroidOnUniv hM).cl X = M.cl X