no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
δ : Type u_1
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : AddCommMonoid γ
inst✝ : AddCommMonoid δ
g : γ →+ δ
f : (i : ι) → β i →+ γ
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]