exact ⟨h.flat_right.subset_ground he.1, h.flat_left.subset_ground⟩
α : 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
no goals