case H
X : Type u_1
x✝ : X
⊢ ↑(AddMonoidHom.comp toFreeAbelianGroup toFinsupp) (of x✝) = ↑(AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)
X : Type u_1
⊢ AddMonoidHom.comp toFreeAbelianGroup toFinsupp = AddMonoidHom.id (FreeAbelianGroup X)
ext
no goals
case H
X : Type u_1
x✝ : X
⊢ ↑(AddMonoidHom.comp toFreeAbelianGroup toFinsupp) (of x✝) = ↑(AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)
rw [toFreeAbelianGroup, toFinsupp, AddMonoidHom.comp_apply, lift.of,
  liftAddHom_apply_single, AddMonoidHom.flip_apply, smulAddHom_apply, one_smul,
  AddMonoidHom.id_apply]