Theorem: tendsto_mul_ceil_div (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ Tendsto (fun p => ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2) (𝓝[>] 0 ×ˢ atTop) (𝓝 0)
Tactic:
rw [Metric.tendsto_nhds]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ ∀ ε > 0, ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < ε

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ ∀ ε > 0, ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < ε
Tactic:
intro δ hδ
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
⊢ ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < δ

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
⊢ ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < δ
Tactic:
have l1 : ∀ᶠ ε : ℝ in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2) := inter_mem_nhdsWithin _ (Iio_mem_nhds (by positivity))
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
⊢ ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < δ

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
⊢ ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < δ
Tactic:
have l2 : ∀ᶠ N : ℕ in atTop, 1 ≤ δ / 2 * N := by
  apply Tendsto.eventually_ge_atTop
  exact tendsto_natCast_atTop_atTop.const_mul_atTop (by positivity)
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
⊢ ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < δ

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
⊢ ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < δ
Tactic:
filter_upwards [l1.prod_mk l2] with (ε, N) ⟨⟨hε, h1⟩, h2⟩
State after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < (ε, N).1
h1 : (ε, N).1 < δ / 2
h2 : 1 ≤ δ / 2 * ↑(ε, N).2
⊢ dist (↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2) 0 < δ

State before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < (ε, N).1
h1 : (ε, N).1 < δ / 2
h2 : 1 ≤ δ / 2 * ↑(ε, N).2
⊢ dist (↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2) 0 < δ
Tactic:
dsimp only at *
State after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ

State before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ
Tactic:
have l3 : 0 < (N : ℝ) := by
  simp ; rw [Nat.pos_iff_ne_zero] ; rintro rfl ; simp at h2 ; linarith
State after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ

State before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ
Tactic:
have l5 : 0 ≤ ε * ↑N := by positivity
State after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ

State before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ
Tactic:
have l6 : ε * N ≤ δ / 2 * N := mul_le_mul h1.le le_rfl (by positivity) (by positivity)
State after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
l6 : ε * ↑N ≤ δ / 2 * ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ

State before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
l6 : ε * ↑N ≤ δ / 2 * ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ
Tactic:
simp [div_lt_iff l3]
State after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
l6 : ε * ↑N ≤ δ / 2 * ↑N
⊢ ↑⌈ε * ↑N⌉₊ < δ * ↑N

State before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
l6 : ε * ↑N ≤ δ / 2 * ↑N
⊢ ↑⌈ε * ↑N⌉₊ < δ * ↑N
Tactic:
convert (Nat.ceil_lt_add_one l5).trans_le (add_le_add l6 h2) using 1
State after:
case h.e'_4
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
l6 : ε * ↑N ≤ δ / 2 * ↑N
⊢ δ * ↑N = δ / 2 * ↑N + δ / 2 * ↑N

State before:
case h.e'_4
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
l6 : ε * ↑N ≤ δ / 2 * ↑N
⊢ δ * ↑N = δ / 2 * ↑N + δ / 2 * ↑N
Tactic:
ring
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
⊢ 0 < δ / 2
Tactic:
positivity
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
⊢ ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
Tactic:
apply Tendsto.eventually_ge_atTop
State after:
case hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
⊢ Tendsto (fun x => δ / 2 * ↑x) atTop atTop

State before:
case hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
⊢ Tendsto (fun x => δ / 2 * ↑x) atTop atTop
Tactic:
exact tendsto_natCast_atTop_atTop.const_mul_atTop (by positivity)
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
⊢ 0 < δ / 2
Tactic:
positivity
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
⊢ 0 < ↑N
Tactic:
simp
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
⊢ 0 < N

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
⊢ 0 < N
Tactic:
rw [Nat.pos_iff_ne_zero]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
⊢ N ≠ 0

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
⊢ N ≠ 0
Tactic:
rintro rfl
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑0
⊢ False

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑0
⊢ False
Tactic:
simp at h2
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ 0
⊢ False

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ 0
⊢ False
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 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
⊢ 0 ≤ ε * ↑N
Tactic:
positivity
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
⊢ 0 ≤ ↑N
Tactic:
positivity
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
⊢ 0 ≤ δ / 2
Tactic:
positivity
State after:
no goals