ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>NoMinOrder α<VAR>x : α<VAR>l : Filter β<VAR>l.NeBot<GOAL>¬Filter.Tendsto (fun x_1 => x) l Filter.atBot
<VAR>α : Type u_3<VAR>PartialOrder α<VAR>Nontrivial α<GOAL>Disjoint Filter.atBot Filter.atTop
<VAR>α : Type u_3<VAR>PartialOrder α<VAR>Nontrivial α<GOAL>Disjoint Filter.atTop Filter.atBot
<VAR>α : Type u_3<VAR>Nonempty α<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≤ x_1<GOAL>Filter.atTop.HasAntitoneBasis Set.Ici
<VAR>α : Type u_3<VAR>Nonempty α<VAR>SemilatticeSup α<GOAL>Filter.atTop.HasBasis (fun x => True) Set.Ici
<VAR>α : Type u_3<VAR>SemilatticeSup α<GOAL>Filter.atTop = Filter.generate (Set.range Set.Ici)
<VAR>α : Type u_3<VAR>SemilatticeSup α<VAR>a : α<GOAL>Filter.atTop.HasBasis (fun x => a ≤ x) Set.Ici
<VAR>α : Type u_3<VAR>Nonempty α<VAR>SemilatticeInf α<GOAL>Filter.atBot.HasBasis (fun x => True) Set.Iic
<VAR>α : Type u_3<VAR>SemilatticeInf α<VAR>a : α<GOAL>Filter.atBot.HasBasis (fun x => x ≤ a) Set.Iic
<VAR>α : Type u_3<VAR>Nonempty α<VAR>SemilatticeSup α<GOAL>Filter.atTop.NeBot
<VAR>α : Type u_3<VAR>Nonempty α<VAR>SemilatticeInf α<GOAL>Filter.atBot.NeBot
<VAR>α : Type u_3<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>s : Set α<GOAL>s ∈ Filter.atTop ↔ ∃ a, ∀ b ≥ a, b ∈ s
<VAR>α : Type u_3<VAR>Nonempty α<VAR>SemilatticeInf α<VAR>s : Set α<GOAL>s ∈ Filter.atBot ↔ ∃ a, ∀ b ≤ a, b ∈ s
<VAR>α : Type u_3<VAR>SemilatticeSup α<VAR>Nonempty α<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in Filter.atTop, p x) ↔ ∃ a, ∀ b ≥ a, p b
<VAR>α : Type u_3<VAR>SemilatticeInf α<VAR>Nonempty α<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in Filter.atBot, p x) ↔ ∃ a, ∀ b ≤ a, p b
<VAR>α : Type u_3<VAR>Preorder α<VAR>a : α<GOAL>∀ᶠ (x : α) in Filter.atTop, a ≤ x
<VAR>α : Type u_3<VAR>Preorder α<VAR>a : α<GOAL>∀ᶠ (x : α) in Filter.atBot, x ≤ a
<VAR>α : Type u_3<VAR>Preorder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>∀ᶠ (x : α) in Filter.atTop, a < x
<VAR>α : Type u_3<VAR>Preorder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>∀ᶠ (x : α) in Filter.atTop, x ≠ a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>NoMaxOrder β<VAR>f : α → β<VAR>l : Filter α<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>c : β<GOAL>∀ᶠ (x : α) in l, c < f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>c : β<GOAL>∀ᶠ (x : α) in l, c ≤ f x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>NoMaxOrder β<VAR>f : α → β<VAR>l : Filter α<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>c : β<GOAL>∀ᶠ (x : α) in l, f x ≠ c
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>NoMaxOrder β<VAR>f : α → β<VAR>l : Filter α<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>c : α<GOAL>∀ᶠ (x : α) in l, x ≠ c
<VAR>α : Type u_3<VAR>Preorder α<VAR>NoMinOrder α<VAR>a : α<GOAL>∀ᶠ (x : α) in Filter.atBot, x < a
<VAR>α : Type u_3<VAR>Preorder α<VAR>NoMinOrder α<VAR>a : α<GOAL>∀ᶠ (x : α) in Filter.atBot, x ≠ a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>NoMinOrder β<VAR>f : α → β<VAR>l : Filter α<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>c : β<GOAL>∀ᶠ (x : α) in l, f x < c
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>f : α → β<VAR>l : Filter α<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>c : β<GOAL>∀ᶠ (x : α) in l, f x ≤ c
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>NoMinOrder β<VAR>f : α → β<VAR>l : Filter α<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>c : β<GOAL>∀ᶠ (x : α) in l, f x ≠ c
<VAR>α : Type u_3<VAR>Preorder α<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in Filter.atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in Filter.atTop, p x
<VAR>α : Type u_3<VAR>Preorder α<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in Filter.atBot, ∀ y ≤ x, p y) ↔ ∀ᶠ (x : α) in Filter.atBot, p x
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>l : Filter α<VAR>p : β → Prop<VAR>f : α → β<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>h_evtl : ∀ᶠ (x : β) in Filter.atTop, p x<GOAL>∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>l : Filter α<VAR>p : β → Prop<VAR>f : α → β<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>h_evtl : ∀ᶠ (x : β) in Filter.atBot, p x<GOAL>∀ᶠ (x : α) in l, ∀ y ≤ f x, p y
<VAR>α : Type u_3<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>NoMaxOrder α<GOAL>Filter.atTop.HasBasis (fun x => True) Set.Ioi
<VAR>α : Type u_3<VAR>SemilatticeSup α<VAR>NoMaxOrder α<VAR>a : α<GOAL>Filter.atTop.HasBasis (fun x => a < x) Set.Ioi
<VAR>α : Type u_3<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>Countable α<GOAL>Filter.atTop.HasCountableBasis (fun x => True) Set.Ici
<VAR>α : Type u_3<VAR>Nonempty α<VAR>SemilatticeInf α<VAR>Countable α<GOAL>Filter.atBot.HasCountableBasis (fun x => True) Set.Iic
<VAR>α : Type u_3<VAR>Preorder α<VAR>a : α<VAR>ha : IsTop a<GOAL>Filter.atTop = 𝓟 (Set.Ici a)
<VAR>α : Type u_3<VAR>Preorder α<VAR>a : α<VAR>ha : IsBot a<GOAL>Filter.atBot = 𝓟 (Set.Iic a)
<VAR>α : Type u_6<VAR>PartialOrder α<VAR>OrderTop α<GOAL>Filter.atTop = pure ⊤
<VAR>α : Type u_6<VAR>PartialOrder α<VAR>OrderBot α<GOAL>Filter.atBot = pure ⊥
<VAR>α : Type u_6<VAR>Subsingleton α<VAR>Preorder α<GOAL>Filter.atTop = ⊤
<VAR>α : Type u_6<VAR>Subsingleton α<VAR>Preorder α<GOAL>Filter.atBot = ⊤
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>PartialOrder α<VAR>OrderTop α<VAR>f : α → β<GOAL>Filter.Tendsto f Filter.atTop (pure (f ⊤))
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>f : α → β<GOAL>Filter.Tendsto f Filter.atBot (pure (f ⊥))
<VAR>α : Type u_3<VAR>SemilatticeSup α<VAR>Nonempty α<VAR>p : α → Prop<VAR>h : ∀ᶠ (x : α) in Filter.atTop, p x<GOAL>∃ a, ∀ b ≥ a, p b
<VAR>α : Type u_3<VAR>SemilatticeInf α<VAR>Nonempty α<VAR>p : α → Prop<VAR>h : ∀ᶠ (x : α) in Filter.atBot, p x<GOAL>∃ a, ∀ b ≤ a, p b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>Nonempty α<VAR>r : α → β → Prop<GOAL>(∃ b, ∀ᶠ (a : α) in Filter.atTop, r a b) ↔ ∀ᶠ (a₀ : α) in Filter.atTop, ∃ b, ∀ a ≥ a₀, r a b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeInf α<VAR>Nonempty α<VAR>r : α → β → Prop<GOAL>(∃ b, ∀ᶠ (a : α) in Filter.atBot, r a b) ↔ ∀ᶠ (a₀ : α) in Filter.atBot, ∃ b, ∀ a ≤ a₀, r a b
<VAR>α : Type u_3<VAR>SemilatticeSup α<VAR>Nonempty α<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in Filter.atTop, p x) ↔ ∀ (a : α), ∃ b ≥ a, p b
<VAR>α : Type u_3<VAR>SemilatticeInf α<VAR>Nonempty α<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in Filter.atBot, p x) ↔ ∀ (a : α), ∃ b ≤ a, p b
<VAR>α : Type u_3<VAR>SemilatticeSup α<VAR>Nonempty α<VAR>NoMaxOrder α<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in Filter.atTop, p x) ↔ ∀ (a : α), ∃ b > a, p b
<VAR>α : Type u_3<VAR>SemilatticeInf α<VAR>Nonempty α<VAR>NoMinOrder α<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in Filter.atBot, p x) ↔ ∀ (a : α), ∃ b < a, p b
<VAR>α : Type u_3<VAR>SemilatticeSup α<VAR>Nonempty α<VAR>p : α → Prop<VAR>h : ∃ᶠ (x : α) in Filter.atTop, p x<VAR>a : α<GOAL>∃ b ≥ a, p b
<VAR>α : Type u_3<VAR>SemilatticeInf α<VAR>Nonempty α<VAR>p : α → Prop<VAR>h : ∃ᶠ (x : α) in Filter.atBot, p x<VAR>a : α<GOAL>∃ b ≤ a, p b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeSup α<VAR>f : α → β<GOAL>Filter.map f Filter.atTop = ⨅ a, 𝓟 (f '' {a' | a ≤ a'})
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Nonempty α<VAR>SemilatticeInf α<VAR>f : α → β<GOAL>Filter.map f Filter.atBot = ⨅ a, 𝓟 (f '' {a' | a' ≤ a})
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>m : α → β<VAR>f : Filter α<GOAL>Filter.Tendsto m f Filter.atTop ↔ ∀ (b : β), ∀ᶠ (a : α) in f, b ≤ m a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>m : α → β<VAR>f : Filter α<GOAL>Filter.Tendsto m f Filter.atBot ↔ ∀ (b : β), ∀ᶠ (a : α) in f, m a ≤ b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>l : Filter α<VAR>f₁ f₂ : α → β<VAR>h : f₁ ≤ᶠ[l] f₂<VAR>h₁ : Filter.Tendsto f₁ l Filter.atTop<GOAL>Filter.Tendsto f₂ l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>l : Filter α<VAR>f₁ f₂ : α → β<VAR>h : f₁ ≤ᶠ[l] f₂<GOAL>Filter.Tendsto f₂ l Filter.atBot → Filter.Tendsto f₁ l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>l : Filter α<VAR>f g : α → β<VAR>h : ∀ (n : α), f n ≤ g n<GOAL>Filter.Tendsto f l Filter.atTop → Filter.Tendsto g l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder β<VAR>l : Filter α<VAR>f g : α → β<VAR>h : ∀ (n : α), f n ≤ g n<GOAL>Filter.Tendsto g l Filter.atBot → Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>LinearOrder α<VAR>s : Set α<VAR>hs : ∀ (x : α), ∃ y ∈ s, x ≤ y<GOAL>Filter.atTop = Filter.generate (Set.Ici '' s)
<VAR>α : Type u_3<VAR>LinearOrder α<VAR>s : Set α<VAR>hs : ¬BddAbove s<GOAL>Filter.atTop = Filter.generate (Set.Ici '' s)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<GOAL>Filter.comap (⇑e) Filter.atTop = Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<GOAL>Filter.comap (⇑e) Filter.atBot = Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<GOAL>Filter.map (⇑e) Filter.atTop = Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<GOAL>Filter.map (⇑e) Filter.atBot = Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<GOAL>Filter.Tendsto (⇑e) Filter.atTop Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<GOAL>Filter.Tendsto (⇑e) Filter.atBot Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>l : Filter γ<VAR>f : γ → α<VAR>e : α ≃o β<GOAL>Filter.Tendsto (fun x => e (f x)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>l : Filter γ<VAR>f : γ → α<VAR>e : α ≃o β<GOAL>Filter.Tendsto (fun x => e (f x)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>Nonempty α<VAR>F : Filter β<VAR>u : α → β<GOAL>(F ⊓ Filter.map u Filter.atTop).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≥ N, u n ∈ U
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeInf α<VAR>Nonempty α<VAR>F : Filter β<VAR>u : α → β<GOAL>(F ⊓ Filter.map u Filter.atBot).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≤ N, u n ∈ U
<VAR>P : ℕ → Prop<VAR>h : ∀ (N : ℕ), ∃ n > N, P n<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
<VAR>P : ℕ → Prop<VAR>h : ∃ᶠ (n : ℕ) in Filter.atTop, P n<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
<VAR>P : ℕ → Prop<VAR>h : ∀ᶠ (n : ℕ) in Filter.atTop, P n<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
<VAR>P : ℕ → ℕ → Prop<VAR>h : ∀ (n : ℕ), ∃ᶠ (k : ℕ) in Filter.atTop, P n k<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
<VAR>P : ℕ → ℕ → Prop<VAR>h : ∀ (n : ℕ), ∀ᶠ (k : ℕ) in Filter.atTop, P n k<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
<VAR>P : ℕ → ℕ → Prop<VAR>h : ∀ (n : ℕ), ∃ N, ∀ k ≥ N, P n k<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
<VAR>p : ℕ → Prop<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hp : ∀ k < n, ∀ᶠ (a : ℕ) in Filter.atTop, p (n * a + k)<GOAL>∀ᶠ (a : ℕ) in Filter.atTop, p a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>Preorder β<VAR>u : α → β<VAR>h : Filter.Tendsto u Filter.atTop Filter.atTop<VAR>a : α<VAR>b : β<GOAL>∃ a' ≥ a, b ≤ u a'
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>Preorder β<VAR>u : α → β<VAR>h : Filter.Tendsto u Filter.atTop Filter.atBot<VAR>a : α<VAR>b : β<GOAL>∃ a' ≥ a, u a' ≤ b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>Preorder β<VAR>NoMaxOrder β<VAR>u : α → β<VAR>h : Filter.Tendsto u Filter.atTop Filter.atTop<VAR>a : α<VAR>b : β<GOAL>∃ a' ≥ a, b < u a'
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>Preorder β<VAR>NoMinOrder β<VAR>u : α → β<VAR>h : Filter.Tendsto u Filter.atTop Filter.atBot<VAR>a : α<VAR>b : β<GOAL>∃ a' ≥ a, u a' < b
<VAR>β : Type u_4<VAR>LinearOrder β<VAR>NoMaxOrder β<VAR>u : ℕ → β<VAR>hu : Filter.Tendsto u Filter.atTop Filter.atTop<VAR>N : ℕ<GOAL>∃ n ≥ N, ∀ k < n, u k < u n
<VAR>β : Type u_4<VAR>LinearOrder β<VAR>NoMinOrder β<VAR>u : ℕ → β<VAR>hu : Filter.Tendsto u Filter.atTop Filter.atBot<VAR>N : ℕ<GOAL>∃ n ≥ N, ∀ k < n, u n < u k
<VAR>β : Type u_4<VAR>LinearOrder β<VAR>NoMaxOrder β<VAR>u : ℕ → β<VAR>hu : Filter.Tendsto u Filter.atTop Filter.atTop<GOAL>∃ᶠ (n : ℕ) in Filter.atTop, ∀ k < n, u k < u n
<VAR>β : Type u_4<VAR>LinearOrder β<VAR>NoMinOrder β<VAR>u : ℕ → β<VAR>hu : Filter.Tendsto u Filter.atTop Filter.atBot<GOAL>∃ᶠ (n : ℕ) in Filter.atTop, ∀ k < n, u n < u k
<VAR>β : Type u_4<VAR>LinearOrder β<VAR>NoMaxOrder β<VAR>u : ℕ → β<VAR>hu : Filter.Tendsto u Filter.atTop Filter.atTop<GOAL>∃ φ, StrictMono φ ∧ StrictMono (u ∘ φ)
<VAR>u : ℕ → ℕ<VAR>hu : ∀ (n : ℕ), n ≤ u n<GOAL>∃ φ, StrictMono φ ∧ StrictMono (u ∘ φ)
<VAR>φ : ℕ → ℕ<VAR>h : StrictMono φ<GOAL>Filter.Tendsto φ Filter.atTop Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : ∀ᶠ (x : α) in l, 0 ≤ f x<VAR>hg : Filter.Tendsto g l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : ∀ᶠ (x : α) in l, f x ≤ 0<VAR>hg : Filter.Tendsto g l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : ∀ (x : α), 0 ≤ f x<VAR>hg : Filter.Tendsto g l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : ∀ (x : α), f x ≤ 0<VAR>hg : Filter.Tendsto g l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>hg : ∀ᶠ (x : α) in l, 0 ≤ g x<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>hg : ∀ᶠ (x : α) in l, g x ≤ 0<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>hg : ∀ (x : α), 0 ≤ g x<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>hg : ∀ (x : α), g x ≤ 0<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>hg : Filter.Tendsto g l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>hg : Filter.Tendsto g l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommMonoid β<VAR>l : Filter α<VAR>f : α → β<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>Filter.Tendsto (fun x => n • f x) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommMonoid β<VAR>l : Filter α<VAR>f : α → β<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>Filter.Tendsto (fun x => n • f x) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedCancelAddCommMonoid β<VAR>l : Filter α<VAR>f : α → β<VAR>C : β<VAR>hf : Filter.Tendsto (fun x => C + f x) l Filter.atTop<GOAL>Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedCancelAddCommMonoid β<VAR>l : Filter α<VAR>f : α → β<VAR>C : β<VAR>hf : Filter.Tendsto (fun x => C + f x) l Filter.atBot<GOAL>Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedCancelAddCommMonoid β<VAR>l : Filter α<VAR>f : α → β<VAR>C : β<VAR>hf : Filter.Tendsto (fun x => f x + C) l Filter.atTop<GOAL>Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedCancelAddCommMonoid β<VAR>l : Filter α<VAR>f : α → β<VAR>C : β<VAR>hf : Filter.Tendsto (fun x => f x + C) l Filter.atBot<GOAL>Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedCancelAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hC : ∀ᶠ (x : α) in l, f x ≤ C<VAR>h : Filter.Tendsto (fun x => f x + g x) l Filter.atTop<GOAL>Filter.Tendsto g l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedCancelAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hC : ∀ᶠ (x : α) in l, C ≤ f x<VAR>h : Filter.Tendsto (fun x => f x + g x) l Filter.atBot<GOAL>Filter.Tendsto g l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedCancelAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hC : ∀ (x : α), f x ≤ C<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atTop → Filter.Tendsto g l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedCancelAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hC : ∀ (x : α), C ≤ f x<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atBot → Filter.Tendsto g l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedCancelAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hC : ∀ᶠ (x : α) in l, g x ≤ C<VAR>h : Filter.Tendsto (fun x => f x + g x) l Filter.atTop<GOAL>Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedCancelAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hC : ∀ᶠ (x : α) in l, C ≤ g x<VAR>h : Filter.Tendsto (fun x => f x + g x) l Filter.atBot<GOAL>Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedCancelAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hC : ∀ (x : α), g x ≤ C<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atTop → Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedCancelAddCommMonoid β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hC : ∀ (x : α), C ≤ g x<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atBot → Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hf : ∀ᶠ (x : α) in l, C ≤ f x<VAR>hg : Filter.Tendsto g l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hf : ∀ᶠ (x : α) in l, f x ≤ C<VAR>hg : Filter.Tendsto g l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hf : ∀ (x : α), C ≤ f x<VAR>hg : Filter.Tendsto g l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hf : ∀ (x : α), f x ≤ C<VAR>hg : Filter.Tendsto g l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>hg : ∀ᶠ (x : α) in l, C ≤ g x<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>hg : ∀ᶠ (x : α) in l, g x ≤ C<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>hg : ∀ (x : α), C ≤ g x<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<VAR>l : Filter α<VAR>f g : α → β<VAR>C : β<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>hg : ∀ (x : α), g x ≤ C<GOAL>Filter.Tendsto (fun x => f x + g x) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<VAR>l : Filter α<VAR>f : α → β<VAR>C : β<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => C + f x) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<VAR>l : Filter α<VAR>f : α → β<VAR>C : β<VAR>hf : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => C + f x) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<VAR>l : Filter α<VAR>f : α → β<VAR>C : β<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x + C) l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<VAR>l : Filter α<VAR>f : α → β<VAR>C : β<VAR>hf : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x + C) l Filter.atBot
<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<GOAL>Filter.map Neg.neg Filter.atBot = Filter.atTop
<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<GOAL>Filter.map Neg.neg Filter.atTop = Filter.atBot
<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<GOAL>Filter.comap Neg.neg Filter.atBot = Filter.atTop
<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<GOAL>Filter.comap Neg.neg Filter.atTop = Filter.atBot
<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<GOAL>Filter.Tendsto Neg.neg Filter.atTop Filter.atBot
<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<GOAL>Filter.Tendsto Neg.neg Filter.atBot Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<VAR>l : Filter α<VAR>f : α → β<GOAL>Filter.Tendsto (fun x => -f x) l Filter.atTop ↔ Filter.Tendsto f l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedAddCommGroup β<VAR>l : Filter α<VAR>f : α → β<GOAL>Filter.Tendsto (fun x => -f x) l Filter.atBot ↔ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedSemiring α<VAR>l : Filter β<VAR>f g : β → α<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>hg : Filter.Tendsto g l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x * g x) l Filter.atTop
<VAR>α : Type u_3<VAR>OrderedSemiring α<GOAL>Filter.Tendsto (fun x => x * x) Filter.atTop Filter.atTop
<VAR>α : Type u_3<VAR>OrderedSemiring α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Filter.Tendsto (fun x => x ^ n) Filter.atTop Filter.atTop
<VAR>α : Type u_3<VAR>MonoidWithZero α<GOAL>(fun n => 0 ^ n) =ᶠ[Filter.atTop] fun x => 0
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedRing α<VAR>l : Filter β<VAR>f g : β → α<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>hg : Filter.Tendsto g l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x * g x) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedRing α<VAR>l : Filter β<VAR>f g : β → α<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>hg : Filter.Tendsto g l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x * g x) l Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>OrderedRing α<VAR>l : Filter β<VAR>f g : β → α<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>hg : Filter.Tendsto g l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x * g x) l Filter.atTop
<VAR>α : Type u_3<VAR>LinearOrderedAddCommGroup α<GOAL>Filter.Tendsto abs Filter.atTop Filter.atTop
<VAR>α : Type u_3<VAR>LinearOrderedAddCommGroup α<GOAL>Filter.Tendsto abs Filter.atBot Filter.atTop
<VAR>α : Type u_3<VAR>LinearOrderedAddCommGroup α<GOAL>Filter.comap abs Filter.atTop = Filter.atBot ⊔ Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedSemiring α<VAR>l : Filter β<VAR>f : β → α<VAR>c : α<VAR>hc : 0 < c<VAR>hf : Filter.Tendsto (fun x => c * f x) l Filter.atTop<GOAL>Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedSemiring α<VAR>l : Filter β<VAR>f : β → α<VAR>c : α<VAR>hc : 0 < c<VAR>hf : Filter.Tendsto (fun x => f x * c) l Filter.atTop<GOAL>Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>LinearOrderedSemiring α<VAR>n : ℕ<GOAL>Filter.Tendsto (fun x => x ^ n) Filter.atTop Filter.atTop ↔ n ≠ 0
<VAR>α : Type u_3<VAR>LinearOrderedRing α<VAR>n : ℕ<GOAL>¬Filter.Tendsto (fun x => x ^ n) Filter.atTop Filter.atBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : 0 < r<GOAL>Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : 0 < r<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : 0 < r<GOAL>Filter.Tendsto (fun x => f x / r) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop