Theorem: Matroid.Hyperplane.inter_covBy_comm (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 : α
hH₁ : M.Hyperplane H₁
hH₂ : M.Hyperplane H₂
⊢ H₁ ∩ H₂ ⋖[M] H₁ ↔ H₁ ∩ H₂ ⋖[M] H₂
Tactic:
obtain (rfl | hne) := eq_or_ne H₁ H₂
State after:
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₂

State before:
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₂
Tactic:
simp
State after:
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₂

State before:
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₂
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
State after:
case inr.refine_1
α : 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₁ ∩ H₂ ⋖[M] H₁
⊢ H₁ ∩ H₂ ⋖[M] H₂

case inr.refine_2
α : 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₁ ∩ H₂ ⋖[M] H₂
⊢ H₁ ∩ H₂ ⋖[M] H₁

State before:
case inr.refine_2
α : 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₁ ∩ H₂ ⋖[M] H₂
⊢ H₁ ∩ H₂ ⋖[M] H₁
Tactic:
exact And.left <| h.covBy_and_covBy_of_covBy_of_ssubset_of_ssubset hH₂.covBy hH₁.flat
  (hH₁.inter_ssubset_left_of_ne hH₂ hne) (hH₁.ssubset_ground)
State after:
no goals

State before:
case inr.refine_1
α : 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₁ ∩ H₂ ⋖[M] H₁
⊢ H₁ ∩ H₂ ⋖[M] H₂
Tactic:
exact And.left <| h.covBy_and_covBy_of_covBy_of_ssubset_of_ssubset hH₁.covBy hH₂.flat
  (hH₁.inter_ssubset_right_of_ne hH₂ hne) hH₂.ssubset_ground
State after:
no goals