simp_rw [← cocircuit_def, dual_dual M, mem_cl_iff_forall_hyperplane (M := M✶) hX he]
α : 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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M✶✶✶.cl X ↔ ∀ (C : Set α), M✶✶.Circuit C → e ∈ C → (X ∩ C).Nonempty
α : 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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ (∀ (H : Set α), M✶.Hyperplane H → X ⊆ H → e ∈ H) ↔ ∀ (C : Set α), M✶.Cocircuit C → e ∈ C → (X ∩ C).Nonempty