exact h.of_delete.of_contract
case 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 α
h : (M ／ C ＼ D).Nonloop e
hNM : M ／ C ＼ D ≤m M
⊢ M.Nonloop e
no goals