obtain ⟨C, D, hC, hD, hCD, ⟨e,(heC | heD)⟩, rfl⟩ :=
  strictMinor_iff_exists_eq_contract_delete.1 h
case refine_1
α : 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
⊢ ∃ e ∈ M.E, N ≤m M ／ e ∨ N ≤m M ＼ e
case refine_1.intro.intro.intro.intro.intro.intro.intro.inl
α : 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 : α
heC : e ∈ C
h : M ／ C ＼ D <m M
⊢ ∃ e ∈ M.E, M ／ C ＼ D ≤m M ／ e ∨ M ／ C ＼ D ≤m M ＼ e

case refine_1.intro.intro.intro.intro.intro.intro.intro.inr
α : 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 : α
heD : e ∈ D
h : M ／ C ＼ D <m M
⊢ ∃ e ∈ M.E, M ／ C ＼ D ≤m M ／ e ∨ M ／ C ＼ D ≤m M ＼ e