rintro ⟨C, D, hC, hD, hCD, ⟨e,he⟩, rfl⟩
case mpr
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ (C ∪ D).Nonempty ∧ N = M ／ C ＼ D) →
    (∃ C D, C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = M ／ C ＼ D) ∧ N.E ⊂ M.E
case mpr.intro.intro.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 α
hC : C ⊆ M.E
hD : D ⊆ M.E
hCD : Disjoint C D
e : α
he : e ∈ C ∪ D
⊢ (∃ C_1 D_1, C_1 ⊆ M.E ∧ D_1 ⊆ M.E ∧ Disjoint C_1 D_1 ∧ M ／ C ＼ D = M ／ C_1 ＼ D_1) ∧ (M ／ C ＼ D).E ⊂ M.E