apply Int.natAbs_le <;> custom_zify
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
boundᵤ : ℤ
hᵤ : Function.BddAboveBy f boundᵤ
boundₗ : ℤ
hₗ : Function.BddBelowBy f boundₗ
g : G
⊢ |f g| ≤ max |boundᵤ| |boundₗ|
case a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
boundᵤ : ℤ
hᵤ : Function.BddAboveBy f boundᵤ
boundₗ : ℤ
hₗ : Function.BddBelowBy f boundₗ
g : G
⊢ f g ≤ max ↑(|boundᵤ|) ↑(|boundₗ|)

case a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
boundᵤ : ℤ
hᵤ : Function.BddAboveBy f boundᵤ
boundₗ : ℤ
hₗ : Function.BddBelowBy f boundₗ
g : G
⊢ -f g ≤ max ↑(|boundᵤ|) ↑(|boundₗ|)