Theorem: Matroid.Hyperplane.inter_ssubset_left_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:
refine inter_subset_left.ssubset_of_ne fun h_eq ↦ hne <| h₁.eq_of_subset h₂ ?_
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_eq : 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_eq : H₁ ∩ H₂ = H₁
⊢ H₁ ⊆ H₂
Tactic:
rw [← h_eq]
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_eq : H₁ ∩ 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_eq : H₁ ∩ H₂ = H₁
⊢ H₁ ∩ H₂ ⊆ H₂
Tactic:
exact inter_subset_right
State after:
no goals