F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.33978
δ : Type ?u.33981
inst✝² : OrderedAddCommMonoid α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : OrderAddMonoidHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ ↑f a ≤ ↑f 0
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.33978
δ : Type ?u.33981
inst✝² : OrderedAddCommMonoid α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : OrderAddMonoidHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ ↑f a ≤ 0
rw [← map_zero f]
no goals
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.33978
δ : Type ?u.33981
inst✝² : OrderedAddCommMonoid α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : OrderAddMonoidHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ ↑f a ≤ ↑f 0
exact OrderHomClass.mono _ ha