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

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

State before:
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
e : α
C : M.ModularCut
he : e ∈ M.E
x✝¹ : Set α
x✝ : x✝¹ ⊆ (C.extension e).E
⊢ (C.extension e).Indep x✝¹ ↔ M.Indep x✝¹
Tactic:
simp [he]
State after:
no goals