Theorem: Matroid.CovBy.exists_eq_cl_insert (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₁
⊢ ∃ e ∈ F₁ \ F₀, M.cl (insert e F₀) = F₁
Tactic:
obtain ⟨e, he⟩ := exists_of_ssubset h.ssubset
State after:
case 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₁
e : α
he : e ∈ F₁ ∧ e ∉ F₀
⊢ ∃ e ∈ F₁ \ F₀, M.cl (insert e F₀) = F₁

State before:
case 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₁
e : α
he : e ∈ F₁ ∧ e ∉ F₀
⊢ ∃ e ∈ F₁ \ F₀, M.cl (insert e F₀) = F₁
Tactic:
exact ⟨e, he, h.cl_insert_eq he⟩
State after:
no goals