Theorem: Matroid.Nonloop.of_contract (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : (M ／ C).Nonloop e
⊢ M.Nonloop e
Tactic:
rw [← indep_singleton] at h ⊢
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : (M ／ C).Indep {e}
⊢ M.Indep {e}

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : (M ／ C).Indep {e}
⊢ M.Indep {e}
Tactic:
exact h.of_contract
State after:
no goals