nth_rw 1 [← h.cl]
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_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
⊢ (M ↾ R).cl F = M.cl F ∩ R