Theorem: Matroid.ModularCut.extIndep_iff_of_mem (Matroid/Extension.lean)

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
heI : e ∈ I
⊢ U.ExtIndep e I ↔ M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
Tactic:
simp [ExtIndep, heI]
State after:
no goals