Theorem: Matroid.CovBy.eq_cl_union_of_covBy_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₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
⊢ F = M.cl (F₀ ∪ F₁)
Tactic:
refine subset_antisymm ?_ (h₁.flat_right.cl_subset_of_subset (union_subset h₀.subset h₁.subset))
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₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
⊢ F ⊆ M.cl (F₀ ∪ F₁)

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₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
⊢ F ⊆ M.cl (F₀ ∪ F₁)
Tactic:
have hnss : ¬ (F₀ ⊆ F₁) :=
  fun hss ↦ hne.symm <| h₀.eq_of_subset_of_ssubset h₁.flat_left hss h₁.ssubset
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₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
hnss : ¬F₀ ⊆ F₁
⊢ F ⊆ M.cl (F₀ ∪ F₁)

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₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
hnss : ¬F₀ ⊆ F₁
⊢ F ⊆ M.cl (F₀ ∪ F₁)
Tactic:
obtain ⟨e, he₀, he₁⟩ := not_subset.1 hnss
State after:
case intro.intro
α : 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₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
hnss : ¬F₀ ⊆ F₁
e : α
he₀ : e ∈ F₀
he₁ : e ∉ F₁
⊢ F ⊆ M.cl (F₀ ∪ F₁)

State before:
case intro.intro
α : 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₀ : F₀ ⋖[M] F
h₁ : F₁ ⋖[M] F
hne : F₀ ≠ F₁
hnss : ¬F₀ ⊆ F₁
e : α
he₀ : e ∈ F₀
he₁ : e ∉ F₁
⊢ F ⊆ M.cl (F₀ ∪ F₁)
Tactic:
obtain rfl := h₁.cl_insert_eq ⟨h₀.subset he₀, he₁⟩
State after:
case intro.intro
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hne : F₀ ≠ F₁
hnss : ¬F₀ ⊆ F₁
e : α
he₀ : e ∈ F₀
he₁ : e ∉ F₁
h₀ : F₀ ⋖[M] M.cl (insert e F₁)
h₁ : F₁ ⋖[M] M.cl (insert e F₁)
⊢ M.cl (insert e F₁) ⊆ M.cl (F₀ ∪ F₁)

State before:
case intro.intro
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hne : F₀ ≠ F₁
hnss : ¬F₀ ⊆ F₁
e : α
he₀ : e ∈ F₀
he₁ : e ∉ F₁
h₀ : F₀ ⋖[M] M.cl (insert e F₁)
h₁ : F₁ ⋖[M] M.cl (insert e F₁)
⊢ M.cl (insert e F₁) ⊆ M.cl (F₀ ∪ F₁)
Tactic:
exact M.cl_subset_cl (insert_subset (Or.inl he₀) subset_union_right)
State after:
no goals