Theorem: Matroid.Hyperplane.inter_ssubset_right_of_ne (Matroid/Flat.lean)

State before:
α : 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₂
Tactic:
rw [inter_comm]
State after:
α : 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₂

State before:
α : 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₂
Tactic:
exact h₂.inter_ssubset_left_of_ne h₁ hne.symm
State after:
no goals