refine ⟨fun h ↦ ⟨M.cl F, M.cl_flat F, ?_⟩, ?_⟩
α : 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✝
⊢ (M ↾ R).Flat F ↔ ∃ F', M.Flat F' ∧ F = F' ∩ R
case refine_1
α : 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✝
h : (M ↾ R).Flat F
⊢ F = M.cl F ∩ R

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