Theorem: Filter.Tendsto.eventually_bddAbove (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
⊢ ∀ᶠ (s : Set α) in l.smallSets, BddAbove (f '' s)
Tactic:
obtain ⟨y', hy'⟩ := exists_gt y
State after:
case intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
y' : β
hy' : y < y'
⊢ ∀ᶠ (s : Set α) in l.smallSets, BddAbove (f '' s)

State before:
case intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
y' : β
hy' : y < y'
⊢ ∀ᶠ (s : Set α) in l.smallSets, BddAbove (f '' s)
Tactic:
obtain ⟨s, hsl, hs⟩ := (eventually_le_of_tendsto_lt hy' hf).exists_mem
State after:
case intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
y' : β
hy' : y < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
⊢ ∀ᶠ (s : Set α) in l.smallSets, BddAbove (f '' s)

State before:
case intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
y' : β
hy' : y < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
⊢ ∀ᶠ (s : Set α) in l.smallSets, BddAbove (f '' s)
Tactic:
simp_rw [Filter.eventually_smallSets, bddAbove_def]
State after:
case intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
y' : β
hy' : y < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
⊢ ∃ s ∈ l, ∀ t ⊆ s, ∃ x, ∀ y ∈ f '' t, y ≤ x

State before:
case intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
y' : β
hy' : y < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
⊢ ∃ s ∈ l, ∀ t ⊆ s, ∃ x, ∀ y ∈ f '' t, y ≤ x
Tactic:
refine ⟨s, hsl, fun t ht ↦ ⟨y', fun y hy ↦ ?_⟩⟩
State after:
case intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y✝ : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y✝)
y' : β
hy' : y✝ < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
t : Set α
ht : t ⊆ s
y : β
hy : y ∈ f '' t
⊢ y ≤ y'

State before:
case intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y✝ : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y✝)
y' : β
hy' : y✝ < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
t : Set α
ht : t ⊆ s
y : β
hy : y ∈ f '' t
⊢ y ≤ y'
Tactic:
obtain ⟨x, hxt, hxy⟩ := hy
State after:
case intro.intro.intro.intro.intro
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y✝ : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y✝)
y' : β
hy' : y✝ < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
t : Set α
ht : t ⊆ s
y : β
x : α
hxt : x ∈ t
hxy : f x = y
⊢ y ≤ y'

State before:
case intro.intro.intro.intro.intro
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y✝ : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y✝)
y' : β
hy' : y✝ < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
t : Set α
ht : t ⊆ s
y : β
x : α
hxt : x ∈ t
hxy : f x = y
⊢ y ≤ y'
Tactic:
exact hxy ▸ hs x (ht hxt)
State after:
no goals