simp
case inl
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H' B C K : Set α
e f : α
hH₁ hH₂ : M.Hyperplane H₁
⊢ H₁ ∩ H₁ ⋖[M] H₁ ↔ H₁ ∩ H₁ ⋖[M] H₁

case inr
α : 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 : α
hH₁ : M.Hyperplane H₁
hH₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
⊢ H₁ ∩ H₂ ⋖[M] H₁ ↔ H₁ ∩ H₂ ⋖[M] H₂
case inr
α : 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 : α
hH₁ : M.Hyperplane H₁
hH₂ : M.Hyperplane H₂
hne : H₁ ≠ H₂
⊢ H₁ ∩ H₂ ⋖[M] H₁ ↔ H₁ ∩ H₂ ⋖[M] H₂