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