rw [delete_eq_restrict, diff_diff_right, inter_eq_self_of_subset_right hI.indep.subset_ground,
  union_comm]
case h.e'_2
α : 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
⊢ M ↾ (I ∪ M.E \ H) = M ＼ (H \ I)
no goals