Theorem: Matroid.Loop.minor (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
he : M.Loop e
heN : e ∈ N.E
hNM : N ≤m M
⊢ N.Loop e
Tactic:
rw [← not_nonloop_iff]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
he : M.Loop e
heN : e ∈ N.E
hNM : N ≤m M
⊢ ¬N.Nonloop e

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K : Set α
M₀ M₁ M₂ : Matroid α
he : M.Loop e
heN : e ∈ N.E
hNM : N ≤m M
⊢ ¬N.Nonloop e
Tactic:
exact fun hnl ↦ he.not_nonloop <| hnl.of_minor hNM
State after:
no goals