no goals
ι : Type ?u.39551
F : Type u_2
α : Type u_3
β : Type u_1
γ : Type ?u.39563
δ : Type ?u.39566
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f x ≤ ↑f y + ↑f (y / x)
simpa only [add_comm, map_div_rev, div_mul_cancel'] using map_mul_le_add f (x / y) y