simp only [h.eq_con_del, delete_ground, contract_ground, diff_diff]
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
h : N ≤m M
⊢ h.C ∪ h.D = M.E \ N.E
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
h : N ≤m M
⊢ h.C ∪ h.D = M.E \ (M.E \ (h.C ∪ h.D))