rintro ⟨e, he, (hc | hd)⟩
case refine_2
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
⊢ (∃ e ∈ M.E, N ≤m M ／ e ∨ N ≤m M ＼ e) → N <m M
case refine_2.intro.intro.inl
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
e : α
he : e ∈ M.E
hc : N ≤m M ／ e
⊢ N <m M

case refine_2.intro.intro.inr
α : Type u_1
M M' N : Matroid α
e✝ f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
e : α
he : e ∈ M.E
hd : N ≤m M ＼ e
⊢ N <m M