no goals
ι : Type ?u.11845
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.11857
δ : Type ?u.11860
inst✝³ : Group α
inst✝² : CommSemigroup β
inst✝¹ : LE β
inst✝ : SubmultiplicativeHomClass F α β
f : F
a b c : α
⊢ ↑f (a / c) ≤ ↑f (a / b) * ↑f (b / c)
simpa only [div_mul_div_cancel'] using map_mul_le_mul f (a / b) (b / c)