Theorem: Tendsto_nhdsWithin_punctured_map_add (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
⊢ Tendsto (fun y => f y + a) (𝓝[>] x) (𝓝[>] (f x + a))
Tactic:
refine tendsto_iff_forall_eventually_mem.mpr ?_
State after:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
⊢ ∀ s ∈ 𝓝[>] (f x + a), ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ s

State before:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
⊢ ∀ s ∈ 𝓝[>] (f x + a), ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ s
Tactic:
intro v hv
State after:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v : Set ℝ
hv : v ∈ 𝓝[>] (f x + a)
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v

State before:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v : Set ℝ
hv : v ∈ 𝓝[>] (f x + a)
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
Tactic:
simp only [mem_nhdsWithin] at hv
State after:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v : Set ℝ
hv : ∃ u, IsOpen u ∧ f x + a ∈ u ∧ u ∩ Ioi (f x + a) ⊆ v
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v

State before:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v : Set ℝ
hv : ∃ u, IsOpen u ∧ f x + a ∈ u ∧ u ∩ Ioi (f x + a) ⊆ v
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
Tactic:
obtain ⟨u, hu, hu2, hu3⟩ := hv
State after:
case intro.intro.intro
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v

State before:
case intro.intro.intro
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
Tactic:
let t := {x | f x + a ∈ u}
State after:
case intro.intro.intro
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v

State before:
case intro.intro.intro
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
Tactic:
have : t ∩ Ioi x ∈ 𝓝[>] x := by
  simp only [mem_nhdsWithin]
  use t
  simp only [subset_inter_iff, inter_subset_left, inter_subset_right, and_self,
    and_true, t]
  simp
  refine ⟨?_, by simp [hu2]⟩
  simp [Metric.isOpen_iff] at hu ⊢
  intro x hx
  obtain ⟨ε, εpos, hε⟩ := hu (f x + a) hx
  simp only [Metric.ball, dist_sub_eq_dist_add_right, setOf_subset_setOf] at hε ⊢
  exact ⟨ε, εpos, fun _ hy ↦ hε (by simp [isometry_iff_dist_eq.mp f_iso, hy])⟩
State after:
case intro.intro.intro
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v

State before:
case intro.intro.intro
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
Tactic:
filter_upwards [this]
State after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
⊢ ∀ a_1 ∈ t ∩ Ioi x, f a_1 + a ∈ v

State before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
⊢ ∀ a_1 ∈ t ∩ Ioi x, f a_1 + a ∈ v
Tactic:
intro b hb
State after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : b ∈ t ∩ Ioi x
⊢ f b + a ∈ v

State before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : b ∈ t ∩ Ioi x
⊢ f b + a ∈ v
Tactic:
simp only [mem_inter_iff, mem_setOf_eq, mem_Ioi, t] at hb
State after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : f b + a ∈ u ∧ x < b
⊢ f b + a ∈ v

State before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : f b + a ∈ u ∧ x < b
⊢ f b + a ∈ v
Tactic:
refine hu3 ?_
State after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : f b + a ∈ u ∧ x < b
⊢ f b + a ∈ u ∩ Ioi (f x + a)

State before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : f b + a ∈ u ∧ x < b
⊢ f b + a ∈ u ∩ Ioi (f x + a)
Tactic:
simp only [mem_inter_iff, mem_Ioi, add_lt_add_iff_right]
State after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : f b + a ∈ u ∧ x < b
⊢ f b + a ∈ u ∧ f x < f b

State before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : f b + a ∈ u ∧ x < b
⊢ f b + a ∈ u ∧ f x < f b
Tactic:
exact ⟨hb.1, f_mono hb.2⟩
State after:
no goals

State before:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ t ∩ Ioi x ∈ 𝓝[>] x
Tactic:
simp only [mem_nhdsWithin]
State after:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ Ioi x ⊆ t ∩ Ioi x

State before:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ Ioi x ⊆ t ∩ Ioi x
Tactic:
use t
State after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen t ∧ x ∈ t ∧ t ∩ Ioi x ⊆ t ∩ Ioi x

State before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen t ∧ x ∈ t ∧ t ∩ Ioi x ⊆ t ∩ Ioi x
Tactic:
simp only [subset_inter_iff, inter_subset_left, inter_subset_right, and_self,
  and_true, t]
State after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen {x | f x + a ∈ u} ∧ x ∈ {x | f x + a ∈ u}

State before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen {x | f x + a ∈ u} ∧ x ∈ {x | f x + a ∈ u}
Tactic:
simp
State after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen {x | f x + a ∈ u} ∧ f x + a ∈ u

State before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen {x | f x + a ∈ u} ∧ f x + a ∈ u
Tactic:
refine ⟨?_, by simp [hu2]⟩
State after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen {x | f x + a ∈ u}

State before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ IsOpen {x | f x + a ∈ u}
Tactic:
simp [Metric.isOpen_iff] at hu ⊢
State after:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
⊢ ∀ (x : ℝ), f x + a ∈ u → ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ {x | f x + a ∈ u}

State before:
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
⊢ ∀ (x : ℝ), f x + a ∈ u → ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ {x | f x + a ∈ u}
Tactic:
intro x hx
State after:
case h
f : ℝ → ℝ
a x✝ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝ + a ∈ u
hu3 : u ∩ Ioi (f x✝ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
⊢ ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ {x | f x + a ∈ u}

State before:
case h
f : ℝ → ℝ
a x✝ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝ + a ∈ u
hu3 : u ∩ Ioi (f x✝ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
⊢ ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ {x | f x + a ∈ u}
Tactic:
obtain ⟨ε, εpos, hε⟩ := hu (f x + a) hx
State after:
case h.intro.intro
f : ℝ → ℝ
a x✝ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝ + a ∈ u
hu3 : u ∩ Ioi (f x✝ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
ε : ℝ
εpos : 0 < ε
hε : Metric.ball (f x + a) ε ⊆ u
⊢ ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ {x | f x + a ∈ u}

State before:
case h.intro.intro
f : ℝ → ℝ
a x✝ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝ + a ∈ u
hu3 : u ∩ Ioi (f x✝ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
ε : ℝ
εpos : 0 < ε
hε : Metric.ball (f x + a) ε ⊆ u
⊢ ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ {x | f x + a ∈ u}
Tactic:
simp only [Metric.ball, dist_sub_eq_dist_add_right, setOf_subset_setOf] at hε ⊢
State after:
case h.intro.intro
f : ℝ → ℝ
a x✝ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝ + a ∈ u
hu3 : u ∩ Ioi (f x✝ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
ε : ℝ
εpos : 0 < ε
hε : {y | dist y (f x + a) < ε} ⊆ u
⊢ ∃ ε, 0 < ε ∧ ∀ (a_1 : ℝ), dist a_1 x < ε → f a_1 + a ∈ u

State before:
case h.intro.intro
f : ℝ → ℝ
a x✝ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝ + a ∈ u
hu3 : u ∩ Ioi (f x✝ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
ε : ℝ
εpos : 0 < ε
hε : {y | dist y (f x + a) < ε} ⊆ u
⊢ ∃ ε, 0 < ε ∧ ∀ (a_1 : ℝ), dist a_1 x < ε → f a_1 + a ∈ u
Tactic:
exact ⟨ε, εpos, fun _ hy ↦ hε (by simp [isometry_iff_dist_eq.mp f_iso, hy])⟩
State after:
no goals

State before:
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
⊢ f x + a ∈ u
Tactic:
simp [hu2]
State after:
no goals

State before:
f : ℝ → ℝ
a x✝¹ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝¹ + a ∈ u
hu3 : u ∩ Ioi (f x✝¹ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
ε : ℝ
εpos : 0 < ε
hε : {y | dist y (f x + a) < ε} ⊆ u
x✝ : ℝ
hy : dist x✝ x < ε
⊢ f x✝ + a ∈ {y | dist y (f x + a) < ε}
Tactic:
simp [isometry_iff_dist_eq.mp f_iso, hy]
State after:
no goals