Theorem: Matroid.Nonloop.contract_indep_iff (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 α
he : M.Nonloop e
⊢ (M ／ e).Indep I ↔ e ∉ I ∧ M.Indep (insert e I)
Tactic:
simp [contract_elem, he.indep.contract_indep_iff]
State after:
no goals