rw [ground_eq, ←delete]
case M_eq
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
ground_eq : M.E = (C.extension e).E \ {e}
⊢ C.extension e ↾ M.E = M
case M_eq
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
F : Set α
C : M.ModularCut
hC : C.Nonempty
e : α
he : e ∉ M.E
cl_eq_self : (C.extension e).cl F = F
e_not_mem : ¬(e ∈ F ∧ F \ {e} ∈ C)
ground_eq : M.E = (C.extension e).E \ {e}
⊢ (C.extension e).delete {e} = M