no goals
ι : Type ?u.7573
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.7585
δ : Type ?u.7588
inst✝³ : Group α
inst✝² : AddCommSemigroup β
inst✝¹ : LE β
inst✝ : MulLEAddHomClass F α β
f : F
a b : α
⊢ ↑f a ≤ ↑f b + ↑f (a / b)
simpa only [add_comm, div_mul_cancel'] using map_mul_le_add f (a / b) b