case H.h1.h
X : Type u_1
x y : X
⊢ ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp toFinsupp toFreeAbelianGroup) (singleAddHom x)) 1) y =
    ↑(↑(AddMonoidHom.comp (AddMonoidHom.id (X →₀ ℤ)) (singleAddHom x)) 1) y
X : Type u_1
⊢ AddMonoidHom.comp toFinsupp toFreeAbelianGroup = AddMonoidHom.id (X →₀ ℤ)
ext (x y)
case H.h1.h
X : Type u_1
x y : X
⊢ ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp toFinsupp toFreeAbelianGroup) (singleAddHom x)) 1) y =
    ↑(↑(singleAddHom x) 1) y
case H.h1.h
X : Type u_1
x y : X
⊢ ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp toFinsupp toFreeAbelianGroup) (singleAddHom x)) 1) y =
    ↑(↑(AddMonoidHom.comp (AddMonoidHom.id (X →₀ ℤ)) (singleAddHom x)) 1) y
simp only [AddMonoidHom.id_comp]
case H.h1.h
X : Type u_1
x y : X
⊢ ↑(↑(AddMonoidHom.comp toFinsupp (↑(AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X))) (of x))) 1) y =
    ↑(↑(singleAddHom x) 1) y
case H.h1.h
X : Type u_1
x y : X
⊢ ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp toFinsupp toFreeAbelianGroup) (singleAddHom x)) 1) y =
    ↑(↑(singleAddHom x) 1) y
rw [AddMonoidHom.comp_assoc, Finsupp.toFreeAbelianGroup_comp_singleAddHom]
no goals
case H.h1.h
X : Type u_1
x y : X
⊢ ↑(↑(AddMonoidHom.comp toFinsupp (↑(AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X))) (of x))) 1) y =
    ↑(↑(singleAddHom x) 1) y
simp only [toFinsupp, AddMonoidHom.coe_comp, Finsupp.singleAddHom_apply, Function.comp_apply,
  one_smul, lift.of, AddMonoidHom.flip_apply, smulAddHom_apply, AddMonoidHom.id_apply]