simpa [insert_subset_iff, he, heH, subset_diff,
hI.indep.subset_ground, disjoint_iff_inter_eq_empty]
α : 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 : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
hB : M.Base (insert e I)
this : insert e I ∩ (H \ I) = ∅
⊢ insert e I ⊆ M.E \ (H \ I)
no goals