rw [← encard_diff_add_encard_of_subset (singleton_subset_iff.2 he), add_comm, encard_singleton]
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ M.E.encard = 1 + ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ 1 + (M.E \ {e}).encard = 1 + ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard