rw [← compl_cocircuit_iff_hyperplane, diff_diff_right, diff_self, empty_union, inter_comm,
  inter_eq_left.mpr h]
α : 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 : α
h : autoParam (K ⊆ M.E) _auto✝
⊢ M.Hyperplane (M.E \ K) ↔ M.Cocircuit K
no goals