rintro F' ⟨hF', hIF'⟩ e (he : M.Basis I (insert e I))
α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J X Y B C R : Set α
e f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
⊢ ∀ t' ∈ {F | M.Flat F ∧ I ∩ M.E ⊆ F}, F ⊆ t'
case intro
α : Type u_1
ι : Type u_2
M : Matroid α
F✝ I J X Y B C R : Set α
e✝ f x y : α
hI : M.Indep I
F : Set α := {x | M.Basis I (insert x I)}
hIF : M.Basis I F
hF : M.Flat F
F' : Set α
hF' : M.Flat F'
hIF' : I ∩ M.E ⊆ F'
e : α
he : M.Basis I (insert e I)
⊢ e ∈ F'