refine fun hcl ↦ ⟨by_contra fun hf ↦ ?_, fun hfF ↦ ?_⟩
α : 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 : α
hF : M.Flat F
he : e ∈ M.E \ F
⊢ M.cl (insert e F) = M.cl (insert f F) → f ∈ M.E \ F
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 : α
hF : M.Flat F
he : e ∈ M.E \ F
hcl : M.cl (insert e F) = M.cl (insert f F)
hf : f ∉ M.E
⊢ False

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 : α
hF : M.Flat F
he : e ∈ M.E \ F
hcl : M.cl (insert e F) = M.cl (insert f F)
hfF : f ∈ F
⊢ False