obtain rfl := hFF'.cl_insert_eq (hF'.symm.subset <| hF.covByPartition.mem_partOf he)
case pos.intro.intro
α : 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
e : α
he : e ∈ M.E \ F
F' : Set α
hFF' : F ⋖[M] F'
hF' : F' \ F = hF.covByPartition.partOf e
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
case pos.intro.intro
α : 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
e : α
he : e ∈ M.E \ F
hFF' : F ⋖[M] M.cl (insert e F)
hF' : M.cl (insert e F) \ F = hF.covByPartition.partOf e
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F