exact h₂.inter_ssubset_left_of_ne h₁ hne.symm
α : 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 : α
h₁ : M.Hyperplane H₁
h₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
⊢ H₂ ∩ H₁ ⊂ H₂
no goals