Theorem: Bounded.of_bddAbove_of_bddBelow (RealsQuasiMorphisms/Basic.lean)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
boundᵤ : ℤ
hᵤ : Function.BddAboveBy f boundᵤ
boundₗ : ℤ
hₗ : Function.BddBelowBy f boundₗ
⊢ Bounded f (max |boundᵤ| |boundₗ|)
Tactic:
intro g
State after:
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ₗ|

State before:
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ₗ|
Tactic:
apply Int.natAbs_le <;> custom_zify
State after:
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ₗ|)