rintro ⟨F, hF, rfl⟩
case refine_2
α : 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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (∃ F', M.Flat F' ∧ F = F' ∩ R) → (M ↾ R).Flat F
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)