case H
α : Type u_3
β : Type u_4
γ : Type ?u.264863
ι : Type ?u.264866
M : Type u_2
M' : Type ?u.264872
N : Type u_1
P : Type ?u.264878
G : Type ?u.264881
H : Type ?u.264884
R : Type ?u.264887
S : Type ?u.264890
inst✝¹ : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
⊢ ∀ (x : α),
    AddMonoidHom.comp (AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g)) (singleAddHom x) =
      AddMonoidHom.comp (AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)) (singleAddHom x)
α : Type u_3
β : Type u_4
γ : Type ?u.264863
ι : Type ?u.264866
M : Type u_2
M' : Type ?u.264872
N : Type u_1
P : Type ?u.264878
G : Type ?u.264881
H : Type ?u.264884
R : Type ?u.264887
S : Type ?u.264890
inst✝¹ : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
⊢ AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g) =
    AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)
apply Finsupp.addHom_ext'
case H
α : Type u_3
β : Type u_4
γ : Type ?u.264863
ι : Type ?u.264866
M : Type u_2
M' : Type ?u.264872
N : Type u_1
P : Type ?u.264878
G : Type ?u.264881
H : Type ?u.264884
R : Type ?u.264887
S : Type ?u.264890
inst✝¹ : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
x : α
⊢ AddMonoidHom.comp (AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g)) (singleAddHom x) =
    AddMonoidHom.comp (AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)) (singleAddHom x)
case H
α : Type u_3
β : Type u_4
γ : Type ?u.264863
ι : Type ?u.264866
M : Type u_2
M' : Type ?u.264872
N : Type u_1
P : Type ?u.264878
G : Type ?u.264881
H : Type ?u.264884
R : Type ?u.264887
S : Type ?u.264890
inst✝¹ : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
⊢ ∀ (x : α),
    AddMonoidHom.comp (AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g)) (singleAddHom x) =
      AddMonoidHom.comp (AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)) (singleAddHom x)
intro x
case H.h
α : Type u_3
β : Type u_4
γ : Type ?u.264863
ι : Type ?u.264866
M : Type u_2
M' : Type ?u.264872
N : Type u_1
P : Type ?u.264878
G : Type ?u.264881
H : Type ?u.264884
R : Type ?u.264887
S : Type ?u.264890
inst✝¹ : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
x : α
⊢ ∀ (x_1 : M),
    ↑(AddMonoidHom.comp (AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g)) (singleAddHom x)) x_1 =
      ↑(AddMonoidHom.comp (AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)) (singleAddHom x)) x_1
case H
α : Type u_3
β : Type u_4
γ : Type ?u.264863
ι : Type ?u.264866
M : Type u_2
M' : Type ?u.264872
N : Type u_1
P : Type ?u.264878
G : Type ?u.264881
H : Type ?u.264884
R : Type ?u.264887
S : Type ?u.264890
inst✝¹ : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
x : α
⊢ AddMonoidHom.comp (AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g)) (singleAddHom x) =
    AddMonoidHom.comp (AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)) (singleAddHom x)
apply AddMonoidHom.ext
case H.h
α : Type u_3
β : Type u_4
γ : Type ?u.264863
ι : Type ?u.264866
M : Type u_2
M' : Type ?u.264872
N : Type u_1
P : Type ?u.264878
G : Type ?u.264881
H : Type ?u.264884
R : Type ?u.264887
S : Type ?u.264890
inst✝¹ : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
x : α
x_1 : M
⊢ ↑(AddMonoidHom.comp (AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g)) (singleAddHom x)) x_1 =
    ↑(AddMonoidHom.comp (AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)) (singleAddHom x)) x_1
case H.h
α : Type u_3
β : Type u_4
γ : Type ?u.264863
ι : Type ?u.264866
M : Type u_2
M' : Type ?u.264872
N : Type u_1
P : Type ?u.264878
G : Type ?u.264881
H : Type ?u.264884
R : Type ?u.264887
S : Type ?u.264890
inst✝¹ : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
x : α
⊢ ∀ (x_1 : M),
    ↑(AddMonoidHom.comp (AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g)) (singleAddHom x)) x_1 =
      ↑(AddMonoidHom.comp (AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)) (singleAddHom x)) x_1
intro x_1
case H.h.h
α : Type u_3
β : Type u_4
γ : Type ?u.264863
ι : Type ?u.264866
M : Type u_2
M' : Type ?u.264872
N : Type u_1
P : Type ?u.264878
G : Type ?u.264881
H : Type ?u.264884
R : Type ?u.264887
S : Type ?u.264890
inst✝¹ : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
x : α
x_1 : M
⊢ ∀ (a : β),
    ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g)) (singleAddHom x)) x_1) a =
      ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)) (singleAddHom x)) x_1) a
case H.h
α : Type u_3
β : Type u_4
γ : Type ?u.264863
ι : Type ?u.264866
M : Type u_2
M' : Type ?u.264872
N : Type u_1
P : Type ?u.264878
G : Type ?u.264881
H : Type ?u.264884
R : Type ?u.264887
S : Type ?u.264890
inst✝¹ : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
x : α
x_1 : M
⊢ ↑(AddMonoidHom.comp (AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g)) (singleAddHom x)) x_1 =
    ↑(AddMonoidHom.comp (AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)) (singleAddHom x)) x_1
apply Finsupp.ext
case H.h.h
α : Type u_3
β : Type u_4
γ : Type ?u.264863
ι : Type ?u.264866
M : Type u_2
M' : Type ?u.264872
N : Type u_1
P : Type ?u.264878
G : Type ?u.264881
H : Type ?u.264884
R : Type ?u.264887
S : Type ?u.264890
inst✝¹ : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
x : α
x_1 : M
a : β
⊢ ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g)) (singleAddHom x)) x_1) a =
    ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)) (singleAddHom x)) x_1) a
case H.h.h
α : Type u_3
β : Type u_4
γ : Type ?u.264863
ι : Type ?u.264866
M : Type u_2
M' : Type ?u.264872
N : Type u_1
P : Type ?u.264878
G : Type ?u.264881
H : Type ?u.264884
R : Type ?u.264887
S : Type ?u.264890
inst✝¹ : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
x : α
x_1 : M
⊢ ∀ (a : β),
    ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g)) (singleAddHom x)) x_1) a =
      ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)) (singleAddHom x)) x_1) a
intro a
no goals
case H.h.h
α : Type u_3
β : Type u_4
γ : Type ?u.264863
ι : Type ?u.264866
M : Type u_2
M' : Type ?u.264872
N : Type u_1
P : Type ?u.264878
G : Type ?u.264881
H : Type ?u.264884
R : Type ?u.264887
S : Type ?u.264890
inst✝¹ : AddCommMonoid M
v v₁ v₂ : α →₀ M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
x : α
x_1 : M
a : β
⊢ ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp (addMonoidHom f) (mapRange.addMonoidHom g)) (singleAddHom x)) x_1) a =
    ↑(↑(AddMonoidHom.comp (AddMonoidHom.comp (mapRange.addMonoidHom g) (addMonoidHom f)) (singleAddHom x)) x_1) a
simp only [AddMonoidHom.coe_comp, Finsupp.mapRange_single, Finsupp.mapDomain.addMonoidHom_apply,
  Finsupp.singleAddHom_apply, eq_self_iff_true, Function.comp_apply, Finsupp.mapDomain_single,
  Finsupp.mapRange.addMonoidHom_apply]