rw [flat_iff_subset_cl_self]
case refine_2.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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
⊢ (M ↾ R).Flat (F ∩ R)
case refine_2.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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
⊢ (M ↾ R).cl (F ∩ R) ⊆ F ∩ R