α : Type u_2
β : Type u_1
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
a✝ b✝ c d : α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : AddHom α β
hf : Monotone ↑f
a b : α
⊢ ↑f a ≤ ↑f (a - b + b)
α : Type u_2
β : Type u_1
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
a✝ b✝ c d : α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : AddHom α β
hf : Monotone ↑f
a b : α
⊢ ↑f a - ↑f b ≤ ↑f (a - b)
rw [tsub_le_iff_right, ← f.map_add]
no goals
α : Type u_2
β : Type u_1
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
a✝ b✝ c d : α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : AddHom α β
hf : Monotone ↑f
a b : α
⊢ ↑f a ≤ ↑f (a - b + b)
exact hf le_tsub_add