Theorem: Matroid.ModularCut.extension_delete (Matroid/Old/_ModularCut.lean)

State before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
C : M.ModularCut
e : α
he : e ∉ M.E
⊢ (C.extension e ＼ e).E = M.E
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
C : M.ModularCut
e : α
he : e ∉ M.E
I : Set α
hI : I ⊆ (C.extension e ＼ e).E
⊢ (C.extension e ＼ e).Indep I ↔ M.Indep I
Tactic:
simp [show e ∉ I from fun heI ↦ by simpa using hI heI]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I✝ B : Set α
Ys Xs : Set (Set α)
C : M.ModularCut
e : α
he : e ∉ M.E
I : Set α
hI : I ⊆ (C.extension e ＼ e).E
heI : e ∈ I
⊢ False
Tactic:
simpa using hI heI
State after:
no goals