simp [matroid_of_cut]
α : 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
α : 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