simp only [hF.covByPartition.rel_iff_partOf_eq_partOf', partOf_covByPartition_eq, mem_diff,
  exists_prop, exists_and_left, and_congr_right_iff]
α : 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 f : α
⊢ hF.covByPartition.Rel e f ↔ e ∈ M.E \ F ∧ f ∈ M.E \ F ∧ M.cl (insert e F) = M.cl (insert f 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✝ : α
hF : M.Flat F
e f : α
⊢ e ∈ M.E ∧ e ∉ F →
    f ∈ M.E ∧ f ∉ F → (M.cl (insert e F) \ F = M.cl (insert f F) \ F ↔ M.cl (insert e F) = M.cl (insert f F))