convert (ENat.tsum_encard_eq_encard_sUnion (M ／ e).parallelClasses.pairwiseDisjoint).symm using 1
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ (M.E \ {e}).encard = ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ (M.E \ {e}).encard = (⋃₀ ↑(M ／ e).parallelClasses).encard

case h.e'_3
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard = ∑' (t : ↑↑(M ／ e).parallelClasses), (↑t).encard