case h1
X : Type u_1
x : X
⊢ ↑(AddMonoidHom.comp toFreeAbelianGroup (singleAddHom x)) 1 =
    ↑(↑(AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X))) (of x)) 1
X : Type u_1
x : X
⊢ AddMonoidHom.comp toFreeAbelianGroup (singleAddHom x) =
    ↑(AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X))) (of x)
ext
no goals
case h1
X : Type u_1
x : X
⊢ ↑(AddMonoidHom.comp toFreeAbelianGroup (singleAddHom x)) 1 =
    ↑(↑(AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X))) (of x)) 1
simp only [AddMonoidHom.coe_comp, Finsupp.singleAddHom_apply, Function.comp_apply, one_smul,
  toFreeAbelianGroup, Finsupp.liftAddHom_apply_single]