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