exact ⟨H, hH, hFH⟩
case intro.intro.intro.intro.intro
α : 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 : α
hF : M.Flat F
h : F ≠ M.E
e : α
heE : e ∈ M.E
heF : e ∉ M.cl F
H : Set α
hH : M.Hyperplane H
hFH : F ⊆ H
⊢ ∃ H, M.Hyperplane H ∧ F ⊆ H
no goals