Theorem: exists_antitone_of_eventually (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
⊢ ∃ v, range v ⊆ range u ∧ Antitone v ∧ v =ᶠ[atTop] u
Tactic:
obtain ⟨N, hN⟩ := eventually_atTop.mp hu
State after:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
⊢ ∃ v, range v ⊆ range u ∧ Antitone v ∧ v =ᶠ[atTop] u

State before:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
⊢ ∃ v, range v ⊆ range u ∧ Antitone v ∧ v =ᶠ[atTop] u
Tactic:
let v (n : ℕ) := u (if n < N then N else n)
State after:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ ∃ v, range v ⊆ range u ∧ Antitone v ∧ v =ᶠ[atTop] u

State before:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ ∃ v, range v ⊆ range u ∧ Antitone v ∧ v =ᶠ[atTop] u
Tactic:
refine ⟨v, ?_, ?_, ?_⟩
State after:
case intro.refine_1
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ range v ⊆ range u

case intro.refine_2
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ Antitone v

case intro.refine_3
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ v =ᶠ[atTop] u

State before:
case intro.refine_1
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ range v ⊆ range u
Tactic:
exact fun x ⟨n, hn⟩ => ⟨if n < N then N else n, hn⟩
State after:
no goals

State before:
case intro.refine_2
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ Antitone v
Tactic:
refine antitone_nat_of_succ_le (fun n => ?_)
State after:
case intro.refine_2
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
⊢ v (n + 1) ≤ v n

State before:
case intro.refine_2
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
⊢ v (n + 1) ≤ v n
Tactic:
by_cases h : n < N
State after:
case pos
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : n < N
⊢ v (n + 1) ≤ v n

case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
⊢ v (n + 1) ≤ v n

State before:
case pos
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : n < N
⊢ v (n + 1) ≤ v n
Tactic:
by_cases h' : n + 1 < N <;> simp [v, h, h']
State after:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : n < N
h' : ¬n + 1 < N
⊢ u (n + 1) ≤ u N

State before:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : n < N
h' : ¬n + 1 < N
⊢ u (n + 1) ≤ u N
Tactic:
have : n + 1 = N := by linarith
State after:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : n < N
h' : ¬n + 1 < N
this : n + 1 = N
⊢ u (n + 1) ≤ u N

State before:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : n < N
h' : ¬n + 1 < N
this : n + 1 = N
⊢ u (n + 1) ≤ u N
Tactic:
simp [this]
State after:
no goals

State before:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : n < N
h' : ¬n + 1 < N
⊢ n + 1 = N
Tactic:
linarith
State after:
no goals

State before:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
⊢ v (n + 1) ≤ v n
Tactic:
have : ¬(n + 1 < N) := by linarith
State after:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
this : ¬n + 1 < N
⊢ v (n + 1) ≤ v n

State before:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
this : ¬n + 1 < N
⊢ v (n + 1) ≤ v n
Tactic:
simp [v, h, this]
State after:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
this : ¬n + 1 < N
⊢ u (n + 1) ≤ u n

State before:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
this : ¬n + 1 < N
⊢ u (n + 1) ≤ u n
Tactic:
apply hN
State after:
case neg.a
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
this : ¬n + 1 < N
⊢ n ≥ N

State before:
case neg.a
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
this : ¬n + 1 < N
⊢ n ≥ N
Tactic:
linarith
State after:
no goals

State before:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
⊢ ¬n + 1 < N
Tactic:
linarith
State after:
no goals

State before:
case intro.refine_3
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ v =ᶠ[atTop] u
Tactic:
have : ∀ᶠ n in atTop, ¬(n < N) := by simpa using ⟨N, fun b hb => by linarith⟩
State after:
case intro.refine_3
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
this : ∀ᶠ (n : ℕ) in atTop, ¬n < N
⊢ v =ᶠ[atTop] u

State before:
case intro.refine_3
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
this : ∀ᶠ (n : ℕ) in atTop, ¬n < N
⊢ v =ᶠ[atTop] u
Tactic:
filter_upwards [this] with n hn
State after:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
this : ∀ᶠ (n : ℕ) in atTop, ¬n < N
n : ℕ
hn : ¬n < N
⊢ v n = u n

State before:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
this : ∀ᶠ (n : ℕ) in atTop, ¬n < N
n : ℕ
hn : ¬n < N
⊢ v n = u n
Tactic:
simp [v, hn]
State after:
no goals

State before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ ∀ᶠ (n : ℕ) in atTop, ¬n < N
Tactic:
simpa using ⟨N, fun b hb => by linarith⟩
State after:
no goals

State before:
n : ℕ
A a b✝ c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
b : ℕ
hb : N ≤ b
⊢ N ≤ b
Tactic:
linarith
State after:
no goals