exact ⟨fun h H hH hXH ↦ h _ hH (inter_subset_left.trans hXH),
  fun h H hH hXH ↦ h H hH (by rwa [inter_eq_self_of_subset_left hX] at hXH )⟩
α : 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
no goals