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