rw [inter_eq_self_of_subset_left hF.subset_ground]
case mpr.intro.intro
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
D F : Set α
hF : M.Flat F
⊢ F \ D = (F ∩ M.E) \ D
no goals