[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
⊢ Disjoint atBot atTop
[PROOFSTEP]
rcases exists_pair_ne α with ⟨x, y, hne⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
⊢ Disjoint atBot atTop
[PROOFSTEP]
by_cases hle : x ≤ y
[GOAL]
case pos
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint atBot atTop
[PROOFSTEP]
refine' disjoint_of_disjoint_of_mem _ (Iic_mem_atBot x) (Ici_mem_atTop y)
[GOAL]
case pos
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint (Iic x) (Ici y)
[PROOFSTEP]
exact Iic_disjoint_Ici.2 (hle.lt_of_ne hne).not_le
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint atBot atTop
[PROOFSTEP]
refine' disjoint_of_disjoint_of_mem _ (Iic_mem_atBot y) (Ici_mem_atTop x)
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint (Iic y) (Ici x)
[PROOFSTEP]
exact Iic_disjoint_Ici.2 hle
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder α
p : α → Prop
⊢ (∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in atTop, p x
[PROOFSTEP]
refine ⟨fun h ↦ h.mono fun x hx ↦ hx x le_rfl, fun h ↦ ?_⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
[PROOFSTEP]
rcases(hasBasis_iInf_principal_finite _).eventually_iff.1 h with ⟨S, hSf, hS⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : Set.Finite S
hS : ∀ ⦃x : α⦄, x ∈ ⋂ (i : α) (_ : i ∈ S), Ici i → p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
[PROOFSTEP]
refine mem_iInf_of_iInter hSf (V := fun x ↦ Ici x.1) (fun _ ↦ Subset.rfl) fun x hx y hy ↦ ?_
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : Set.Finite S
hS : ∀ ⦃x : α⦄, x ∈ ⋂ (i : α) (_ : i ∈ S), Ici i → p x
x : α
hx : x ∈ ⋂ (i : ↑S), (fun x => Ici ↑x) i
y : α
hy : x ≤ y
⊢ p y
[PROOFSTEP]
simp only [mem_iInter] at hS hx 
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : Set.Finite S
x y : α
hy : x ≤ y
hS : ∀ ⦃x : α⦄, (∀ (i : α), i ∈ S → x ∈ Ici i) → p x
hx : ∀ (i : ↑S), x ∈ Ici ↑i
⊢ p y
[PROOFSTEP]
exact hS fun z hz ↦ le_trans (hx ⟨z, hz⟩) hy
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β✝ : Type u_4
γ : Type u_5
α : Type u_6
β : Type u_7
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atTop
h_evtl : ∀ᶠ (x : β) in atTop, p x
⊢ ∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y
[PROOFSTEP]
rw [← Filter.eventually_forall_ge_atTop] at h_evtl 
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β✝ : Type u_4
γ : Type u_5
α : Type u_6
β : Type u_7
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atTop
h_evtl : ∀ᶠ (x : β) in atTop, ∀ (y : β), x ≤ y → p y
⊢ ∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y
[PROOFSTEP]
exact (h_evtl.comap f).filter_mono hf.le_comap
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β✝ : Type u_4
γ : Type u_5
α : Type u_6
β : Type u_7
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, p x
⊢ ∀ᶠ (x : α) in l, ∀ (y : β), y ≤ f x → p y
[PROOFSTEP]
rw [← Filter.eventually_forall_le_atBot] at h_evtl 
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β✝ : Type u_4
γ : Type u_5
α : Type u_6
β : Type u_7
inst✝ : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, ∀ (y : β), y ≤ x → p y
⊢ ∀ᶠ (x : α) in l, ∀ (y : β), y ≤ f x → p y
[PROOFSTEP]
exact (h_evtl.comap f).filter_mono hf.le_comap
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝¹ : Subsingleton α
inst✝ : Preorder α
⊢ atTop = ⊤
[PROOFSTEP]
refine' top_unique fun s hs x => _
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝¹ : Subsingleton α
inst✝ : Preorder α
s : Set α
hs : s ∈ atTop
x : α
⊢ x ∈ s
[PROOFSTEP]
rw [atTop, ciInf_subsingleton x, mem_principal] at hs 
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝¹ : Subsingleton α
inst✝ : Preorder α
s : Set α
x : α
hs : Ici x ⊆ s
⊢ x ∈ s
[PROOFSTEP]
exact hs left_mem_Ici
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
r : α → β → Prop
⊢ (∃ b, ∀ᶠ (a : α) in atTop, r a b) ↔ ∀ᶠ (a₀ : α) in atTop, ∃ b, ∀ (a : α), a ≥ a₀ → r a b
[PROOFSTEP]
simp_rw [eventually_atTop, ← exists_swap (α := α)]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
r : α → β → Prop
⊢ (∃ x y, ∀ (b : α), b ≥ x → r b y) ↔ ∃ a, ∀ (b : α), b ≥ a → ∃ b_1, ∀ (a : α), a ≥ b → r a b_1
[PROOFSTEP]
exact exists_congr fun a ↦ .symm <| forall_ge_iff <| Monotone.exists fun _ _ _ hb H n hn ↦ H n (hb.trans hn)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeInf α
inst✝ : Nonempty α
r : α → β → Prop
⊢ (∃ b, ∀ᶠ (a : α) in atBot, r a b) ↔ ∀ᶠ (a₀ : α) in atBot, ∃ b, ∀ (a : α), a ≤ a₀ → r a b
[PROOFSTEP]
simp_rw [eventually_atBot, ← exists_swap (α := α)]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeInf α
inst✝ : Nonempty α
r : α → β → Prop
⊢ (∃ x y, ∀ (b : α), b ≤ x → r b y) ↔ ∃ a, ∀ (b : α), b ≤ a → ∃ b_1, ∀ (a : α), a ≤ b → r a b_1
[PROOFSTEP]
exact exists_congr fun a ↦ .symm <| forall_le_iff <| Antitone.exists fun _ _ _ hb H n hn ↦ H n (hn.trans hb)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
p : α → Prop
⊢ (∀ (i : α), True → ∃ x, x ∈ Ici i ∧ p x) ↔ ∀ (a : α), ∃ b, b ≥ a ∧ p b
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : NoMaxOrder α
p : α → Prop
⊢ (∀ (i : α), True → ∃ x, x ∈ Ioi i ∧ p x) ↔ ∀ (a : α), ∃ b, b > a ∧ p b
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder β
m : α → β
f : Filter α
⊢ Tendsto m f atTop ↔ ∀ (b : β), ∀ᶠ (a : α) in f, b ≤ m a
[PROOFSTEP]
simp only [atTop, tendsto_iInf, tendsto_principal, mem_Ici]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder β
l : Filter α
f₁ f₂ : α → β
h : f₁ ≤ᶠ[l] f₂
h₁ : Tendsto f₁ l atTop
b : β
⊢ ∀ᶠ (a : α) in l, b ≤ f₂ a
[PROOFSTEP]
filter_upwards [tendsto_atTop.1 h₁ b, h] with x using le_trans
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
⊢ comap (↑e) atTop = atTop
[PROOFSTEP]
simp [atTop, ← e.surjective.iInf_comp]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
⊢ map (↑e) atTop = atTop
[PROOFSTEP]
rw [← e.comap_atTop, map_comap_of_surjective e.surjective]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
l : Filter γ
f : γ → α
e : α ≃o β
⊢ Tendsto (fun x => ↑e (f x)) l atTop ↔ Tendsto f l atTop
[PROOFSTEP]
rw [← e.comap_atTop, tendsto_comap_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
l : Filter γ
f : γ → α
e : α ≃o β
⊢ Tendsto (fun x => ↑e (f x)) l atTop ↔ Tendsto (↑e ∘ f) l atTop
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
F : Filter β
u : α → β
⊢ NeBot (F ⊓ map u atTop) ↔ ∀ (U : Set β), U ∈ F → ∀ (N : α), ∃ n, n ≥ N ∧ u n ∈ U
[PROOFSTEP]
simp_rw [inf_neBot_iff_frequently_left, frequently_map, frequently_atTop]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
F : Filter β
u : α → β
⊢ (∀ {p : β → Prop}, (∀ᶠ (x : β) in F, p x) → ∀ (a : α), ∃ b, b ≥ a ∧ p (u b)) ↔
    ∀ (U : Set β), U ∈ F → ∀ (N : α), ∃ n, n ≥ N ∧ u n ∈ U
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → Prop
h : ∀ (N : ℕ), ∃ n, n > N ∧ P n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
[PROOFSTEP]
choose u hu hu' using h
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → Prop
u : ℕ → ℕ
hu : ∀ (N : ℕ), u N > N
hu' : ∀ (N : ℕ), P (u N)
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
[PROOFSTEP]
refine ⟨fun n => u^[n + 1] 0, strictMono_nat_of_lt_succ fun n => ?_, fun n => ?_⟩
[GOAL]
case refine_1
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → Prop
u : ℕ → ℕ
hu : ∀ (N : ℕ), u N > N
hu' : ∀ (N : ℕ), P (u N)
n : ℕ
⊢ u^[n + 1] 0 < u^[n + 1 + 1] 0
[PROOFSTEP]
exact Trans.trans (hu _) (Function.iterate_succ_apply' _ _ _).symm
[GOAL]
case refine_2
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → Prop
u : ℕ → ℕ
hu : ∀ (N : ℕ), u N > N
hu' : ∀ (N : ℕ), P (u N)
n : ℕ
⊢ P ((fun n => u^[n + 1] 0) n)
[PROOFSTEP]
simpa only [Function.iterate_succ_apply'] using hu' _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → Prop
h : ∃ᶠ (n : ℕ) in atTop, P n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
[PROOFSTEP]
rw [frequently_atTop'] at h 
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → Prop
h : ∀ (a : ℕ), ∃ b, b > a ∧ P b
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
[PROOFSTEP]
exact extraction_of_frequently_atTop' h
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → ℕ → Prop
h : ∀ (n : ℕ), ∃ᶠ (k : ℕ) in atTop, P n k
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
[PROOFSTEP]
simp only [frequently_atTop'] at h 
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → ℕ → Prop
h : ∀ (n a : ℕ), ∃ b, b > a ∧ P n b
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
[PROOFSTEP]
choose u hu hu' using h
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
[PROOFSTEP]
use(fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v : ℕ → ℕ)
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ (StrictMono fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v) ∧
    ∀ (n : ℕ), P n (Nat.recOn n (u 0 0) fun n v => u (n + 1) v)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ StrictMono fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v
[PROOFSTEP]
apply strictMono_nat_of_lt_succ
[GOAL]
case h.left.hf
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∀ (n : ℕ), (Nat.recOn n (u 0 0) fun n v => u (n + 1) v) < Nat.recOn (n + 1) (u 0 0) fun n v => u (n + 1) v
[PROOFSTEP]
intro n
[GOAL]
case h.left.hf
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n : ℕ
⊢ (Nat.recOn n (u 0 0) fun n v => u (n + 1) v) < Nat.recOn (n + 1) (u 0 0) fun n v => u (n + 1) v
[PROOFSTEP]
apply hu
[GOAL]
case h.right
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∀ (n : ℕ), P n (Nat.recOn n (u 0 0) fun n v => u (n + 1) v)
[PROOFSTEP]
intro n
[GOAL]
case h.right
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n : ℕ
⊢ P n (Nat.recOn n (u 0 0) fun n v => u (n + 1) v)
[PROOFSTEP]
cases n
[GOAL]
case h.right.zero
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ P Nat.zero (Nat.recOn Nat.zero (u 0 0) fun n v => u (n + 1) v)
[PROOFSTEP]
simp [hu']
[GOAL]
case h.right.succ
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
n✝ : ℕ
⊢ P (Nat.succ n✝) (Nat.recOn (Nat.succ n✝) (u 0 0) fun n v => u (n + 1) v)
[PROOFSTEP]
simp [hu']
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
P : ℕ → ℕ → Prop
h : ∀ (n : ℕ), ∃ N, ∀ (k : ℕ), k ≥ N → P n k
⊢ ∀ (n : ℕ), ∀ᶠ (k : ℕ) in atTop, P n k
[PROOFSTEP]
simp [eventually_atTop, h]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ (k : ℕ), k < n → ∀ᶠ (a : ℕ) in atTop, p (n * a + k)
⊢ ∀ᶠ (a : ℕ) in atTop, p a
[PROOFSTEP]
simp only [eventually_atTop] at hp ⊢
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ (k : ℕ), k < n → ∃ a, ∀ (b : ℕ), b ≥ a → p (n * b + k)
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → p b
[PROOFSTEP]
choose! N hN using hp
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < n → ∀ (b : ℕ), b ≥ N k → p (n * b + k)
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → p b
[PROOFSTEP]
refine ⟨(Finset.range n).sup (n * N ·), fun b hb => ?_⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < n → ∀ (b : ℕ), b ≥ N k → p (n * b + k)
b : ℕ
hb : b ≥ Finset.sup (Finset.range n) fun x => n * N x
⊢ p b
[PROOFSTEP]
rw [← Nat.div_add_mod b n]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < n → ∀ (b : ℕ), b ≥ N k → p (n * b + k)
b : ℕ
hb : b ≥ Finset.sup (Finset.range n) fun x => n * N x
⊢ p (n * (b / n) + b % n)
[PROOFSTEP]
have hlt := Nat.mod_lt b hn.bot_lt
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < n → ∀ (b : ℕ), b ≥ N k → p (n * b + k)
b : ℕ
hb : b ≥ Finset.sup (Finset.range n) fun x => n * N x
hlt : b % n < n
⊢ p (n * (b / n) + b % n)
[PROOFSTEP]
refine hN _ hlt _ ?_
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < n → ∀ (b : ℕ), b ≥ N k → p (n * b + k)
b : ℕ
hb : b ≥ Finset.sup (Finset.range n) fun x => n * N x
hlt : b % n < n
⊢ b / n ≥ N (b % n)
[PROOFSTEP]
rw [ge_iff_le, Nat.le_div_iff_mul_le hn.bot_lt, mul_comm]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < n → ∀ (b : ℕ), b ≥ N k → p (n * b + k)
b : ℕ
hb : b ≥ Finset.sup (Finset.range n) fun x => n * N x
hlt : b % n < n
⊢ n * N (b % n) ≤ b
[PROOFSTEP]
exact (Finset.le_sup (f := (n * N ·)) (Finset.mem_range.2 hlt)).trans hb
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
u : α → β
h : Tendsto u atTop atTop
a : α
b : β
⊢ ∃ a', a' ≥ a ∧ b ≤ u a'
[PROOFSTEP]
have : Nonempty α := ⟨a⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
u : α → β
h : Tendsto u atTop atTop
a : α
b : β
this : Nonempty α
⊢ ∃ a', a' ≥ a ∧ b ≤ u a'
[PROOFSTEP]
have : ∀ᶠ x in atTop, a ≤ x ∧ b ≤ u x := (eventually_ge_atTop a).and (h.eventually <| eventually_ge_atTop b)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
u : α → β
h : Tendsto u atTop atTop
a : α
b : β
this✝ : Nonempty α
this : ∀ᶠ (x : α) in atTop, a ≤ x ∧ b ≤ u x
⊢ ∃ a', a' ≥ a ∧ b ≤ u a'
[PROOFSTEP]
exact this.exists
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
u : α → β
h : Tendsto u atTop atTop
a : α
b : β
⊢ ∃ a', a' ≥ a ∧ b < u a'
[PROOFSTEP]
cases' exists_gt b with b' hb'
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
u : α → β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
⊢ ∃ a', a' ≥ a ∧ b < u a'
[PROOFSTEP]
rcases exists_le_of_tendsto_atTop h a b' with ⟨a', ha', ha''⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
u : α → β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
a' : α
ha' : a' ≥ a
ha'' : b' ≤ u a'
⊢ ∃ a', a' ≥ a ∧ b < u a'
[PROOFSTEP]
exact ⟨a', ha', lt_of_lt_of_le hb' ha''⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
⊢ ∀ (N : ℕ), ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
[PROOFSTEP]
intro N
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N : ℕ
⊢ ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
[PROOFSTEP]
obtain ⟨k : ℕ, - : k ≤ N, hku : ∀ l ≤ N, u l ≤ u k⟩ : ∃ k ≤ N, ∀ l ≤ N, u l ≤ u k
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N : ℕ
⊢ ∃ k, k ≤ N ∧ ∀ (l : ℕ), l ≤ N → u l ≤ u k
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
⊢ ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
[PROOFSTEP]
exact exists_max_image _ u (finite_le_nat N) ⟨N, le_refl N⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
⊢ ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
[PROOFSTEP]
have ex : ∃ n ≥ N, u k < u n := exists_lt_of_tendsto_atTop hu _ _
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
⊢ ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
[PROOFSTEP]
obtain ⟨n : ℕ, hnN : n ≥ N, hnk : u k < u n, hn_min : ∀ m, m < n → N ≤ m → u m ≤ u k⟩ :
  ∃ n ≥ N, u k < u n ∧ ∀ m, m < n → N ≤ m → u m ≤ u k :=
  by
  rcases Nat.findX ex with ⟨n, ⟨hnN, hnk⟩, hn_min⟩
  push_neg at hn_min 
  exact ⟨n, hnN, hnk, hn_min⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
⊢ ∃ n, n ≥ N ∧ u k < u n ∧ ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
[PROOFSTEP]
rcases Nat.findX ex with ⟨n, ⟨hnN, hnk⟩, hn_min⟩
[GOAL]
case mk.intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hn_min : ∀ (m : ℕ), m < n → ¬(m ≥ N ∧ u k < u m)
hnN : n ≥ N
hnk : u k < u n
⊢ ∃ n, n ≥ N ∧ u k < u n ∧ ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
[PROOFSTEP]
push_neg at hn_min 
[GOAL]
case mk.intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → m ≥ N → u m ≤ u k
⊢ ∃ n, n ≥ N ∧ u k < u n ∧ ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
[PROOFSTEP]
exact ⟨n, hnN, hnk, hn_min⟩
[GOAL]
case intro.intro.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
⊢ ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
[PROOFSTEP]
use n, hnN
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
⊢ ∀ (k : ℕ), k < n → u k < u n
[PROOFSTEP]
rintro (l : ℕ) (hl : l < n)
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
l : ℕ
hl : l < n
⊢ u l < u n
[PROOFSTEP]
have hlk : u l ≤ u k := by
  cases' (le_total l N : l ≤ N ∨ N ≤ l) with H H
  · exact hku l H
  · exact hn_min l hl H
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
l : ℕ
hl : l < n
⊢ u l ≤ u k
[PROOFSTEP]
cases' (le_total l N : l ≤ N ∨ N ≤ l) with H H
[GOAL]
case inl
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
l : ℕ
hl : l < n
H : l ≤ N
⊢ u l ≤ u k
[PROOFSTEP]
exact hku l H
[GOAL]
case inr
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
l : ℕ
hl : l < n
H : N ≤ l
⊢ u l ≤ u k
[PROOFSTEP]
exact hn_min l hl H
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
l : ℕ
hl : l < n
hlk : u l ≤ u k
⊢ u l < u n
[PROOFSTEP]
calc
  u l ≤ u k := hlk
  _ < u n := hnk
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
⊢ ∃ᶠ (n : ℕ) in atTop, ∀ (k : ℕ), k < n → u k < u n
[PROOFSTEP]
simpa [frequently_atTop] using high_scores hu
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : OrderedAddCommGroup β
l : Filter α
f g : α → β
C : β
hf : ∀ᶠ (x : α) in l, C ≤ f x
hg : Tendsto g l atTop
⊢ ∀ᶠ (x : α) in l, (fun x => -f x) x ≤ -C
[PROOFSTEP]
simpa
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : OrderedAddCommGroup β
l : Filter α
f g : α → β
C : β
hf : ∀ᶠ (x : α) in l, C ≤ f x
hg : Tendsto g l atTop
⊢ Tendsto (fun x => (fun x => -f x) x + (fun x => f x + g x) x) l atTop
[PROOFSTEP]
simpa
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : OrderedAddCommGroup β
l : Filter α
f g : α → β
C : β
hf : Tendsto f l atTop
hg : ∀ᶠ (x : α) in l, C ≤ g x
⊢ ∀ᶠ (x : α) in l, (fun x => -g x) x ≤ -C
[PROOFSTEP]
simp [hg]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : OrderedAddCommGroup β
l : Filter α
f g : α → β
C : β
hf : Tendsto f l atTop
hg : ∀ᶠ (x : α) in l, C ≤ g x
⊢ Tendsto (fun x => (fun x => f x + g x) x + (fun x => -g x) x) l atTop
[PROOFSTEP]
simp [hf]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : StrictOrderedSemiring α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x * g x) l atTop
[PROOFSTEP]
refine' tendsto_atTop_mono' _ _ hg
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : StrictOrderedSemiring α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
⊢ g ≤ᶠ[l] fun x => f x * g x
[PROOFSTEP]
filter_upwards [hg.eventually (eventually_ge_atTop 0), hf.eventually (eventually_ge_atTop 1)] with _ using
  le_mul_of_one_le_left
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : StrictOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atBot
⊢ Tendsto (fun x => f x * g x) l atBot
[PROOFSTEP]
have := hf.atTop_mul_atTop <| tendsto_neg_atBot_atTop.comp hg
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : StrictOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atBot
this : Tendsto (fun x => f x * (Neg.neg ∘ g) x) l atTop
⊢ Tendsto (fun x => f x * g x) l atBot
[PROOFSTEP]
simpa only [(· ∘ ·), neg_mul_eq_mul_neg, neg_neg] using tendsto_neg_atTop_atBot.comp this
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : StrictOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x * g x) l atBot
[PROOFSTEP]
have : Tendsto (fun x => -f x * g x) l atTop := (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop hg
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : StrictOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atTop
this : Tendsto (fun x => -f x * g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atBot
[PROOFSTEP]
simpa only [(· ∘ ·), neg_mul_eq_neg_mul, neg_neg] using tendsto_neg_atTop_atBot.comp this
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : StrictOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atBot
⊢ Tendsto (fun x => f x * g x) l atTop
[PROOFSTEP]
have : Tendsto (fun x => -f x * -g x) l atTop :=
  (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop (tendsto_neg_atBot_atTop.comp hg)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : StrictOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atBot
this : Tendsto (fun x => -f x * -g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atTop
[PROOFSTEP]
simpa only [neg_mul_neg] using this
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedAddCommGroup α
⊢ comap abs atTop = atBot ⊔ atTop
[PROOFSTEP]
refine'
  le_antisymm (((atTop_basis.comap _).le_basis_iff (atBot_basis.sup atTop_basis)).2 _)
    (sup_le tendsto_abs_atBot_atTop.le_comap tendsto_abs_atTop_atTop.le_comap)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedAddCommGroup α
⊢ ∀ (i' : α × α), True ∧ True → ∃ i, True ∧ abs ⁻¹' Ici i ⊆ Iic i'.fst ∪ Ici i'.snd
[PROOFSTEP]
rintro ⟨a, b⟩ -
[GOAL]
case mk
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ ∃ i, True ∧ abs ⁻¹' Ici i ⊆ Iic (a, b).fst ∪ Ici (a, b).snd
[PROOFSTEP]
refine' ⟨max (-a) b, trivial, fun x hx => _⟩
[GOAL]
case mk
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedAddCommGroup α
a b x : α
hx : x ∈ abs ⁻¹' Ici (max (-a) b)
⊢ x ∈ Iic (a, b).fst ∪ Ici (a, b).snd
[PROOFSTEP]
rw [mem_preimage, mem_Ici, le_abs', max_le_iff, ← min_neg_neg, le_min_iff, neg_neg] at hx 
[GOAL]
case mk
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedAddCommGroup α
a b x : α
hx : x ≤ a ∧ x ≤ -b ∨ -a ≤ x ∧ b ≤ x
⊢ x ∈ Iic (a, b).fst ∪ Ici (a, b).snd
[PROOFSTEP]
exact hx.imp And.left And.right
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedSemiring α
l : Filter β
f : β → α
n : ℕ
h : Tendsto (fun x => x ^ n) atTop atTop
hn : n = 0
⊢ False
[PROOFSTEP]
simp only [hn, pow_zero, not_tendsto_const_atTop] at h 
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedRing α
⊢ ¬Tendsto (fun x => x ^ 0) atTop atBot
[PROOFSTEP]
simp [not_tendsto_const_atBot]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
hr : 0 < r
h : Tendsto f l atTop
⊢ Tendsto (fun x => r⁻¹ * (r * f x)) l atTop
[PROOFSTEP]
simpa only [inv_mul_cancel_left₀ hr.ne']
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
hr : 0 < r
⊢ Tendsto (fun x => f x * r) l atTop ↔ Tendsto f l atTop
[PROOFSTEP]
simpa only [mul_comm] using tendsto_const_mul_atTop_of_pos hr
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
inst✝ : NeBot l
h : Tendsto f l atTop
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r
[PROOFSTEP]
refine' ⟨fun hrf => not_le.mp fun hr => _, fun hr => (tendsto_const_mul_atTop_of_pos hr).mpr h⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
inst✝ : NeBot l
h : Tendsto f l atTop
hrf : Tendsto (fun x => r * f x) l atTop
hr : r ≤ 0
⊢ False
[PROOFSTEP]
rcases((h.eventually_ge_atTop 0).and (hrf.eventually_gt_atTop 0)).exists with ⟨x, hx, hrx⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
inst✝ : NeBot l
h : Tendsto f l atTop
hrf : Tendsto (fun x => r * f x) l atTop
hr : r ≤ 0
x : β
hx : 0 ≤ f x
hrx : 0 < r * f x
⊢ False
[PROOFSTEP]
exact (mul_nonpos_of_nonpos_of_nonneg hr hx).not_lt hrx
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
inst✝ : NeBot l
h : Tendsto f l atTop
⊢ Tendsto (fun x => f x * r) l atTop ↔ 0 < r
[PROOFSTEP]
simp only [mul_comm _ r, tendsto_const_mul_atTop_iff_pos h]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x / r) l atTop
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.atTop_mul_const (inv_pos.2 hr)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
⊢ Tendsto (fun x => c * x ^ n) atTop atTop ↔ n ≠ 0 ∧ 0 < c
[PROOFSTEP]
refine' ⟨fun h => ⟨_, _⟩, fun h => tendsto_const_mul_pow_atTop h.1 h.2⟩
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
h : Tendsto (fun x => c * x ^ n) atTop atTop
⊢ n ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
h : Tendsto (fun x => c * x ^ 0) atTop atTop
⊢ False
[PROOFSTEP]
simp only [pow_zero, not_tendsto_const_atTop] at h 
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
h : Tendsto (fun x => c * x ^ n) atTop atTop
⊢ 0 < c
[PROOFSTEP]
rcases((h.eventually_gt_atTop 0).and (eventually_ge_atTop 0)).exists with ⟨k, hck, hk⟩
[GOAL]
case refine'_2.intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
h : Tendsto (fun x => c * x ^ n) atTop atTop
k : α
hck : 0 < c * k ^ n
hk : 0 ≤ k
⊢ 0 < c
[PROOFSTEP]
exact pos_of_mul_pos_left hck (pow_nonneg hk _)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atBot
[PROOFSTEP]
simpa only [← mul_neg, ← tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos hr
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x => f x * r) l atBot ↔ Tendsto f l atBot
[PROOFSTEP]
simpa only [mul_comm] using tendsto_const_mul_atBot_of_pos hr
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x => r * f x) l atTop ↔ Tendsto f l atBot
[PROOFSTEP]
simpa only [neg_mul, tendsto_neg_atBot_iff] using tendsto_const_mul_atBot_of_pos (neg_pos.2 hr)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x => f x * r) l atTop ↔ Tendsto f l atBot
[PROOFSTEP]
simpa only [mul_comm] using tendsto_const_mul_atTop_of_neg hr
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atTop
[PROOFSTEP]
simpa only [neg_mul, tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos (neg_pos.2 hr)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x => f x * r) l atBot ↔ Tendsto f l atTop
[PROOFSTEP]
simpa only [mul_comm] using tendsto_const_mul_atBot_of_neg hr
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
[PROOFSTEP]
rcases lt_trichotomy r 0 with (hr | rfl | hr)
[GOAL]
case inl
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
hr : r < 0
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
[PROOFSTEP]
simp [hr, hr.not_lt, tendsto_const_mul_atTop_of_neg]
[GOAL]
case inr.inl
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
inst✝ : NeBot l
⊢ Tendsto (fun x => 0 * f x) l atTop ↔ 0 < 0 ∧ Tendsto f l atTop ∨ 0 < 0 ∧ Tendsto f l atBot
[PROOFSTEP]
simp [not_tendsto_const_atTop]
[GOAL]
case inr.inr
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
hr : 0 < r
⊢ Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
[PROOFSTEP]
simp [hr, hr.not_lt, tendsto_const_mul_atTop_of_pos]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
⊢ Tendsto (fun x => f x * r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
[PROOFSTEP]
simp only [mul_comm _ r, tendsto_const_mul_atTop_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
⊢ Tendsto (fun x => r * f x) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop
[PROOFSTEP]
simp only [← tendsto_neg_atTop_iff, ← mul_neg, tendsto_const_mul_atTop_iff, neg_neg]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
⊢ Tendsto (fun x => f x * r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop
[PROOFSTEP]
simp only [mul_comm _ r, tendsto_const_mul_atBot_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
h : Tendsto f l atBot
⊢ Tendsto (fun x => r * f x) l atTop ↔ r < 0
[PROOFSTEP]
simp [tendsto_const_mul_atTop_iff, h, h.not_tendsto disjoint_atBot_atTop]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
h : Tendsto f l atBot
⊢ Tendsto (fun x => f x * r) l atTop ↔ r < 0
[PROOFSTEP]
simp only [mul_comm _ r, tendsto_const_mul_atTop_iff_neg h]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
h : Tendsto f l atBot
⊢ Tendsto (fun x => r * f x) l atBot ↔ 0 < r
[PROOFSTEP]
simp [tendsto_const_mul_atBot_iff, h, h.not_tendsto disjoint_atBot_atTop]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
h : Tendsto f l atBot
⊢ Tendsto (fun x => f x * r) l atBot ↔ 0 < r
[PROOFSTEP]
simp only [mul_comm _ r, tendsto_const_mul_atBot_iff_pos h]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
h : Tendsto f l atTop
⊢ Tendsto (fun x => r * f x) l atBot ↔ r < 0
[PROOFSTEP]
simp [tendsto_const_mul_atBot_iff, h, h.not_tendsto disjoint_atTop_atBot]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
h : Tendsto f l atTop
⊢ Tendsto (fun x => f x * r) l atBot ↔ r < 0
[PROOFSTEP]
simp only [mul_comm _ r, tendsto_const_mul_atBot_iff_neg h]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r : α
hr : 0 < r
hf : Tendsto f l atBot
⊢ Tendsto (fun x => f x / r) l atBot
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hf.atBot_mul_const (inv_pos.2 hr)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r c : α
n : ℕ
⊢ Tendsto (fun x => c * x ^ n) atTop atBot ↔ n ≠ 0 ∧ c < 0
[PROOFSTEP]
simp only [← tendsto_neg_atTop_iff, ← neg_mul, tendsto_const_mul_pow_atTop_iff, neg_pos]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f : α → β
l : Filter β
⊢ Tendsto f atTop l ↔ ∀ (s : Set β), s ∈ l → ∃ a, ∀ (b : α), b ≥ a → f b ∈ s
[PROOFSTEP]
simp only [tendsto_def, mem_atTop_sets]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f : α → β
l : Filter β
⊢ (∀ (s : Set β), s ∈ l → ∃ a, ∀ (b : α), b ≥ a → b ∈ f ⁻¹' s) ↔ ∀ (s : Set β), s ∈ l → ∃ a, ∀ (b : α), b ≥ a → f b ∈ s
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
s : Set α
⊢ Tendsto f atTop (𝓟 s) ↔ ∃ N, ∀ (n : β), n ≥ N → f n ∈ s
[PROOFSTEP]
rw [tendsto_iff_comap, comap_principal, le_principal_iff, mem_atTop_sets]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
s : Set α
⊢ (∃ a, ∀ (b : β), b ≥ a → b ∈ f ⁻¹' s) ↔ ∃ N, ∀ (n : β), n ≥ N → f n ∈ s
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
e : β → γ
l : Filter α
hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂
hu : ∀ (c : γ), ∃ b, c ≤ e b
⊢ Tendsto (e ∘ f) l atTop ↔ Tendsto f l atTop
[PROOFSTEP]
rw [← comap_embedding_atTop hm hu, tendsto_comap_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
⊢ atTop = ⨅ (x : α), 𝓟 (Ici {x})
[PROOFSTEP]
refine' le_antisymm (le_iInf fun i => le_principal_iff.2 <| mem_atTop { i }) _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
⊢ ⨅ (x : α), 𝓟 (Ici {x}) ≤ atTop
[PROOFSTEP]
refine' le_iInf fun s => le_principal_iff.2 <| mem_iInf_of_iInter s.finite_toSet (fun i => mem_principal_self _) _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
s : Finset α
⊢ ⋂ (i : ↑↑s), Ici {↑i} ⊆ Ici s
[PROOFSTEP]
simp only [subset_def, mem_iInter, SetCoe.forall, mem_Ici, Finset.le_iff_subset, Finset.mem_singleton,
  Finset.subset_iff, forall_eq]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
s : Finset α
⊢ ∀ (x : Finset α), (∀ (x_1 : α), x_1 ∈ ↑s → x_1 ∈ x) → ∀ ⦃x_1 : α⦄, x_1 ∈ s → x_1 ∈ x
[PROOFSTEP]
exact fun t => id
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
⊢ Tendsto f atTop atTop
[PROOFSTEP]
simp only [atTop_finset_eq_iInf, tendsto_iInf, tendsto_principal]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
⊢ ∀ (i : α), ∀ᶠ (a : β) in atTop, f a ∈ Ici {i}
[PROOFSTEP]
intro a
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
a : α
⊢ ∀ᶠ (a_1 : β) in atTop, f a_1 ∈ Ici {a}
[PROOFSTEP]
rcases h' a with ⟨b, hb⟩
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
a : α
b : β
hb : a ∈ f b
⊢ ∀ᶠ (a_1 : β) in atTop, f a_1 ∈ Ici {a}
[PROOFSTEP]
exact (eventually_ge_atTop b).mono fun b' hb' => (Finset.singleton_subset_iff.2 hb).trans (h hb')
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : DecidableEq β
i : β → γ
j : γ → β
h : Function.LeftInverse j i
a : β
⊢ a ∈ Finset.image j {i a}
[PROOFSTEP]
simp only [Finset.image_singleton, h a, Finset.mem_singleton]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ atTop ×ˢ atTop = atTop
[PROOFSTEP]
cases isEmpty_or_nonempty α
[GOAL]
case inl
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝ : IsEmpty α
⊢ atTop ×ˢ atTop = atTop
case inr
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝ : Nonempty α
⊢ atTop ×ˢ atTop = atTop
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case inr
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝ : Nonempty α
⊢ atTop ×ˢ atTop = atTop
[PROOFSTEP]
cases isEmpty_or_nonempty β
[GOAL]
case inr.inl
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : IsEmpty β
⊢ atTop ×ˢ atTop = atTop
case inr.inr
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ atTop ×ˢ atTop = atTop
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case inr.inr
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
h✝¹ : Nonempty α
h✝ : Nonempty β
⊢ atTop ×ˢ atTop = atTop
[PROOFSTEP]
simpa [atTop, prod_iInf_left, prod_iInf_right, iInf_prod] using iInf_comm
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
α₁ : Type u_6
α₂ : Type u_7
β₁ : Type u_8
β₂ : Type u_9
inst✝¹ : Preorder β₁
inst✝ : Preorder β₂
u₁ : β₁ → α₁
u₂ : β₂ → α₂
⊢ map u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop
[PROOFSTEP]
rw [prod_map_map_eq, prod_atTop_atTop_eq, Prod.map_def]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeInf α
⊢ Tendsto (fun a => (a, a)) atBot atBot
[PROOFSTEP]
rw [← prod_atBot_atBot_eq]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeInf α
⊢ Tendsto (fun a => (a, a)) atBot (atBot ×ˢ atBot)
[PROOFSTEP]
exact tendsto_id.prod_mk tendsto_id
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
⊢ Tendsto (fun a => (a, a)) atTop atTop
[PROOFSTEP]
rw [← prod_atTop_atTop_eq]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
⊢ Tendsto (fun a => (a, a)) atTop (atTop ×ˢ atTop)
[PROOFSTEP]
exact tendsto_id.prod_mk tendsto_id
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeInf γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atBot
[PROOFSTEP]
rw [← prod_atBot_atBot_eq]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeInf γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (atBot ×ˢ atBot)
[PROOFSTEP]
exact hf.prod_map hg
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atTop
[PROOFSTEP]
rw [← prod_atTop_atTop_eq]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (atTop ×ˢ atTop)
[PROOFSTEP]
exact hf.prod_map hg
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) atBot atBot
[PROOFSTEP]
rw [← prod_atBot_atBot_eq]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) (atBot ×ˢ atBot) atBot
[PROOFSTEP]
exact hf.prod_map_prod_atBot hg
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) atTop atTop
[PROOFSTEP]
rw [← prod_atTop_atTop_eq]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) (atTop ×ˢ atTop) atTop
[PROOFSTEP]
exact hf.prod_map_prod_atTop hg
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeInf α
inst✝ : Nonempty α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ a, ∀ (k l : α), k ≤ a → l ≤ a → p (k, l)
[PROOFSTEP]
simp [← prod_atBot_atBot_eq, (@atBot_basis α _ _).prod_self.eventually_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeInf α
inst✝ : Nonempty α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ a, ∀ (k : α), k ≤ a → ∀ (l : α), l ≤ a → p (k, l)
[PROOFSTEP]
simp only [eventually_atBot_prod_self, ball_cond_comm]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atTop, p x) ↔ ∃ a, ∀ (k : α), k ≥ a → ∀ (l : α), l ≥ a → p (k, l)
[PROOFSTEP]
simp only [eventually_atTop_prod_self, ball_cond_comm]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)
[PROOFSTEP]
rw [← prod_atTop_atTop_eq] at hp 
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop ×ˢ atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)
[PROOFSTEP]
exact hp.curry
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
g : β → α
b' : β
hf : Monotone f
gc : ∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b)
hgi : ∀ (b : β), b ≥ b' → b ≤ f (g b)
⊢ map f atTop = atTop
[PROOFSTEP]
refine' le_antisymm (hf.tendsto_atTop_atTop fun b => ⟨g (b ⊔ b'), le_sup_left.trans <| hgi _ le_sup_right⟩) _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
g : β → α
b' : β
hf : Monotone f
gc : ∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b)
hgi : ∀ (b : β), b ≥ b' → b ≤ f (g b)
⊢ atTop ≤ map f atTop
[PROOFSTEP]
rw [@map_atTop_eq _ _ ⟨g b'⟩]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
g : β → α
b' : β
hf : Monotone f
gc : ∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b)
hgi : ∀ (b : β), b ≥ b' → b ≤ f (g b)
⊢ atTop ≤ ⨅ (a : α), 𝓟 (f '' {a' | a ≤ a'})
[PROOFSTEP]
refine' le_iInf fun a => iInf_le_of_le (f a ⊔ b') <| principal_mono.2 fun b hb => _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
g : β → α
b' : β
hf : Monotone f
gc : ∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b)
hgi : ∀ (b : β), b ≥ b' → b ≤ f (g b)
a : α
b : β
hb : b ∈ Ici (f a ⊔ b')
⊢ b ∈ f '' {a' | a ≤ a'}
[PROOFSTEP]
rw [mem_Ici, sup_le_iff] at hb 
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
g : β → α
b' : β
hf : Monotone f
gc : ∀ (a : α) (b : β), b ≥ b' → (f a ≤ b ↔ a ≤ g b)
hgi : ∀ (b : β), b ≥ b' → b ≤ f (g b)
a : α
b : β
hb : f a ≤ b ∧ b' ≤ b
⊢ b ∈ f '' {a' | a ≤ a'}
[PROOFSTEP]
exact ⟨g b, (gc _ _ hb.2).1 hb.1, le_antisymm ((gc _ _ hb.2).2 le_rfl) (hgi _ hb.2)⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
⊢ map Subtype.val atTop = atTop
[PROOFSTEP]
haveI : Nonempty s := ⟨⟨a, h le_rfl⟩⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this : Nonempty ↑s
⊢ map Subtype.val atTop = atTop
[PROOFSTEP]
have : Directed (· ≥ ·) fun x : s => 𝓟 (Ici x) := by
  intro x y
  use⟨x ⊔ y ⊔ a, h le_sup_right⟩
  simp only [ge_iff_le, principal_mono, Ici_subset_Ici, ← Subtype.coe_le_coe, Subtype.coe_mk]
  exact ⟨le_sup_left.trans le_sup_left, le_sup_right.trans le_sup_left⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this : Nonempty ↑s
⊢ Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
[PROOFSTEP]
intro x y
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this : Nonempty ↑s
x y : ↑s
⊢ ∃ z,
    (fun x x_1 => x ≥ x_1) ((fun x => 𝓟 (Ici x)) x) ((fun x => 𝓟 (Ici x)) z) ∧
      (fun x x_1 => x ≥ x_1) ((fun x => 𝓟 (Ici x)) y) ((fun x => 𝓟 (Ici x)) z)
[PROOFSTEP]
use⟨x ⊔ y ⊔ a, h le_sup_right⟩
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this : Nonempty ↑s
x y : ↑s
⊢ (fun x x_1 => x ≥ x_1) ((fun x => 𝓟 (Ici x)) x)
      ((fun x => 𝓟 (Ici x)) { val := ↑x ⊔ ↑y ⊔ a, property := (_ : ↑x ⊔ ↑y ⊔ a ∈ s) }) ∧
    (fun x x_1 => x ≥ x_1) ((fun x => 𝓟 (Ici x)) y)
      ((fun x => 𝓟 (Ici x)) { val := ↑x ⊔ ↑y ⊔ a, property := (_ : ↑x ⊔ ↑y ⊔ a ∈ s) })
[PROOFSTEP]
simp only [ge_iff_le, principal_mono, Ici_subset_Ici, ← Subtype.coe_le_coe, Subtype.coe_mk]
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this : Nonempty ↑s
x y : ↑s
⊢ ↑x ≤ ↑x ⊔ ↑y ⊔ a ∧ ↑y ≤ ↑x ⊔ ↑y ⊔ a
[PROOFSTEP]
exact ⟨le_sup_left.trans le_sup_left, le_sup_right.trans le_sup_left⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
⊢ map Subtype.val atTop = atTop
[PROOFSTEP]
simp only [le_antisymm_iff, atTop, le_iInf_iff, le_principal_iff, mem_map, mem_setOf_eq, map_iInf_eq this,
  map_principal]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
⊢ (∀ (i : α), Ici i ∈ ⨅ (i : ↑s), 𝓟 (Subtype.val '' Ici i)) ∧ ∀ (i : ↑s), Subtype.val '' Ici i ∈ ⨅ (a : α), 𝓟 (Ici a)
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
⊢ ∀ (i : α), Ici i ∈ ⨅ (i : ↑s), 𝓟 (Subtype.val '' Ici i)
[PROOFSTEP]
intro x
[GOAL]
case left
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
x : α
⊢ Ici x ∈ ⨅ (i : ↑s), 𝓟 (Subtype.val '' Ici i)
[PROOFSTEP]
refine' mem_of_superset (mem_iInf_of_mem ⟨x ⊔ a, h le_sup_right⟩ (mem_principal_self _)) _
[GOAL]
case left
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
x : α
⊢ Subtype.val '' Ici { val := x ⊔ a, property := (_ : x ⊔ a ∈ s) } ⊆ Ici x
[PROOFSTEP]
rintro _ ⟨y, hy, rfl⟩
[GOAL]
case left.intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
x : α
y : ↑s
hy : y ∈ Ici { val := x ⊔ a, property := (_ : x ⊔ a ∈ s) }
⊢ ↑y ∈ Ici x
[PROOFSTEP]
exact le_trans le_sup_left (Subtype.coe_le_coe.2 hy)
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
⊢ ∀ (i : ↑s), Subtype.val '' Ici i ∈ ⨅ (a : α), 𝓟 (Ici a)
[PROOFSTEP]
intro x
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
x : ↑s
⊢ Subtype.val '' Ici x ∈ ⨅ (a : α), 𝓟 (Ici a)
[PROOFSTEP]
filter_upwards [mem_atTop (↑x ⊔ a)] with b hb
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
s : Set α
h : Ici a ⊆ s
this✝ : Nonempty ↑s
this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)
x : ↑s
b : α
hb : ↑x ⊔ a ≤ b
⊢ b ∈ Subtype.val '' Ici x
[PROOFSTEP]
exact ⟨⟨b, h <| le_sup_right.trans hb⟩, Subtype.coe_le_coe.1 (le_sup_left.trans hb), rfl⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
⊢ atTop = comap Subtype.val atTop
[PROOFSTEP]
rcases isEmpty_or_nonempty (Ioi a) with h | ⟨⟨b, hb⟩⟩
[GOAL]
case inl
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
h : IsEmpty ↑(Ioi a)
⊢ atTop = comap Subtype.val atTop
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case inr.intro.mk
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a b : α
hb : b ∈ Ioi a
⊢ atTop = comap Subtype.val atTop
[PROOFSTEP]
rw [← map_val_atTop_of_Ici_subset (Ici_subset_Ioi.2 hb), comap_map Subtype.coe_injective]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
⊢ atTop = comap Subtype.val atTop
[PROOFSTEP]
rw [← map_val_Ici_atTop a, comap_map Subtype.coe_injective]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
f : β → ↑(Ioi a)
l : Filter β
⊢ Tendsto f l atTop ↔ Tendsto (fun x => ↑(f x)) l atTop
[PROOFSTEP]
rw [atTop_Ioi_eq, tendsto_comap_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
f : β → ↑(Ioi a)
l : Filter β
⊢ Tendsto (Subtype.val ∘ f) l atTop ↔ Tendsto (fun x => ↑(f x)) l atTop
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeInf α
a : α
f : β → ↑(Iio a)
l : Filter β
⊢ Tendsto f l atBot ↔ Tendsto (fun x => ↑(f x)) l atBot
[PROOFSTEP]
rw [atBot_Iio_eq, tendsto_comap_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeInf α
a : α
f : β → ↑(Iio a)
l : Filter β
⊢ Tendsto (Subtype.val ∘ f) l atBot ↔ Tendsto (fun x => ↑(f x)) l atBot
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
f : β → ↑(Ici a)
l : Filter β
⊢ Tendsto f l atTop ↔ Tendsto (fun x => ↑(f x)) l atTop
[PROOFSTEP]
rw [atTop_Ici_eq, tendsto_comap_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
f : β → ↑(Ici a)
l : Filter β
⊢ Tendsto (Subtype.val ∘ f) l atTop ↔ Tendsto (fun x => ↑(f x)) l atTop
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeInf α
a : α
f : β → ↑(Iic a)
l : Filter β
⊢ Tendsto f l atBot ↔ Tendsto (fun x => ↑(f x)) l atBot
[PROOFSTEP]
rw [atBot_Iic_eq, tendsto_comap_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeInf α
a : α
f : β → ↑(Iic a)
l : Filter β
⊢ Tendsto (Subtype.val ∘ f) l atBot ↔ Tendsto (fun x => ↑(f x)) l atBot
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : NoMaxOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atTop l ↔ Tendsto f atTop l
[PROOFSTEP]
rw [← map_val_Ioi_atTop a, tendsto_map'_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeSup α
inst✝ : NoMaxOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atTop l ↔ Tendsto (f ∘ Subtype.val) atTop l
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atTop l ↔ Tendsto f atTop l
[PROOFSTEP]
rw [← map_val_Ici_atTop a, tendsto_map'_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeSup α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atTop l ↔ Tendsto (f ∘ Subtype.val) atTop l
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeInf α
inst✝ : NoMinOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atBot l ↔ Tendsto f atBot l
[PROOFSTEP]
rw [← map_val_Iio_atBot a, tendsto_map'_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : SemilatticeInf α
inst✝ : NoMinOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atBot l ↔ Tendsto (f ∘ Subtype.val) atBot l
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeInf α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atBot l ↔ Tendsto f atBot l
[PROOFSTEP]
rw [← map_val_Iic_atBot a, tendsto_map'_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : SemilatticeInf α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atBot l ↔ Tendsto (f ∘ Subtype.val) atBot l
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
k a : ℕ
h : a ≥ k
⊢ a ≤ (fun a => a - k) a + k
[PROOFSTEP]
rw [tsub_add_cancel_of_le h]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
k b : ℕ
x✝ : b ≥ 0
⊢ b ≤ (fun a => a + k) b - k
[PROOFSTEP]
rw [add_tsub_cancel_right]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : ℕ → α
l : Filter α
k : ℕ
⊢ Tendsto (f ∘ fun n => n + k) atTop l ↔ Tendsto f atTop l
[PROOFSTEP]
rw [← tendsto_map'_iff, map_add_atTop_eq_nat]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
k : ℕ
hk : 0 < k
a b : ℕ
x✝ : b ≥ 1
⊢ a / k ≤ b ↔ a ≤ (fun b => b * k + (k - 1)) b
[PROOFSTEP]
simp only [← Nat.lt_succ_iff, Nat.div_lt_iff_lt_mul hk, Nat.succ_eq_add_one, add_assoc,
  tsub_add_cancel_of_le (Nat.one_le_iff_ne_zero.2 hk.ne'), add_mul, one_mul]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
k : ℕ
hk : 0 < k
b : ℕ
x✝ : b ≥ 1
⊢ b = b * k / k
[PROOFSTEP]
rw [Nat.mul_div_cancel b hk]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
⊢ Tendsto u atTop atTop
[PROOFSTEP]
apply h.tendsto_atTop_atTop
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
⊢ ∀ (b : α), ∃ a, b ≤ u a
[PROOFSTEP]
intro b
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
b : α
⊢ ∃ a, b ≤ u a
[PROOFSTEP]
rcases not_bddAbove_iff.1 H b with ⟨_, ⟨N, rfl⟩, hN⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
b : α
N : ι
hN : b < u N
⊢ ∃ a, b ≤ u a
[PROOFSTEP]
exact ⟨N, le_of_lt hN⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝³ : Nonempty α
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
f : α → β
h : Tendsto f atTop atTop
⊢ ¬BddAbove (range f)
[PROOFSTEP]
rintro ⟨M, hM⟩
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝³ : Nonempty α
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
f : α → β
h : Tendsto f atTop atTop
M : β
hM : M ∈ upperBounds (range f)
⊢ False
[PROOFSTEP]
cases' mem_atTop_sets.mp (h <| Ioi_mem_atTop M) with a ha
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝³ : Nonempty α
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
f : α → β
h : Tendsto f atTop atTop
M : β
hM : M ∈ upperBounds (range f)
a : α
ha : ∀ (b : α), b ≥ a → b ∈ f ⁻¹' Ioi M
⊢ False
[PROOFSTEP]
apply lt_irrefl M
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝³ : Nonempty α
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
f : α → β
h : Tendsto f atTop atTop
M : β
hM : M ∈ upperBounds (range f)
a : α
ha : ∀ (b : α), b ≥ a → b ∈ f ⁻¹' Ioi M
⊢ M < M
[PROOFSTEP]
calc
  M < f a := ha a le_rfl
  _ ≤ M := hM (Set.mem_range_self a)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
f : β → α
g : γ → α
h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
⊢ map (fun s => ∏ b in s, f b) atTop ≤ map (fun s => ∏ x in s, g x) atTop
[PROOFSTEP]
classical
refine' ((atTop_basis.map _).le_basis_iff (atTop_basis.map _)).2 fun b _ => _
let ⟨v, hv⟩ := h_eq b
refine ⟨v, trivial, ?_⟩
simpa [image_subset_iff] using hv
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
f : β → α
g : γ → α
h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
⊢ map (fun s => ∏ b in s, f b) atTop ≤ map (fun s => ∏ x in s, g x) atTop
[PROOFSTEP]
refine' ((atTop_basis.map _).le_basis_iff (atTop_basis.map _)).2 fun b _ => _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
f : β → α
g : γ → α
h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
b : Finset γ
x✝ : True
⊢ ∃ i, True ∧ (fun s => ∏ b in s, f b) '' Ici i ⊆ (fun s => ∏ x in s, g x) '' Ici b
[PROOFSTEP]
let ⟨v, hv⟩ := h_eq b
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
f : β → α
g : γ → α
h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
b : Finset γ
x✝ : True
v : Finset β
hv : ∀ (v' : Finset β), v ⊆ v' → ∃ u', b ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
⊢ ∃ i, True ∧ (fun s => ∏ b in s, f b) '' Ici i ⊆ (fun s => ∏ x in s, g x) '' Ici b
[PROOFSTEP]
refine ⟨v, trivial, ?_⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
f : β → α
g : γ → α
h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
b : Finset γ
x✝ : True
v : Finset β
hv : ∀ (v' : Finset β), v ⊆ v' → ∃ u', b ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
⊢ (fun s => ∏ b in s, f b) '' Ici v ⊆ (fun s => ∏ x in s, g x) '' Ici b
[PROOFSTEP]
simpa [image_subset_iff] using hv
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
⊢ ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ HasAntitoneBasis f (s ∘ φ)
[PROOFSTEP]
suffices : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ m n, m < n → r (φ m) (φ n)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
⊢ ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ HasAntitoneBasis f (s ∘ φ)
[PROOFSTEP]
rcases this with ⟨φ, hφ, hrφ⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
φ : ℕ → ℕ
hφ : StrictMono φ
hrφ : ∀ (m n : ℕ), m < n → r (φ m) (φ n)
⊢ ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ HasAntitoneBasis f (s ∘ φ)
[PROOFSTEP]
exact ⟨φ, hφ, hrφ, hs.comp_strictMono hφ⟩
[GOAL]
case this
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
[PROOFSTEP]
have : ∀ t : Set ℕ, t.Finite → ∀ᶠ n in atTop, ∀ m ∈ t, m < n ∧ r m n := fun t ht =>
  (eventually_all_finite ht).2 fun m _ => (eventually_gt_atTop m).and (hr _)
[GOAL]
case this
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), Set.Finite t → ∀ᶠ (n : ℕ) in atTop, ∀ (m : ℕ), m ∈ t → m < n ∧ r m n
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
[PROOFSTEP]
rcases seq_of_forall_finite_exists fun t ht => (this t ht).exists with ⟨φ, hφ⟩
[GOAL]
case this.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), Set.Finite t → ∀ᶠ (n : ℕ) in atTop, ∀ (m : ℕ), m ∈ t → m < n ∧ r m n
φ : ℕ → ℕ
hφ : ∀ (n m : ℕ), m ∈ φ '' Iio n → m < φ n ∧ r m (φ n)
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
[PROOFSTEP]
simp only [ball_image_iff, forall_and, mem_Iio] at hφ 
[GOAL]
case this.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
s : ℕ → Set α
hs : HasAntitoneBasis f s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), Set.Finite t → ∀ᶠ (n : ℕ) in atTop, ∀ (m : ℕ), m ∈ t → m < n ∧ r m n
φ : ℕ → ℕ
hφ : (∀ (x x_1 : ℕ), x_1 < x → φ x_1 < φ x) ∧ ∀ (x x_1 : ℕ), x_1 < x → r (φ x_1) (φ x)
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
[PROOFSTEP]
exact ⟨φ, forall_swap.2 hφ.1, forall_swap.2 hφ.2⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
inst✝¹ : IsCountablyGenerated f
inst✝ : NeBot f
⊢ ∃ x, Tendsto x atTop f
[PROOFSTEP]
obtain ⟨B, h⟩ := f.exists_antitone_basis
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
inst✝¹ : IsCountablyGenerated f
inst✝ : NeBot f
B : ℕ → Set α
h : HasAntitoneBasis f B
⊢ ∃ x, Tendsto x atTop f
[PROOFSTEP]
choose x hx using fun n => Filter.nonempty_of_mem (h.mem n)
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
inst✝¹ : IsCountablyGenerated f
inst✝ : NeBot f
B : ℕ → Set α
h : HasAntitoneBasis f B
x : ℕ → α
hx : ∀ (n : ℕ), x n ∈ B n
⊢ ∃ x, Tendsto x atTop f
[PROOFSTEP]
exact ⟨x, h.tendsto hx⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
[PROOFSTEP]
haveI h_ne_bot : (atTop : Filter α).NeBot := atTop_neBot
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
[PROOFSTEP]
obtain ⟨ys, h⟩ := exists_seq_tendsto (atTop : Filter α)
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
[PROOFSTEP]
let xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) Finset.nonempty_range_succ ys
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
[PROOFSTEP]
have h_mono : Monotone xs := by
  intro i j hij
  rw [Finset.sup'_le_iff]
  intro k hk
  refine' Finset.le_sup'_of_le _ _ le_rfl
  rw [Finset.mem_range] at hk ⊢
  exact hk.trans_le (add_le_add_right hij _)
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
⊢ Monotone xs
[PROOFSTEP]
intro i j hij
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
i j : ℕ
hij : i ≤ j
⊢ xs i ≤ xs j
[PROOFSTEP]
rw [Finset.sup'_le_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
i j : ℕ
hij : i ≤ j
⊢ ∀ (b : ℕ), b ∈ Finset.range (i + 1) → ys b ≤ xs j
[PROOFSTEP]
intro k hk
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
i j : ℕ
hij : i ≤ j
k : ℕ
hk : k ∈ Finset.range (i + 1)
⊢ ys k ≤ xs j
[PROOFSTEP]
refine' Finset.le_sup'_of_le _ _ le_rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
i j : ℕ
hij : i ≤ j
k : ℕ
hk : k ∈ Finset.range (i + 1)
⊢ k ∈ Finset.range (j + 1)
[PROOFSTEP]
rw [Finset.mem_range] at hk ⊢
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
i j : ℕ
hij : i ≤ j
k : ℕ
hk : k < i + 1
⊢ k < j + 1
[PROOFSTEP]
exact hk.trans_le (add_le_add_right hij _)
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
[PROOFSTEP]
refine' ⟨xs, h_mono, _⟩
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
⊢ Tendsto xs atTop atTop
[PROOFSTEP]
refine' tendsto_atTop_atTop_of_monotone h_mono _
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
⊢ ∀ (b : α), ∃ a, b ≤ xs a
[PROOFSTEP]
have : ∀ a : α, ∃ n : ℕ, a ≤ ys n := by
  rw [tendsto_atTop_atTop] at h 
  intro a
  obtain ⟨i, hi⟩ := h a
  exact ⟨i, hi i le_rfl⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
⊢ ∀ (a : α), ∃ n, a ≤ ys n
[PROOFSTEP]
rw [tendsto_atTop_atTop] at h 
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : ∀ (b : α), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ys a
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
⊢ ∀ (a : α), ∃ n, a ≤ ys n
[PROOFSTEP]
intro a
[GOAL]
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : ∀ (b : α), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ys a
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
a : α
⊢ ∃ n, a ≤ ys n
[PROOFSTEP]
obtain ⟨i, hi⟩ := h a
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : ∀ (b : α), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ys a
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
a : α
i : ℕ
hi : ∀ (a_1 : ℕ), i ≤ a_1 → a ≤ ys a_1
⊢ ∃ n, a ≤ ys n
[PROOFSTEP]
exact ⟨i, hi i le_rfl⟩
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
this : ∀ (a : α), ∃ n, a ≤ ys n
⊢ ∀ (b : α), ∃ a, b ≤ xs a
[PROOFSTEP]
intro a
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
this : ∀ (a : α), ∃ n, a ≤ ys n
a : α
⊢ ∃ a_1, a ≤ xs a_1
[PROOFSTEP]
obtain ⟨i, hi⟩ := this a
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
this : ∀ (a : α), ∃ n, a ≤ ys n
a : α
i : ℕ
hi : a ≤ ys i
⊢ ∃ a_1, a ≤ xs a_1
[PROOFSTEP]
refine' ⟨i, hi.trans _⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
this : ∀ (a : α), ∃ n, a ≤ ys n
a : α
i : ℕ
hi : a ≤ ys i
⊢ ys i ≤ xs i
[PROOFSTEP]
refine' Finset.le_sup'_of_le _ _ le_rfl
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
inst✝² : SemilatticeSup α
inst✝¹ : Nonempty α
inst✝ : IsCountablyGenerated atTop
h_ne_bot : NeBot atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
xs : ℕ → α := fun n => Finset.sup' (Finset.range (n + 1)) (_ : Finset.Nonempty (Finset.range (n + 1))) ys
h_mono : Monotone xs
this : ∀ (a : α), ∃ n, a ≤ ys n
a : α
i : ℕ
hi : a ≤ ys i
⊢ i ∈ Finset.range (i + 1)
[PROOFSTEP]
rw [Finset.mem_range_succ_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
⊢ Tendsto f k l ↔ ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l
[PROOFSTEP]
refine' ⟨fun h x hx => h.comp hx, fun H s hs => _⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
H : ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l
s : Set β
hs : s ∈ l
⊢ s ∈ map f k
[PROOFSTEP]
contrapose! H
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
[PROOFSTEP]
have : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ)) := by simpa [neBot_iff, inf_principal_eq_bot]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
⊢ NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
[PROOFSTEP]
simpa [neBot_iff, inf_principal_eq_bot]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
this : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
[PROOFSTEP]
rcases(k ⊓ 𝓟 (f ⁻¹' sᶜ)).exists_seq_tendsto with ⟨x, hx⟩
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
this : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
x : ℕ → α
hx : Tendsto x atTop (k ⊓ 𝓟 (f ⁻¹' sᶜ))
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
[PROOFSTEP]
rw [tendsto_inf, tendsto_principal] at hx 
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
this : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
⊢ ∃ x, Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
[PROOFSTEP]
refine' ⟨x, hx.1, fun h => _⟩
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
this : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
h : Tendsto (f ∘ x) atTop l
⊢ False
[PROOFSTEP]
rcases(hx.2.and (h hs)).exists with ⟨N, hnmem, hmem⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β
k : Filter α
l : Filter β
inst✝ : IsCountablyGenerated k
s : Set β
hs : s ∈ l
H : ¬s ∈ map f k
this : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ))
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
h : Tendsto (f ∘ x) atTop l
N : ℕ
hnmem : x N ∈ f ⁻¹' sᶜ
hmem : (f ∘ x) N ∈ s
⊢ False
[PROOFSTEP]
exact hnmem hmem
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
x : ι → α
f : Filter α
l : Filter ι
⊢ ¬Tendsto x l f ↔ ∃ s, s ∈ f ∧ ∃ᶠ (n : ι) in l, ¬x n ∈ s
[PROOFSTEP]
simp only [tendsto_iff_forall_eventually_mem, not_forall, exists_prop, Filter.Frequently, not_not]
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
⊢ (∃ᶠ (n : ι) in l, p n) ↔ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
[PROOFSTEP]
refine' ⟨fun h_freq => _, fun h_exists_freq => _⟩
[GOAL]
case refine'_1
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
⊢ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
[PROOFSTEP]
have : NeBot (l ⊓ 𝓟 {x : ι | p x}) := by simpa [neBot_iff, inf_principal_eq_bot]
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
⊢ NeBot (l ⊓ 𝓟 {x | p x})
[PROOFSTEP]
simpa [neBot_iff, inf_principal_eq_bot]
[GOAL]
case refine'_1
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
⊢ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
[PROOFSTEP]
obtain ⟨x, hx⟩ := exists_seq_tendsto (l ⊓ 𝓟 {x : ι | p x})
[GOAL]
case refine'_1.intro
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
x : ℕ → ι
hx : Tendsto x atTop (l ⊓ 𝓟 {x | p x})
⊢ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
[PROOFSTEP]
rw [tendsto_inf] at hx 
[GOAL]
case refine'_1.intro
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
x : ℕ → ι
hx : Tendsto x atTop l ∧ Tendsto x atTop (𝓟 {x | p x})
⊢ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
[PROOFSTEP]
cases' hx with hx_l hx_p
[GOAL]
case refine'_1.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
x : ℕ → ι
hx_l : Tendsto x atTop l
hx_p : Tendsto x atTop (𝓟 {x | p x})
⊢ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
[PROOFSTEP]
refine' ⟨x, hx_l, _⟩
[GOAL]
case refine'_1.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
x : ℕ → ι
hx_l : Tendsto x atTop l
hx_p : Tendsto x atTop (𝓟 {x | p x})
⊢ ∃ᶠ (n : ℕ) in atTop, p (x n)
[PROOFSTEP]
rw [tendsto_principal] at hx_p 
[GOAL]
case refine'_1.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_freq : ∃ᶠ (n : ι) in l, p n
this : NeBot (l ⊓ 𝓟 {x | p x})
x : ℕ → ι
hx_l : Tendsto x atTop l
hx_p : ∀ᶠ (a : ℕ) in atTop, x a ∈ {x | p x}
⊢ ∃ᶠ (n : ℕ) in atTop, p (x n)
[PROOFSTEP]
exact hx_p.frequently
[GOAL]
case refine'_2
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h_exists_freq : ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ᶠ (n : ι) in l, p n
[PROOFSTEP]
obtain ⟨x, hx_tendsto, hx_freq⟩ := h_exists_freq
[GOAL]
case refine'_2.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ᶠ (n : ι) in l, p n
[PROOFSTEP]
simp_rw [Filter.Frequently, Filter.Eventually] at hx_freq ⊢
[GOAL]
case refine'_2.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ¬{x_1 | ¬p (x x_1)} ∈ atTop
⊢ ¬{x | ¬p x} ∈ l
[PROOFSTEP]
have : {n : ℕ | ¬p (x n)} = {n | x n ∈ {y | ¬p y}} := rfl
[GOAL]
case refine'_2.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ¬{x_1 | ¬p (x x_1)} ∈ atTop
this : {n | ¬p (x n)} = {n | x n ∈ {y | ¬p y}}
⊢ ¬{x | ¬p x} ∈ l
[PROOFSTEP]
rw [this, ← mem_map'] at hx_freq 
[GOAL]
case refine'_2.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ¬{y | ¬p y} ∈ map (fun n => x n) atTop
this : {n | ¬p (x n)} = {n | x n ∈ {y | ¬p y}}
⊢ ¬{x | ¬p x} ∈ l
[PROOFSTEP]
exact mt (@hx_tendsto _) hx_freq
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)
[PROOFSTEP]
have : (∀ᶠ n in l, p n) ↔ ¬∃ᶠ n in l, ¬p n := by
  rw [not_frequently]
  simp_rw [not_not]
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ¬∃ᶠ (n : ι) in l, ¬p n
[PROOFSTEP]
rw [not_frequently]
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ∀ᶠ (x : ι) in l, ¬¬p x
[PROOFSTEP]
simp_rw [not_not]
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
this : (∀ᶠ (n : ι) in l, p n) ↔ ¬∃ᶠ (n : ι) in l, ¬p n
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)
[PROOFSTEP]
rw [this, frequently_iff_seq_frequently]
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
this : (∀ᶠ (n : ι) in l, p n) ↔ ¬∃ᶠ (n : ι) in l, ¬p n
⊢ (¬∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, ¬p (x n)) ↔
    ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)
[PROOFSTEP]
push_neg
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
this : (∀ᶠ (n : ι) in l, p n) ↔ ¬∃ᶠ (n : ι) in l, ¬p n
⊢ (∀ (x : ℕ → ι), Tendsto x atTop l → ¬∃ᶠ (n : ℕ) in atTop, ¬p (x n)) ↔
    ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)
[PROOFSTEP]
simp_rw [not_frequently, not_not]
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : Tendsto x atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))
[PROOFSTEP]
rw [tendsto_iff_seq_tendsto] at h_tendsto 
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : ∀ (x_1 : ℕ → ℕ), Tendsto x_1 atTop atTop → Tendsto (x ∘ x_1) atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))
[PROOFSTEP]
choose ns hge hns using frequently_atTop.1 h
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : ∀ (x_1 : ℕ → ℕ), Tendsto x_1 atTop atTop → Tendsto (x ∘ x_1) atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
ns : ℕ → ℕ
hge : ∀ (a : ℕ), ns a ≥ a
hns : ∀ (a : ℕ), p (x (ns a))
⊢ ∃ ns, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))
[PROOFSTEP]
exact ⟨ns, h_tendsto ns (tendsto_atTop_mono hge tendsto_id), hns⟩
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h : ∃ᶠ (n : ι) in l, p n
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)
[PROOFSTEP]
rw [frequently_iff_seq_frequently] at h 
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
h : ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)
[PROOFSTEP]
obtain ⟨x, hx_tendsto, hx_freq⟩ := h
[GOAL]
case intro.intro
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)
[PROOFSTEP]
obtain ⟨n_to_n, h_tendsto, h_freq⟩ := subseq_forall_of_frequently hx_tendsto hx_freq
[GOAL]
case intro.intro.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
ι : Type u_6
l : Filter ι
p : ι → Prop
hl : IsCountablyGenerated l
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ∃ᶠ (n : ℕ) in atTop, p (x n)
n_to_n : ℕ → ℕ
h_tendsto : Tendsto (fun n => x (n_to_n n)) atTop l
h_freq : ∀ (n : ℕ), p (x (n_to_n n))
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)
[PROOFSTEP]
exact ⟨x ∘ n_to_n, h_tendsto, h_freq⟩
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
ι : Type u_7
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n => x (ns (ms n))) atTop f
⊢ Tendsto x l f
[PROOFSTEP]
by_contra h
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
ι : Type u_7
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n => x (ns (ms n))) atTop f
h : ¬Tendsto x l f
⊢ False
[PROOFSTEP]
obtain ⟨s, hs, hfreq⟩ : ∃ s ∈ f, ∃ᶠ n in l, x n ∉ s := by rwa [not_tendsto_iff_exists_frequently_nmem] at h 
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
ι : Type u_7
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n => x (ns (ms n))) atTop f
h : ¬Tendsto x l f
⊢ ∃ s, s ∈ f ∧ ∃ᶠ (n : ι) in l, ¬x n ∈ s
[PROOFSTEP]
rwa [not_tendsto_iff_exists_frequently_nmem] at h 
[GOAL]
case intro.intro
ι✝ : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
ι : Type u_7
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n => x (ns (ms n))) atTop f
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
⊢ False
[PROOFSTEP]
obtain ⟨y, hy_tendsto, hy_freq⟩ := exists_seq_forall_of_frequently hfreq
[GOAL]
case intro.intro.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
ι : Type u_7
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n => x (ns (ms n))) atTop f
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
⊢ False
[PROOFSTEP]
specialize hxy y hy_tendsto
[GOAL]
case intro.intro.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
ι : Type u_7
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
hxy : ∃ ms, Tendsto (fun n => x (y (ms n))) atTop f
⊢ False
[PROOFSTEP]
obtain ⟨ms, hms_tendsto⟩ := hxy
[GOAL]
case intro.intro.intro.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
ι : Type u_7
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : Tendsto (fun n => x (y (ms n))) atTop f
⊢ False
[PROOFSTEP]
specialize hms_tendsto hs
[GOAL]
case intro.intro.intro.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
ι : Type u_7
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : s ∈ map (fun n => x (y (ms n))) atTop
⊢ False
[PROOFSTEP]
rw [mem_map] at hms_tendsto 
[GOAL]
case intro.intro.intro.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
ι : Type u_7
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
⊢ False
[PROOFSTEP]
have hms_freq : ∀ n : ℕ, x (y (ms n)) ∉ s := fun n => hy_freq (ms n)
[GOAL]
case intro.intro.intro.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
ι : Type u_7
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
⊢ False
[PROOFSTEP]
have h_empty : (fun n : ℕ => x (y (ms n))) ⁻¹' s = ∅ := by
  ext1 n
  simp only [Set.mem_preimage, Set.mem_empty_iff_false, iff_false_iff]
  exact hms_freq n
[GOAL]
ι✝ : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
ι : Type u_7
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
⊢ (fun n => x (y (ms n))) ⁻¹' s = ∅
[PROOFSTEP]
ext1 n
[GOAL]
case h
ι✝ : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
ι : Type u_7
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
n : ℕ
⊢ n ∈ (fun n => x (y (ms n))) ⁻¹' s ↔ n ∈ ∅
[PROOFSTEP]
simp only [Set.mem_preimage, Set.mem_empty_iff_false, iff_false_iff]
[GOAL]
case h
ι✝ : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
ι : Type u_7
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
n : ℕ
⊢ ¬x (y (ms n)) ∈ s
[PROOFSTEP]
exact hms_freq n
[GOAL]
case intro.intro.intro.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
ι : Type u_7
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : (fun n => x (y (ms n))) ⁻¹' s ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
h_empty : (fun n => x (y (ms n))) ⁻¹' s = ∅
⊢ False
[PROOFSTEP]
rw [h_empty] at hms_tendsto 
[GOAL]
case intro.intro.intro.intro.intro
ι✝ : Type u_1
ι' : Type u_2
α✝ : Type u_3
β : Type u_4
γ : Type u_5
α : Type u_6
ι : Type u_7
x : ι → α
f : Filter α
l : Filter ι
inst✝ : IsCountablyGenerated l
h : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, ¬x n ∈ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), ¬x (y n) ∈ s
ms : ℕ → ℕ
hms_tendsto : ∅ ∈ atTop
hms_freq : ∀ (n : ℕ), ¬x (y (ms n)) ∈ s
h_empty : (fun n => x (y (ms n))) ⁻¹' s = ∅
⊢ False
[PROOFSTEP]
exact empty_not_mem atTop hms_tendsto
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
[PROOFSTEP]
obtain ⟨B, h⟩ := f.exists_antitone_basis
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
[PROOFSTEP]
have : ∀ N, ∃ n ≥ N, u n ∈ B N := fun N => Filter.inf_map_atTop_neBot_iff.mp hx _ (h.1.mem_of_mem trivial) N
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
this : ∀ (N : ℕ), ∃ n, n ≥ N ∧ u n ∈ B N
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
[PROOFSTEP]
choose φ hφ using this
[GOAL]
case intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
[PROOFSTEP]
cases' forall_and.mp hφ with φ_ge φ_in
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
[PROOFSTEP]
have lim_uφ : Tendsto (u ∘ φ) atTop f := h.tendsto φ_in
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
lim_uφ : Tendsto (u ∘ φ) atTop f
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
[PROOFSTEP]
have lim_φ : Tendsto φ atTop atTop := tendsto_atTop_mono φ_ge tendsto_id
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
lim_uφ : Tendsto (u ∘ φ) atTop f
lim_φ : Tendsto φ atTop atTop
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
[PROOFSTEP]
obtain ⟨ψ, hψ, hψφ⟩ : ∃ ψ : ℕ → ℕ, StrictMono ψ ∧ StrictMono (φ ∘ ψ)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
lim_uφ : Tendsto (u ∘ φ) atTop f
lim_φ : Tendsto φ atTop atTop
⊢ ∃ ψ, StrictMono ψ ∧ StrictMono (φ ∘ ψ)
case intro.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
lim_uφ : Tendsto (u ∘ φ) atTop f
lim_φ : Tendsto φ atTop atTop
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψφ : StrictMono (φ ∘ ψ)
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
[PROOFSTEP]
exact strictMono_subseq_of_tendsto_atTop lim_φ
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : Filter α
inst✝ : IsCountablyGenerated f
u : ℕ → α
hx : NeBot (f ⊓ map u atTop)
B : ℕ → Set α
h : HasAntitoneBasis f B
φ : ℕ → ℕ
hφ : ∀ (N : ℕ), φ N ≥ N ∧ u (φ N) ∈ B N
φ_ge : ∀ (x : ℕ), φ x ≥ x
φ_in : ∀ (x : ℕ), u (φ x) ∈ B x
lim_uφ : Tendsto (u ∘ φ) atTop f
lim_φ : Tendsto φ atTop atTop
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψφ : StrictMono (φ ∘ ψ)
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
[PROOFSTEP]
exact ⟨φ ∘ ψ, hψφ, lim_uφ.comp hψ.tendsto_atTop⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β✝ : Type u_4
γ : Type u_5
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x => x ∈ s i
inst✝ : DecidablePred fun x => x ∈ ⋃ (i : ι), s i
hs : Monotone s
f g : (a : α) → β a
a : α
⊢ ∀ᶠ (i : ι) in atTop, Set.piecewise (s i) f g a = Set.piecewise (⋃ (i : ι), s i) f g a
[PROOFSTEP]
rcases em (∃ i, a ∈ s i) with ⟨i, hi⟩ | ha
[GOAL]
case inl.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β✝ : Type u_4
γ : Type u_5
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x => x ∈ s i
inst✝ : DecidablePred fun x => x ∈ ⋃ (i : ι), s i
hs : Monotone s
f g : (a : α) → β a
a : α
i : ι
hi : a ∈ s i
⊢ ∀ᶠ (i : ι) in atTop, Set.piecewise (s i) f g a = Set.piecewise (⋃ (i : ι), s i) f g a
[PROOFSTEP]
refine (eventually_ge_atTop i).mono fun j hij ↦ ?_
[GOAL]
case inl.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β✝ : Type u_4
γ : Type u_5
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x => x ∈ s i
inst✝ : DecidablePred fun x => x ∈ ⋃ (i : ι), s i
hs : Monotone s
f g : (a : α) → β a
a : α
i : ι
hi : a ∈ s i
j : ι
hij : i ≤ j
⊢ Set.piecewise (s j) f g a = Set.piecewise (⋃ (i : ι), s i) f g a
[PROOFSTEP]
simp only [Set.piecewise_eq_of_mem, hs hij hi, subset_iUnion _ _ hi]
[GOAL]
case inr
ι : Type u_1
ι' : Type u_2
α : Type u_3
β✝ : Type u_4
γ : Type u_5
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x => x ∈ s i
inst✝ : DecidablePred fun x => x ∈ ⋃ (i : ι), s i
hs : Monotone s
f g : (a : α) → β a
a : α
ha : ¬∃ i, a ∈ s i
⊢ ∀ᶠ (i : ι) in atTop, Set.piecewise (s i) f g a = Set.piecewise (⋃ (i : ι), s i) f g a
[PROOFSTEP]
refine eventually_of_forall fun i ↦ ?_
[GOAL]
case inr
ι : Type u_1
ι' : Type u_2
α : Type u_3
β✝ : Type u_4
γ : Type u_5
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x => x ∈ s i
inst✝ : DecidablePred fun x => x ∈ ⋃ (i : ι), s i
hs : Monotone s
f g : (a : α) → β a
a : α
ha : ¬∃ i, a ∈ s i
i : ι
⊢ Set.piecewise (s i) f g a = Set.piecewise (⋃ (i : ι), s i) f g a
[PROOFSTEP]
simp only [Set.piecewise_eq_of_not_mem, not_exists.1 ha i, mt mem_iUnion.1 ha]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β✝ : Type u_4
γ : Type u_5
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x => x ∈ s i
inst✝ : DecidablePred fun x => x ∈ ⋂ (i : ι), s i
hs : Antitone s
f g : (a : α) → β a
a : α
⊢ ∀ᶠ (i : ι) in atTop, Set.piecewise (s i) f g a = Set.piecewise (⋂ (i : ι), s i) f g a
[PROOFSTEP]
classical
convert ← (compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a using 3
· convert congr_fun (Set.piecewise_compl (s _) g f) a
· simp only [(· ∘ ·), ← compl_iInter, Set.piecewise_compl]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β✝ : Type u_4
γ : Type u_5
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x => x ∈ s i
inst✝ : DecidablePred fun x => x ∈ ⋂ (i : ι), s i
hs : Antitone s
f g : (a : α) → β a
a : α
⊢ ∀ᶠ (i : ι) in atTop, Set.piecewise (s i) f g a = Set.piecewise (⋂ (i : ι), s i) f g a
[PROOFSTEP]
convert ← (compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a using 3
[GOAL]
case h.e'_2.h.h.e'_2
ι : Type u_1
ι' : Type u_2
α : Type u_3
β✝ : Type u_4
γ : Type u_5
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x => x ∈ s i
inst✝ : DecidablePred fun x => x ∈ ⋂ (i : ι), s i
hs : Antitone s
f g : (a : α) → β a
a : α
x✝ : ι
⊢ Set.piecewise ((compl ∘ s) x✝) g f a = Set.piecewise (s x✝) f g a
[PROOFSTEP]
convert congr_fun (Set.piecewise_compl (s _) g f) a
[GOAL]
case h.e'_2.h.h.e'_3
ι : Type u_1
ι' : Type u_2
α : Type u_3
β✝ : Type u_4
γ : Type u_5
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x => x ∈ s i
inst✝ : DecidablePred fun x => x ∈ ⋂ (i : ι), s i
hs : Antitone s
f g : (a : α) → β a
a : α
x✝ : ι
⊢ Set.piecewise (⋃ (i : ι), (compl ∘ s) i) g f a = Set.piecewise (⋂ (i : ι), s i) f g a
[PROOFSTEP]
simp only [(· ∘ ·), ← compl_iInter, Set.piecewise_compl]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
⊢ Filter.map (fun s => ∏ i in s, f (g i)) atTop = Filter.map (fun s => ∏ i in s, f i) atTop
[PROOFSTEP]
haveI := Classical.decEq β
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
⊢ Filter.map (fun s => ∏ i in s, f (g i)) atTop = Filter.map (fun s => ∏ i in s, f i) atTop
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
⊢ Filter.map (fun s => ∏ i in s, f (g i)) atTop ≤ Filter.map (fun s => ∏ i in s, f i) atTop
[PROOFSTEP]
refine' map_atTop_finset_prod_le_of_prod_eq fun s => _
[GOAL]
case a
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
⊢ Filter.map (fun s => ∏ i in s, f i) atTop ≤ Filter.map (fun s => ∏ i in s, f (g i)) atTop
[PROOFSTEP]
refine' map_atTop_finset_prod_le_of_prod_eq fun s => _
[GOAL]
case a
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
⊢ ∃ v, ∀ (v' : Finset γ), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x in u', f x = ∏ b in v', f (g b)
[PROOFSTEP]
refine' ⟨s.preimage g (hg.injOn _), fun t ht => _⟩
[GOAL]
case a
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
⊢ ∃ u', s ⊆ u' ∧ ∏ x in u', f x = ∏ b in t, f (g b)
[PROOFSTEP]
refine' ⟨t.image g ∪ s, Finset.subset_union_right _ _, _⟩
[GOAL]
case a
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
⊢ ∏ x in Finset.image g t ∪ s, f x = ∏ b in t, f (g b)
[PROOFSTEP]
rw [← Finset.prod_image (hg.injOn _)]
[GOAL]
case a
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
⊢ ∏ x in Finset.image g t ∪ s, f x = ∏ x in Finset.image (fun x => g x) t, f x
[PROOFSTEP]
refine' (prod_subset (subset_union_left _ _) _).symm
[GOAL]
case a
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
⊢ ∀ (x : β), x ∈ Finset.image g t ∪ s → ¬x ∈ Finset.image g t → f x = 1
[PROOFSTEP]
simp only [Finset.mem_union, Finset.mem_image]
[GOAL]
case a
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
⊢ ∀ (x : β), (∃ a, a ∈ t ∧ g a = x) ∨ x ∈ s → (¬∃ a, a ∈ t ∧ g a = x) → f x = 1
[PROOFSTEP]
refine' fun y hy hyt => hf y (mt _ hyt)
[GOAL]
case a
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
y : β
hy : (∃ a, a ∈ t ∧ g a = y) ∨ y ∈ s
hyt : ¬∃ a, a ∈ t ∧ g a = y
⊢ y ∈ Set.range g → ∃ a, a ∈ t ∧ g a = y
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case a.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
x : γ
hy : (∃ a, a ∈ t ∧ g a = g x) ∨ g x ∈ s
hyt : ¬∃ a, a ∈ t ∧ g a = g x
⊢ ∃ a, a ∈ t ∧ g a = g x
[PROOFSTEP]
exact ⟨x, ht (Finset.mem_preimage.2 <| hy.resolve_left hyt), rfl⟩
[GOAL]
case a
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset γ
⊢ ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x in u', f (g x) = ∏ b in v', f b
[PROOFSTEP]
refine' ⟨s.image g, fun t ht => _⟩
[GOAL]
case a
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset γ
t : Finset β
ht : Finset.image g s ⊆ t
⊢ ∃ u', s ⊆ u' ∧ ∏ x in u', f (g x) = ∏ b in t, f b
[PROOFSTEP]
simp only [← prod_preimage _ _ (hg.injOn _) _ fun x _ => hf x]
[GOAL]
case a
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset γ
t : Finset β
ht : Finset.image g s ⊆ t
⊢ ∃ u', s ⊆ u' ∧ ∏ x in u', f (g x) = ∏ x in Finset.preimage t g (_ : InjOn g (g ⁻¹' ↑t)), f (g x)
[PROOFSTEP]
exact ⟨_, (image_subset_iff_subset_preimage _).1 ht, rfl⟩
