[GOAL]
X : Type u_1
x : X
⊢ AddMonoidHom.comp toFreeAbelianGroup (singleAddHom x) =
    ↑(AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X))) (of x)
[PROOFSTEP]
ext
[GOAL]
case h1
X : Type u_1
x : X
⊢ ↑(AddMonoidHom.comp toFreeAbelianGroup (singleAddHom x)) 1 =
    ↑(↑(AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X))) (of x)) 1
[PROOFSTEP]
simp only [AddMonoidHom.coe_comp, Finsupp.singleAddHom_apply, Function.comp_apply, one_smul, toFreeAbelianGroup,
  Finsupp.liftAddHom_apply_single]
[GOAL]
X : Type u_1
⊢ AddMonoidHom.comp toFinsupp toFreeAbelianGroup = AddMonoidHom.id (X →₀ ℤ)
[PROOFSTEP]
ext x y
[GOAL]
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
[PROOFSTEP]
simp only [AddMonoidHom.id_comp]
[GOAL]
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
[PROOFSTEP]
rw [AddMonoidHom.comp_assoc, Finsupp.toFreeAbelianGroup_comp_singleAddHom]
[GOAL]
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
[PROOFSTEP]
simp only [toFinsupp, AddMonoidHom.coe_comp, Finsupp.singleAddHom_apply, Function.comp_apply, one_smul, lift.of,
  AddMonoidHom.flip_apply, smulAddHom_apply, AddMonoidHom.id_apply]
[GOAL]
X : Type u_1
⊢ AddMonoidHom.comp toFreeAbelianGroup toFinsupp = AddMonoidHom.id (FreeAbelianGroup X)
[PROOFSTEP]
ext
[GOAL]
case H
X : Type u_1
x✝ : X
⊢ ↑(AddMonoidHom.comp toFreeAbelianGroup toFinsupp) (of x✝) = ↑(AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)
[PROOFSTEP]
rw [toFreeAbelianGroup, toFinsupp, AddMonoidHom.comp_apply, lift.of, liftAddHom_apply_single, AddMonoidHom.flip_apply,
  smulAddHom_apply, one_smul, AddMonoidHom.id_apply]
[GOAL]
X✝ : Type u_1
X : Type u_2
x : FreeAbelianGroup X
⊢ ↑toFreeAbelianGroup (↑toFinsupp x) = x
[PROOFSTEP]
rw [← AddMonoidHom.comp_apply, Finsupp.toFreeAbelianGroup_comp_toFinsupp, AddMonoidHom.id_apply]
[GOAL]
X : Type u_1
x : X
⊢ ↑toFinsupp (of x) = single x 1
[PROOFSTEP]
simp only [toFinsupp, lift.of]
[GOAL]
X : Type u_1
f : X →₀ ℤ
⊢ ↑toFinsupp (↑toFreeAbelianGroup f) = f
[PROOFSTEP]
rw [← AddMonoidHom.comp_apply, toFinsupp_comp_toFreeAbelianGroup, AddMonoidHom.id_apply]
[GOAL]
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ x ∈ support a ↔ ↑(coeff x) a ≠ 0
[PROOFSTEP]
rw [support, Finsupp.mem_support_iff]
[GOAL]
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ ↑(↑toFinsupp a) x ≠ 0 ↔ ↑(coeff x) a ≠ 0
[PROOFSTEP]
exact Iff.rfl
[GOAL]
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ ¬x ∈ support a ↔ ↑(coeff x) a = 0
[PROOFSTEP]
rw [support, Finsupp.not_mem_support_iff]
[GOAL]
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ ↑(↑toFinsupp a) x = 0 ↔ ↑(coeff x) a = 0
[PROOFSTEP]
exact Iff.rfl
[GOAL]
X : Type u_1
⊢ support 0 = ∅
[PROOFSTEP]
simp only [support, Finsupp.support_zero, AddMonoidHom.map_zero]
[GOAL]
X : Type u_1
x : X
⊢ support (of x) = {x}
[PROOFSTEP]
rw [support, toFinsupp_of, Finsupp.support_single_ne_zero _ one_ne_zero]
[GOAL]
X : Type u_1
a : FreeAbelianGroup X
⊢ support (-a) = support a
[PROOFSTEP]
simp only [support, AddMonoidHom.map_neg, Finsupp.support_neg]
[GOAL]
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ support (k • a) = support a
[PROOFSTEP]
ext x
[GOAL]
case a
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
x : X
⊢ x ∈ support (k • a) ↔ x ∈ support a
[PROOFSTEP]
simp only [mem_support_iff, AddMonoidHom.map_zsmul]
[GOAL]
case a
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
x : X
⊢ k • ↑(coeff x) a ≠ 0 ↔ ↑(coeff x) a ≠ 0
[PROOFSTEP]
simp only [h, zsmul_int_int, false_or_iff, Ne.def, mul_eq_zero]
[GOAL]
X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ support (k • a) = support a
[PROOFSTEP]
apply support_zsmul k _ a
[GOAL]
X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ ↑k ≠ 0
[PROOFSTEP]
exact_mod_cast h
[GOAL]
X : Type u_1
a b : FreeAbelianGroup X
⊢ support (a + b) ⊆ support a ∪ support b
[PROOFSTEP]
simp only [support, AddMonoidHom.map_add]
[GOAL]
X : Type u_1
a b : FreeAbelianGroup X
⊢ (↑toFinsupp a + ↑toFinsupp b).support ⊆ (↑toFinsupp a).support ∪ (↑toFinsupp b).support
[PROOFSTEP]
apply Finsupp.support_add
