Theorem: AlmostHom.bounded_of_nonneg_of_nonpos (RealsQuasiMorphisms/Order.lean)

State before:
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₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
⊢ |toFun f g| ≤ Int.toNat (max (max bound₁ bound₂) (max bound₃ bound₄))
Tactic:
custom_zify
State after:
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₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
⊢ ↑(|toFun f g|) ≤ ↑(Int.toNat (max (max bound₁ bound₂) (max bound₃ bound₄)))

State before:
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₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
⊢ ↑(|toFun f g|) ≤ ↑(Int.toNat (max (max bound₁ bound₂) (max bound₃ bound₄)))
Tactic:
refine Int.le_trans ?_ (Int.self_le_toNat ..)
State after:
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₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)

State before:
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₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Tactic:
cases le_total 0 g
State after:
case inl
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₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h✝ : 0 ≤ g
⊢ ↑(|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₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h✝ : g ≤ 0
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)

State before:
case inl
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₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h✝ : 0 ≤ g
⊢ ↑(|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₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h✝ : g ≤ 0
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Tactic:
case' inl h_ge =>
  specialize h₁' h_ge; specialize h₂' h_ge
  refine Int.le_trans ?_ (Int.le_max_left ..)
State after:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ ↑(|toFun f g|) ≤ 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₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h✝ : g ≤ 0
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)

State before:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ ↑(|toFun f g|) ≤ 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₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h✝ : g ≤ 0
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Tactic:
case' inr h_le =>
  specialize h₃' h_le; specialize h₄' h_le
  refine Int.le_trans ?_ (Int.le_max_right ..)
State after:
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 bound₃ bound₄

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

State before:
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 bound₃ bound₄

case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ ↑(|toFun f g|) ≤ max bound₁ bound₂
Tactic:
all_goals apply Int.natAbs_le' <;>
  (apply Int.le_trans (by assumption)
   solve| apply Int.le_max_left | apply Int.le_max_right)
State after:
no goals

State before:
case inl
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₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Tactic:
specialize h₁' h_ge
State after:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ : ℤ
h₂' : Function.BddAboveOnBy (-f).toFun (Set.Ici 0) bound₂
bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)

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

State before:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Tactic:
refine Int.le_trans ?_ (Int.le_max_left ..)
State after:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ ↑(|toFun f g|) ≤ max bound₁ bound₂

State before:
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₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_le : g ≤ 0
⊢ ↑(|toFun f g|) ≤ max (max bound₁ bound₂) (max bound₃ bound₄)
Tactic:
specialize h₃' h_le
State after:
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₄)

State before:
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₄)
Tactic:
specialize h₄' h_le
State after:
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₄)

State before:
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₄)
Tactic:
refine Int.le_trans ?_ (Int.le_max_right ..)
State after:
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 bound₃ bound₄

State before:
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ ↑(|toFun f g|) ≤ max bound₁ bound₂
Tactic:
apply Int.natAbs_le' <;>
(apply Int.le_trans (by assumption)
solve| apply Int.le_max_left | apply Int.le_max_right)
State after:
no goals

State before:
case inl.h₂
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ -toFun f g ≤ max bound₁ bound₂
Tactic:
apply Int.le_trans (by assumption)
State after:
case inl.h₂
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ bound₂ ≤ max bound₁ bound₂

State before:
case inl.h₂
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ bound₂ ≤ max bound₁ bound₂
Tactic:
solve| apply Int.le_max_left | apply Int.le_max_right
State after:
no goals

State before:
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ -toFun f g ≤ ?m.42307
Tactic:
assumption
State after:
no goals

State before:
case inl.h₁
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ bound₁ ≤ max bound₁ bound₂
Tactic:
apply Int.le_max_left
State after:
no goals

State before:
case inl.h₂
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ bound₂ ≤ max bound₁ bound₂
Tactic:
apply Int.le_max_right
State after:
no goals