rw [contract_delete_contract_delete']
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M₃ : Matroid α
C₁ D₁ C₂ D₂ : Set α
⊢ M₃ ／ C₂ ＼ D₂ ／ C₁ ＼ D₁ ≤m M₃
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ M₃ : Matroid α
C₁ D₁ C₂ D₂ : Set α
⊢ M₃ ／ (C₂ ∪ C₁ \ D₂) ＼ (D₂ ∪ D₁) ≤m M₃