simp_rw [cocircuit_iff_mem_minimals_compl_nonspanning, hyperplane_iff_maximal_nonspanning,
  (and_comm (b := _ ⊆ _)), mem_minimals_setOf_iff, mem_maximals_setOf_iff,
  diff_diff_cancel_left hH, and_iff_right hH, subset_diff, and_imp, 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 : α
hH : autoParam (H ⊆ M.E) _auto✝
⊢ M.Cocircuit (M.E \ H) ↔ M.Hyperplane 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 : α
hH : autoParam (H ⊆ M.E) _auto✝
⊢ ¬M.Spanning H →
    ((∀ ⦃y : Set α⦄, ¬M.Spanning (M.E \ y) → y ⊆ M.E → Disjoint y H → M.E \ H = y) ↔
      ∀ ⦃y : Set α⦄, y ⊆ M.E → ¬M.Spanning y → H ⊆ y → H = y)