exact hd.trans_strictMinor (deleteElem_strictMinor he)
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
no goals