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

State before:
G : Type ?u.65059
f : AlmostHom ℤ
h : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
⊢ ∃ m, ↑bound * 2 < toFun f ↑m
Tactic:
unfold Function.BddAboveOn Function.BddAboveOnBy at h
State after:
G : Type ?u.65059
f : AlmostHom ℤ
h : ¬∃ b, ∀ {a : ℤ}, a ∈ Set.Ici 0 → toFun f a ≤ b
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
⊢ ∃ m, ↑bound * 2 < toFun f ↑m

State before:
G : Type ?u.65059
f : AlmostHom ℤ
h : ¬∃ b, ∀ {a : ℤ}, a ∈ Set.Ici 0 → toFun f a ≤ b
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
⊢ ∃ m, ↑bound * 2 < toFun f ↑m
Tactic:
push_neg at h
State after:
G : Type ?u.65059
f : AlmostHom ℤ
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
h : ∀ (b : ℤ), Exists fun {a} => a ∈ Set.Ici 0 ∧ b < toFun f a
⊢ ∃ m, ↑bound * 2 < toFun f ↑m

State before:
G : Type ?u.65059
f : AlmostHom ℤ
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
h : ∀ (b : ℤ), Exists fun {a} => a ∈ Set.Ici 0 ∧ b < toFun f a
⊢ ∃ m, ↑bound * 2 < toFun f ↑m
Tactic:
let ⟨m, h_nonneg, h⟩ := h (bound * 2)
State after:
G : Type ?u.65059
f : AlmostHom ℤ
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
h✝ : ∀ (b : ℤ), Exists fun {a} => a ∈ Set.Ici 0 ∧ b < toFun f a
m : ℤ
h_nonneg : m ∈ Set.Ici 0
h : ↑bound * 2 < toFun f m
⊢ ∃ m, ↑bound * 2 < toFun f ↑m

State before:
G : Type ?u.65059
f : AlmostHom ℤ
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
h✝ : ∀ (b : ℤ), Exists fun {a} => a ∈ Set.Ici 0 ∧ b < toFun f a
m : ℤ
h_nonneg : m ∈ Set.Ici 0
h : ↑bound * 2 < toFun f m
⊢ ∃ m, ↑bound * 2 < toFun f ↑m
Tactic:
exact ⟨m.toNat, Int.toNat_of_nonneg h_nonneg ▸ h⟩
State after:
no goals

State before:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
h_ge : n ≥ ↑(Int.toNat R + (m + 3) * bound)
⊢ toFun f n ≥ R
Tactic:
let n' := n.toNat
State after:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
h_ge : n ≥ ↑(Int.toNat R + (m + 3) * bound)
n' : ℕ := Int.toNat n
⊢ toFun f n ≥ R

State before:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
h_ge : n ≥ ↑(Int.toNat R + (m + 3) * bound)
n' : ℕ := Int.toNat n
⊢ toFun f n ≥ R
Tactic:
have : ↑n' = n :=
  Int.toNat_of_nonneg <| Int.le_trans (Int.ofNat_zero_le ..) h_ge
State after:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
h_ge : n ≥ ↑(Int.toNat R + (m + 3) * bound)
n' : ℕ := Int.toNat n
this : ↑n' = n
⊢ toFun f n ≥ R

State before:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
h_ge : n ≥ ↑(Int.toNat R + (m + 3) * bound)
n' : ℕ := Int.toNat n
this : ↑n' = n
⊢ toFun f n ≥ R
Tactic:
rewrite [←this] at h_ge ⊢
State after:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
n' : ℕ := Int.toNat n
h_ge : ↑n' ≥ ↑(Int.toNat R + (m + 3) * bound)
this : ↑n' = n
⊢ toFun f ↑n' ≥ R

State before:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
n' : ℕ := Int.toNat n
h_ge : ↑n' ≥ ↑(Int.toNat R + (m + 3) * bound)
this : ↑n' = n
⊢ toFun f ↑n' ≥ R
Tactic:
let h_ge : n' ≥ R.toNat + (m + 3) * bound := Int.ofNat_le.mp h_ge
State after:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
n' : ℕ := Int.toNat n
h_ge✝ : ↑n' ≥ ↑(Int.toNat R + (m + 3) * bound)
this : ↑n' = n
h_ge : n' ≥ Int.toNat R + (m + 3) * bound := Iff.mp Int.ofNat_le h_ge✝
⊢ toFun f ↑n' ≥ R

State before:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
n' : ℕ := Int.toNat n
h_ge✝ : ↑n' ≥ ↑(Int.toNat R + (m + 3) * bound)
this : ↑n' = n
h_ge : n' ≥ Int.toNat R + (m + 3) * bound := Iff.mp Int.ofNat_le h_ge✝
⊢ toFun f ↑n' ≥ R
Tactic:
calc f n' ≥ n' - ↑((m + 3) * bound)
              := positive_linear_growth_of_large_enough_value h_a h n'
        _ ≥ ↑(R.toNat + (m + 3) * bound) - ↑((m + 3) * bound)
              := Int.sub_le_sub_right (c := _) <| Int.ofNat_le.mpr h_ge
        _ ≥ R.toNat := by custom_zify; linarith
        _ ≥ R       := Int.self_le_toNat ..
State after:
no goals

State before:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
n' : ℕ := Int.toNat n
h_ge✝ : ↑n' ≥ ↑(Int.toNat R + (m + 3) * bound)
this : ↑n' = n
h_ge : n' ≥ Int.toNat R + (m + 3) * bound := Iff.mp Int.ofNat_le h_ge✝
⊢ ↑(Int.toNat R + (m + 3) * bound) - ↑((m + 3) * bound) ≥ ↑(Int.toNat R)
Tactic:
custom_zify
State after:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
n' : ℕ := Int.toNat n
h_ge✝ : ↑n' ≥ ↑(Int.toNat R + (m + 3) * bound)
this : ↑n' = n
h_ge : n' ≥ Int.toNat R + (m + 3) * bound := Iff.mp Int.ofNat_le h_ge✝
⊢ ↑(Int.toNat R) + (↑m + (1 + 1 + 1)) * ↑bound - (↑m + (1 + 1 + 1)) * ↑bound ≥ ↑(Int.toNat R)

State before:
G : Type ?u.65059
f : AlmostHom ℤ
h✝ : ¬Function.BddAboveOn f.toFun (Set.Ici 0)
bound : ℕ
h_a : ∀ (g₁ g₂ : ℤ), |toFun f (g₁ + g₂) - toFun f g₁ - toFun f g₂| ≤ bound
m : ℕ
h : ↑bound * 2 < toFun f ↑m
R n : ℤ
n' : ℕ := Int.toNat n
h_ge✝ : ↑n' ≥ ↑(Int.toNat R + (m + 3) * bound)
this : ↑n' = n
h_ge : n' ≥ Int.toNat R + (m + 3) * bound := Iff.mp Int.ofNat_le h_ge✝
⊢ ↑(Int.toNat R) + (↑m + (1 + 1 + 1)) * ↑bound - (↑m + (1 + 1 + 1)) * ↑bound ≥ ↑(Int.toNat R)
Tactic:
linarith
State after:
no goals