rw [← contract_inter_ground_eq, hE.1.2.symm.inter_eq, contract_empty, ← delete_inter_ground_eq,
  hE.2.symm.inter_eq, delete_empty]
case intro.intro.intro.intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
C D : Set α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
⊢ M = M ／ C ＼ D
no goals