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

State before:
G : Type ?u.72001
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
R : ℤ
bound : ℕ
h_a : ∀ (g : ℤ), |toFun f (-g) - -toFun f g| ≤ bound
N : ℕ
h : ∀ (n : ℤ), n ≥ ↑N → toFun f n ≥ -R + ↑bound
n : ℤ
h_le : n ≤ -↑N
⊢ toFun f n - -toFun f (-n) ≤ ↑bound
Tactic:
conv in f n => rw [←neg_neg n]
State after:
G : Type ?u.72001
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
R : ℤ
bound : ℕ
h_a : ∀ (g : ℤ), |toFun f (-g) - -toFun f g| ≤ bound
N : ℕ
h : ∀ (n : ℤ), n ≥ ↑N → toFun f n ≥ -R + ↑bound
n : ℤ
h_le : n ≤ -↑N
⊢ toFun f (- -n) - -toFun f (-n) ≤ ↑bound

State before:
G : Type ?u.72001
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
R : ℤ
bound : ℕ
h_a : ∀ (g : ℤ), |toFun f (-g) - -toFun f g| ≤ bound
N : ℕ
h : ∀ (n : ℤ), n ≥ ↑N → toFun f n ≥ -R + ↑bound
n : ℤ
h_le : n ≤ -↑N
⊢ toFun f (- -n) - -toFun f (-n) ≤ ↑bound
Tactic:
exact Int.le_trans (Int.le_natAbs ..) (Int.ofNat_le.mpr <| h_a (-n))
State after:
no goals

State before:
G : Type ?u.72001
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
R : ℤ
bound : ℕ
h_a : ∀ (g : ℤ), |toFun f (-g) - -toFun f g| ≤ bound
N : ℕ
h : ∀ (n : ℤ), n ≥ ↑N → toFun f n ≥ -R + ↑bound
n : ℤ
h_le : n ≤ -↑N
this : toFun f n - -toFun f (-n) ≤ ↑bound
⊢ toFun f n ≤ R
Tactic:
linarith [this, h (-n) (Int.le_neg_of_le_neg h_le)]
State after:
no goals