Theorem: Matroid.CovBy.cl_insert_eq (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₁
he : e ∈ F₁ \ F₀
⊢ M.cl (insert e F₀) = F₁
Tactic:
refine'
  h.eq_of_ssubset_of_subset (M.cl_flat _)
    ((ssubset_insert he.2).trans_subset (M.subset_cl _ _))
    (h.flat_right.cl_subset_of_subset (insert_subset he.1 h.ssubset.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₁
he : e ∈ F₁ \ F₀
⊢ insert e F₀ ⊆ M.E

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₁
he : e ∈ F₁ \ F₀
⊢ insert e F₀ ⊆ M.E
Tactic:
rw [insert_eq, union_subset_iff, singleton_subset_iff]
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₁
he : e ∈ F₁ \ F₀
⊢ e ∈ M.E ∧ F₀ ⊆ M.E

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₁
he : e ∈ F₁ \ F₀
⊢ e ∈ M.E ∧ F₀ ⊆ M.E
Tactic:
exact ⟨h.flat_right.subset_ground he.1, h.flat_left.subset_ground⟩
State after:
no goals