Theorem: Matroid.matroid_of_cut_indep_iff (Matroid/Old/ModularCut.lean)

State before:
α : Type u_1
I : Set α
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
e : α
e_nE : e ∉ M.E
⊢ (M.matroid_of_cut hC e_nE).Indep I ↔ if e ∈ I then M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ C else M.Indep I
Tactic:
simp [matroid_of_cut]
State after:
α : Type u_1
I : Set α
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
e : α
e_nE : e ∉ M.E
⊢ (M.indepmatroid_of_cut C hC e_nE).Indep I ↔ if e ∈ I then M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ C else M.Indep I