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

State before:
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
e : α
e_nE : e ∉ M.E
⊢ (M.matroid_of_cut hC e_nE).E = insert e M.E
Tactic:
simp [matroid_of_cut]
State after:
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
e : α
e_nE : e ∉ M.E
⊢ (M.indepmatroid_of_cut C hC e_nE).E = insert e M.E