rintro rfl
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF : M.Flat F
hI : M.Indep I
⊢ M.cl I = F → M.Basis I F
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hI : M.Indep I
hF : M.Flat (M.cl I)
⊢ M.Basis I (M.cl I)