no goals
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
x : γ
⊢ ↑(↑fromAddMonoid (↑(of (fun i => γ →+ β i) i) f)) x = ↑(of β i) (↑f x)
rw [fromAddMonoid_of, AddMonoidHom.coe_comp, Function.comp]