no goals
ι : Type ?u.2724
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.2736
δ : Type ?u.2739
inst✝³ : Group α
inst✝² : CommSemigroup β
inst✝¹ : LE β
inst✝ : SubmultiplicativeHomClass F α β
f : F
a b : α
⊢ ↑f a ≤ ↑f b * ↑f (a / b)
simpa only [mul_comm, div_mul_cancel'] using map_mul_le_mul f (a / b) b