no goals
α : Type u
β : Type v
inst✝¹ : Semiring α
inst✝ : Semiring β
f : α → β
hf✝ : IsSemiringHom f
x y : α
hf : IsSemiringHom f
src✝ : IsSemiringHom f := hf
⊢ ∀ (x y : α), f (x + y) = f x + f y
apply @‹IsSemiringHom f›.map_add