no goals
α : Type u_4
ι : Type ?u.518287
γ : Type ?u.518290
A : Type ?u.518293
B : Type ?u.518296
C : Type ?u.518299
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g✝ : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type ?u.521429
M : Type u_1
M' : Type ?u.521435
N : Type u_2
P : Type u_3
G : Type ?u.521444
H : Type ?u.521447
R : Type ?u.521450
S : Type ?u.521453
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
g : N →+ P
f : α → M →+ N
a : α
⊢ ↑(AddEquiv.symm liftAddHom) (AddMonoidHom.comp g (↑liftAddHom f)) a = AddMonoidHom.comp g (f a)
rw [liftAddHom_symm_apply, AddMonoidHom.comp_assoc, liftAddHom_comp_single]