simp_rw [← M.cl_inter_ground X,
  M.cl_eq_sInter_hyperplanes _ (inter_subset_left.trans hX), mem_inter_iff, and_iff_left he,
  mem_sInter, mem_setOf_eq, and_imp]
α : 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 ↔ ∀ (H : Set α), M.Hyperplane H → X ⊆ H → e ∈ 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 : α
hX : autoParam (X ⊆ M.E) _auto✝
he : autoParam (e ∈ M.E) _auto✝
⊢ (∀ (t : Set α), M.Hyperplane t → X ∩ M.E ⊆ t → e ∈ t) ↔ ∀ (H : Set α), M.Hyperplane H → X ⊆ H → e ∈ H