specialize h₄' h_le
case inr
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_le : g ≤ 0
h₃' : toFun f g ≤ bound₃
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
case inr
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ : ℤ
h₁' : Function.BddAboveOnBy f.toFun (Set.Ici 0) bound₁
bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ bound₄ : ℤ
g : G
h_le : g ≤ 0
h₃' : toFun f g ≤ bound₃
h₄' : toFun (-f) g ≤ bound₄
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)