Theorem: Matroid.Restriction.restriction_deleteElem (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
h : N ≤r M
he : e ∉ N.E
⊢ Disjoint {e} N.E
Tactic:
simpa
State after:
no goals