Theorem: Matroid.CovBy.covBy_cl_union_of_inter_covBy (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₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
⊢ F₀ ⋖[M] M.cl (F₀ ∪ F₁)
Tactic:
obtain ⟨e₀, -, h₀'⟩ := h₀.exists_eq_cl_insert
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₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
⊢ F₀ ⋖[M] 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₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
⊢ F₀ ⋖[M] M.cl (F₀ ∪ F₁)
Tactic:
obtain ⟨e₁, he₁, h₁'⟩ := h₁.exists_eq_cl_insert
State after:
case intro.intro.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₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
e₁ : α
he₁ : e₁ ∈ F₁ \ (F₀ ∩ F₁)
h₁' : M.cl (insert e₁ (F₀ ∩ F₁)) = F₁
⊢ F₀ ⋖[M] M.cl (F₀ ∪ F₁)

State before:
case intro.intro.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₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
e₁ : α
he₁ : e₁ ∈ F₁ \ (F₀ ∩ F₁)
h₁' : M.cl (insert e₁ (F₀ ∩ F₁)) = F₁
⊢ F₀ ⋖[M] M.cl (F₀ ∪ F₁)
Tactic:
nth_rw 2 [← h₀', ← h₁']
State after:
case intro.intro.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₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
e₁ : α
he₁ : e₁ ∈ F₁ \ (F₀ ∩ F₁)
h₁' : M.cl (insert e₁ (F₀ ∩ F₁)) = F₁
⊢ F₀ ⋖[M] M.cl (M.cl (insert e₀ (F₀ ∩ F₁)) ∪ M.cl (insert e₁ (F₀ ∩ F₁)))

State before:
case intro.intro.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₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
e₁ : α
he₁ : e₁ ∈ F₁ \ (F₀ ∩ F₁)
h₁' : M.cl (insert e₁ (F₀ ∩ F₁)) = F₁
⊢ F₀ ⋖[M] M.cl (M.cl (insert e₀ (F₀ ∩ F₁)) ∪ M.cl (insert e₁ (F₀ ∩ F₁)))
Tactic:
rw [cl_cl_union_cl_eq_cl_union, ← singleton_union, ← singleton_union,
  ← union_union_distrib_right, union_comm {e₀}, union_assoc, singleton_union, singleton_union,
  ← M.cl_insert_cl_eq_cl_insert, h₀']
State after:
case intro.intro.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₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
e₁ : α
he₁ : e₁ ∈ F₁ \ (F₀ ∩ F₁)
h₁' : M.cl (insert e₁ (F₀ ∩ F₁)) = F₁
⊢ F₀ ⋖[M] M.cl (insert e₁ F₀)

State before:
case intro.intro.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₀ ∩ F₁ ⋖[M] F₀
h₁ : F₀ ∩ F₁ ⋖[M] F₁
e₀ : α
h₀' : M.cl (insert e₀ (F₀ ∩ F₁)) = F₀
e₁ : α
he₁ : e₁ ∈ F₁ \ (F₀ ∩ F₁)
h₁' : M.cl (insert e₁ (F₀ ∩ F₁)) = F₁
⊢ F₀ ⋖[M] M.cl (insert e₁ F₀)
Tactic:
exact h₀.flat_right.covBy_cl_insert (fun h ↦ he₁.2 ⟨h, he₁.1⟩) (h₁.flat_right.subset_ground he₁.1)
State after:
no goals