simpa [inter_assoc, diff_eq_empty.2 hR]
α : 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
this : M.cl (F ∩ R) ∩ R ⊆ F
⊢ (M ↾ R).cl (F ∩ R) ⊆ F ∩ R
no goals