awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderInf α
inst_3 : InfConvergenceClass α
f : ι → α
h_anti : Antitone f
hbdd : BddBelow (range f)
⊢ Tendsto f atTop (𝓝 (⨅ (i : ι), f i))

Tactic:
convert! tendsto_atBot_ciSup h_anti.dual hbdd.dual using 1

Premises used: tendsto_atBot_ciSup, Antitone.dual, BddBelow.dual
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : CompleteLattice α
inst_3 : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
⊢ Tendsto f atTop (𝓝 (⨆ (i : ι), f i))

Tactic:
tendsto_atTop_ciSup h_mono (OrderTop.bddAbove _)

Premises used: tendsto_atTop_ciSup, OrderTop.bddAbove
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : CompleteLattice α
inst_3 : SupConvergenceClass α
f : ι → α
h_anti : Antitone f
⊢ Tendsto f atBot (𝓝 (⨆ (i : ι), f i))

Tactic:
tendsto_atBot_ciSup h_anti (OrderTop.bddAbove _)

Premises used: tendsto_atBot_ciSup, OrderTop.bddAbove
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : CompleteLattice α
inst_3 : InfConvergenceClass α
f : ι → α
h_mono : Monotone f
⊢ Tendsto f atBot (𝓝 (⨅ (i : ι), f i))

Tactic:
tendsto_atBot_ciInf h_mono (OrderBot.bddBelow _)

Premises used: tendsto_atBot_ciInf, OrderBot.bddBelow
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : CompleteLattice α
inst_3 : InfConvergenceClass α
f : ι → α
h_anti : Antitone f
⊢ Tendsto f atTop (𝓝 (⨅ (i : ι), f i))

Tactic:
tendsto_atTop_ciInf h_anti (OrderBot.bddBelow _)

Premises used: tendsto_atTop_ciInf, OrderBot.bddBelow
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SupConvergenceClass α
inst_5 : SupConvergenceClass β
tendsto_coe_atTop_isLUB :
  ∀ (a : α × β) (s : Set (α × β)),
    IsLUB s a → Tendsto (α := { x : α × β // x ∈ s }) (Subtype.val (p := fun (x : α × β) ↦ x ∈ s)) atTop (𝓝 a)
⊢ SupConvergenceClass (α × β)

Tactic:
constructor
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SupConvergenceClass α
inst_5 : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB s (a, b)
⊢ IsLUB (range (s.restrict (π := fun (a : α × β) ↦ α) fst)) (a, b).1 ∧
    IsLUB (range (s.restrict (π := fun (a : α × β) ↦ β) snd)) (a, b).2

Tactic:
rw [isLUB_prod, ← range_restrict, ← range_restrict] at h

Premises used: Set.range_restrict, isLUB_prod
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SupConvergenceClass α
inst_5 : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h :
  IsLUB (range (s.restrict (π := fun (a : α × β) ↦ α) fst)) (a, b).1 ∧
    IsLUB (range (s.restrict (π := fun (a : α × β) ↦ β) snd)) (a, b).2
⊢ Tendsto (fun (x : (↑s : Type (max u_1 u_2))) ↦ (↑x : α × β).1) atTop (𝓝 a)

Tactic:
have A : Tendsto (fun x : s => (x : α × β).1) atTop (𝓝 a) :=
    tendsto_atTop_isLUB (monotone_fst.restrict s) h.1
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SupConvergenceClass α
inst_5 : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h :
  IsLUB (range (s.restrict (π := fun (a : α × β) ↦ α) fst)) (a, b).1 ∧
    IsLUB (range (s.restrict (π := fun (a : α × β) ↦ β) snd)) (a, b).2
A : Tendsto (fun (x : (↑s : Type (max u_1 u_2))) ↦ (↑x : α × β).1) atTop (𝓝 a)
⊢ Tendsto (fun (x : (↑s : Type (max u_1 u_2))) ↦ (↑x : α × β).2) atTop (𝓝 b)

Tactic:
have B : Tendsto (fun x : s => (x : α × β).2) atTop (𝓝 b) :=
    tendsto_atTop_isLUB (monotone_snd.restrict s) h.2
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SupConvergenceClass α
inst_5 : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h :
  IsLUB (range (s.restrict (π := fun (a : α × β) ↦ α) fst)) (a, b).1 ∧
    IsLUB (range (s.restrict (π := fun (a : α × β) ↦ β) snd)) (a, b).2
A : Tendsto (fun (x : (↑s : Type (max u_1 u_2))) ↦ (↑x : α × β).1) atTop (𝓝 a)
B : Tendsto (fun (x : (↑s : Type (max u_1 u_2))) ↦ (↑x : α × β).2) atTop (𝓝 b)
⊢ Tendsto (α := { x : α × β // x ∈ s }) (Subtype.val (p := fun (x : α × β) ↦ x ∈ s)) atTop (𝓝 (a, b))

Tactic:
A.prodMk_nhds B

Premises used: Set.Mem, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SupConvergenceClass α
inst_5 : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h :
  IsLUB (range (s.restrict (π := fun (a : α × β) ↦ α) fst)) (a, b).1 ∧
    IsLUB (range (s.restrict (π := fun (a : α × β) ↦ β) snd)) (a, b).2
A : Tendsto (fun (x : (↑s : Type (max u_1 u_2))) ↦ (↑x : α × β).1) atTop (𝓝 a)
B : Tendsto (fun (x : (↑s : Type (max u_1 u_2))) ↦ (↑x : α × β).2) atTop (𝓝 b)
⊢ Tendsto (α := { x : α × β // x ∈ s }) (Subtype.val (p := fun (x : α × β) ↦ x ∈ s)) atTop (𝓝 (a, b))

Tactic:
exact A.prodMk_nhds B

Premises used: Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : InfConvergenceClass α
inst_5 : InfConvergenceClass β
⊢ InfConvergenceClass (α × β)

Tactic:
show InfConvergenceClass (αᵒᵈ × βᵒᵈ)ᵒᵈ from OrderDual.infConvergenceClass

Premises used: setOf, OrderDual.infConvergenceClass, OrderDual
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α_1 : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), SupConvergenceClass.{u_4} (α i)
⊢ SupConvergenceClass ((i : ι) → α i)

Tactic:
⟨fun f s h => ?_⟩

Premises used: SupConvergenceClass.mk
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α_1 : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), SupConvergenceClass.{u_4} (α i)
refine :
  ∀ (f : (i : ι) → α i) (s : Set ((i : ι) → α i)) (h : IsLUB s f),
    Tendsto (α := { x : (i : ι) → α i // x ∈ s }) (Subtype.val (p := fun (x : (i : ι) → α i) ↦ x ∈ s)) atTop (𝓝 f)
⊢ SupConvergenceClass ((i : ι) → α i)

Tactic:
refine ⟨fun f s h => ?_⟩
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α_1 : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), SupConvergenceClass.{u_4} (α i)
f : (i : ι) → α i
s : Set ((i : ι) → α i)
h : IsLUB s f
⊢ ∀ (a : ι), IsLUB (range (s.restrict (π := fun (a_1 : (x : ι) → α x) ↦ α a) (eval (β := α) a))) (f a)

Tactic:
simp only [isLUB_pi, ← range_restrict] at h

Premises used: Set.range_restrict, isLUB_pi
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α_1 : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), SupConvergenceClass.{u_4} (α i)
f : (i : ι) → α i
s : Set ((i : ι) → α i)
h : ∀ (a : ι), IsLUB (range (s.restrict (π := fun (a_1 : (x : ι) → α x) ↦ α a) (eval (β := α) a))) (f a)
⊢ Tendsto (α := { x : (i : ι) → α i // x ∈ s }) (Subtype.val (p := fun (x : (i : ι) → α i) ↦ x ∈ s)) atTop (𝓝 f)

Tactic:
tendsto_pi_nhds.2 fun i => tendsto_atTop_isLUB ((monotone_eval _).restrict _) (h i)

Premises used: Iff.mpr, Function.monotone_eval, tendsto_pi_nhds, Monotone.restrict, tendsto_atTop_isLUB
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α_1 : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), SupConvergenceClass.{u_4} (α i)
f : (i : ι) → α i
s : Set ((i : ι) → α i)
h : ∀ (a : ι), IsLUB (range (s.restrict (π := fun (a_1 : (x : ι) → α x) ↦ α a) (eval (β := α) a))) (f a)
⊢ Tendsto (α := { x : (i : ι) → α i // x ∈ s }) (Subtype.val (p := fun (x : (i : ι) → α i) ↦ x ∈ s)) atTop (𝓝 f)

Tactic:
exact tendsto_pi_nhds.2 fun i => tendsto_atTop_isLUB ((monotone_eval _).restrict _) (h i)

Premises used: Iff.mpr, Function.monotone_eval, tendsto_pi_nhds, Monotone.restrict, tendsto_atTop_isLUB
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α_1 : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), InfConvergenceClass.{u_4} (α i)
⊢ InfConvergenceClass ((i : ι) → α i)

Tactic:
show InfConvergenceClass (∀ i, (α i)ᵒᵈ)ᵒᵈ from OrderDual.infConvergenceClass

Premises used: iInf, Set.Mem, setOf, OrderDual.infConvergenceClass, OrderDual
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : SupConvergenceClass α
⊢ SupConvergenceClass (ι → α)

Tactic:
supConvergenceClass

Premises used: Pi.supConvergenceClass
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : InfConvergenceClass α
⊢ InfConvergenceClass (ι → α)

Tactic:
Pi.infConvergenceClass

Premises used: Pi.infConvergenceClass
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι : Type u_3
α : Type u_4
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
f : ι → α
h_mono : Monotone f
⊢ Tendsto f atTop atTop ∨ ∃ (l : α), Tendsto f atTop (𝓝 l)

Tactic:
if H : BddAbove (range f) then Or.inr ⟨_, tendsto_atTop_ciSup h_mono H⟩
  else Or.inl <| tendsto_atTop_atTop_of_monotone' h_mono H

Premises used: iSup, tendsto_atTop_ciSup, dite, Filter.tendsto_atTop_atTop_of_monotone', Exists.intro, Or.inl, Or.inr
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι : Type u_3
α : Type u_4
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
f : ι → α
h_mono : Monotone f
⊢ Tendsto f atTop atTop ∨ ∃ (l : α), Tendsto f atTop (𝓝 l)

Tactic:
exact if H : BddAbove (range f) then Or.inr ⟨_, tendsto_atTop_ciSup h_mono H⟩
  else Or.inl <| tendsto_atTop_atTop_of_monotone' h_mono H

Premises used: BddAbove, Or.inl, Set.range, Or.inr
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι : Type u_3
α : Type u_4
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
f : ι → α
h_mono : Monotone f
⊢ Tendsto f atTop atTop ∨ ∃ (l : α), Tendsto f atTop (𝓝 l)

Tactic:
classical
  exact if H : BddAbove (range f) then Or.inr ⟨_, tendsto_atTop_ciSup h_mono H⟩
  else Or.inl <| tendsto_atTop_atTop_of_monotone' h_mono H

Premises used: BddAbove, Or.inl, Set.range, Or.inr
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι : Type u_3
α : Type u_4
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
f : ι → α
h_mono : Antitone f
⊢ Tendsto f atTop atBot ∨ ∃ (l : α), Tendsto f atTop (𝓝 l)

Tactic:
tendsto_atTop_of_monotone (α := αᵒᵈ) h_mono

Premises used: setOf, Filter.atBot, Set.Iic, OrderDual, tendsto_atTop_of_monotone
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι : Type u_3
α : Type u_4
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
f : ι → α
h_mono : Monotone f
⊢ Tendsto f atBot atBot ∨ ∃ (l : α), Tendsto f atBot (𝓝 l)

Tactic:
tendsto_atTop_of_monotone (ι := ιᵒᵈ) (α := αᵒᵈ) h_mono.dual

Premises used: setOf, Monotone.dual, Filter.atBot, Set.Iic, OrderDual, tendsto_atTop_of_monotone
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι : Type u_3
α : Type u_4
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
f : ι → α
h_mono : Antitone f
⊢ Tendsto f atBot atTop ∨ ∃ (l : α), Tendsto f atBot (𝓝 l)

Tactic:
tendsto_atTop_of_antitone (ι := ιᵒᵈ) (α := αᵒᵈ) h_mono.dual

Premises used: Set.Ici, setOf, Antitone.dual, Filter.atTop, Filter.atBot, Set.Iic, tendsto_atTop_of_antitone, OrderDual
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : SemilatticeSup ι₁
inst_1 : Preorder ι₂
inst_2 : Nonempty ι₁
inst_3 : TopologicalSpace α
inst_4 : ConditionallyCompleteLinearOrder α
inst_5 : OrderTopology α
inst_6 : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
mp : Tendsto f atTop (𝓝 l) → Tendsto (f ∘ φ) atTop (𝓝 l)
mpr : Tendsto (f ∘ φ) atTop (𝓝 l) → Tendsto f atTop (𝓝 l)
⊢ Tendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l)

Tactic:
constructor
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : SemilatticeSup ι₁
inst_1 : Preorder ι₂
inst_2 : Nonempty ι₁
inst_3 : TopologicalSpace α
inst_4 : ConditionallyCompleteLinearOrder α
inst_5 : OrderTopology α
inst_6 : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto f atTop (𝓝 l)
⊢ Tendsto (f ∘ φ) atTop (𝓝 l)

Tactic:
h.comp hg

Premises used: Filter.Tendsto.comp
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : SemilatticeSup ι₁
inst_1 : Preorder ι₂
inst_2 : Nonempty ι₁
inst_3 : TopologicalSpace α
inst_4 : ConditionallyCompleteLinearOrder α
inst_5 : OrderTopology α
inst_6 : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto f atTop (𝓝 l)
⊢ Tendsto (f ∘ φ) atTop (𝓝 l)

Tactic:
exact h.comp hg

Premises used: Filter.Tendsto.comp
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : SemilatticeSup ι₁
inst_1 : Preorder ι₂
inst_2 : Nonempty ι₁
inst_3 : TopologicalSpace α
inst_4 : ConditionallyCompleteLinearOrder α
inst_5 : OrderTopology α
inst_6 : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
mpr : ∀ (h' : Tendsto f atTop atTop), Tendsto f atTop (𝓝 l)
mpr₁ : ∀ (l' : α) (hl' : Tendsto f atTop (𝓝 l')), Tendsto f atTop (𝓝 l)
⊢ Tendsto f atTop (𝓝 l)

Tactic:
rcases tendsto_atTop_of_monotone hf with (h' | ⟨l', hl'⟩)

Premises used: tendsto_atTop_of_monotone
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : SemilatticeSup ι₁
inst_1 : Preorder ι₂
inst_2 : Nonempty ι₁
inst_3 : TopologicalSpace α
inst_4 : ConditionallyCompleteLinearOrder α
inst_5 : OrderTopology α
inst_6 : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
h' : Tendsto f atTop atTop
⊢ Tendsto f atTop (𝓝 l)

Tactic:
(not_tendsto_atTop_of_tendsto_nhds h (h'.comp hg)).elim

Premises used: False.elim, not_tendsto_atTop_of_tendsto_nhds, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : SemilatticeSup ι₁
inst_1 : Preorder ι₂
inst_2 : Nonempty ι₁
inst_3 : TopologicalSpace α
inst_4 : ConditionallyCompleteLinearOrder α
inst_5 : OrderTopology α
inst_6 : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
h' : Tendsto f atTop atTop
⊢ Tendsto f atTop (𝓝 l)

Tactic:
exact (not_tendsto_atTop_of_tendsto_nhds h (h'.comp hg)).elim

Premises used: False.elim, not_tendsto_atTop_of_tendsto_nhds, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : SemilatticeSup ι₁
inst_1 : Preorder ι₂
inst_2 : Nonempty ι₁
inst_3 : TopologicalSpace α
inst_4 : ConditionallyCompleteLinearOrder α
inst_5 : OrderTopology α
inst_6 : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
l' : α
hl' mpr mpr₁ mpr₂ mpr₃ : Tendsto f atTop (𝓝 l')
⊢ Tendsto f atTop (𝓝 l)

Tactic:
rwa [tendsto_nhds_unique h (hl'.comp hg)]

Premises used: Filter.Tendsto.comp, tendsto_nhds_unique
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : SemilatticeSup ι₁
inst_1 : Preorder ι₂
inst_2 : Nonempty ι₁
inst_3 : TopologicalSpace α
inst_4 : ConditionallyCompleteLinearOrder α
inst_5 : OrderTopology α
inst_6 : NoMinOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Antitone f
hg : Tendsto φ atTop atTop
⊢ Tendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l)

Tactic:
tendsto_iff_tendsto_subseq_of_monotone (α := αᵒᵈ) hf hg

Premises used: tendsto_iff_tendsto_subseq_of_monotone, OrderDual
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderClosedTopology α
inst_3 : Preorder β
inst_4 : IsDirectedOrder β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
b : β
⊢ f b ≤ a

Tactic:
haveI : Nonempty β := Nonempty.intro b
  _root_.ge_of_tendsto ha ((eventually_ge_atTop b).mono fun _ hxy => hf hxy)

Premises used: ge_of_tendsto, Filter.Eventually.mono, Filter.eventually_ge_atTop
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderClosedTopology α
inst_3 : Preorder β
inst_4 : IsCodirectedOrder β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atBot (𝓝 a)
b : β
⊢ a ≤ f b

Tactic:
hf.dual.ge_of_tendsto ha b

Premises used: Monotone.ge_of_tendsto, Monotone.dual
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderClosedTopology α
inst_3 : Preorder β
inst_4 : IsDirectedOrder β
f : β → α
a : α
hf : Antitone f
ha : Tendsto f atTop (𝓝 a)
b : β
⊢ a ≤ f b

Tactic:
hf.dual_right.ge_of_tendsto ha b

Premises used: Antitone.dual_right, Monotone.ge_of_tendsto
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderClosedTopology α
inst_3 : Preorder β
inst_4 : IsCodirectedOrder β
f : β → α
a : α
hf : Antitone f
ha : Tendsto f atBot (𝓝 a)
b : β
⊢ f b ≤ a

Tactic:
hf.dual_right.le_of_tendsto ha b

Premises used: Antitone.dual_right, Monotone.le_of_tendsto
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderClosedTopology α
inst_3 : Preorder β
inst_4 : IsDirectedOrder β
inst_5 : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
left : a ∈ upperBounds (range f)
right : a ∈ lowerBounds (upperBounds (range f))
⊢ IsLUB (range f) a

Tactic:
constructor
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderClosedTopology α
inst_3 : Preorder β
inst_4 : IsDirectedOrder β
inst_5 : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
b : β
⊢ f b ≤ a

Tactic:
hf.ge_of_tendsto ha b

Premises used: Monotone.ge_of_tendsto
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderClosedTopology α
inst_3 : Preorder β
inst_4 : IsDirectedOrder β
inst_5 : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
b : β
⊢ f b ≤ a

Tactic:
exact hf.ge_of_tendsto ha b

Premises used: Monotone.ge_of_tendsto
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderClosedTopology α
inst_3 : Preorder β
inst_4 : IsDirectedOrder β
inst_5 : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ lowerBounds (upperBounds (range f))

Tactic:
fun _ hb => le_of_tendsto' ha fun x => hb (Set.mem_range_self x)

Premises used: Set.mem_range_self, lowerBounds, Set.Mem, setOf, le_of_tendsto'
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderClosedTopology α
inst_3 : Preorder β
inst_4 : IsDirectedOrder β
inst_5 : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ lowerBounds (upperBounds (range f))

Tactic:
exact fun _ hb => le_of_tendsto' ha fun x => hb (Set.mem_range_self x)

Premises used: le_of_tendsto'
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderClosedTopology α
inst_3 : Preorder β
inst_4 : IsCodirectedOrder β
inst_5 : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atBot (𝓝 a)
⊢ IsGLB (range f) a

Tactic:
isLUB_of_tendsto_atTop (α := αᵒᵈ) (β := βᵒᵈ) hf.dual ha

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, Monotone.dual, IsGreatest, IsGLB, OrderDual, isLUB_of_tendsto_atTop
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderClosedTopology α
inst_3 : Preorder β
inst_4 : IsCodirectedOrder β
inst_5 : Nonempty β
f : β → α
a : α
hf : Antitone f
ha : Tendsto f atBot (𝓝 a)
⊢ IsLUB (range f) a

Tactic:
isLUB_of_tendsto_atTop (α := α) (β := βᵒᵈ) hf.dual_left ha

Premises used: Antitone.dual_left, OrderDual, isLUB_of_tendsto_atTop
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderClosedTopology α
inst_3 : Preorder β
inst_4 : IsDirectedOrder β
inst_5 : Nonempty β
f : β → α
a : α
hf : Antitone f
ha : Tendsto f atTop (𝓝 a)
⊢ IsGLB (range f) a

Tactic:
isGLB_of_tendsto_atBot (α := α) (β := βᵒᵈ) hf.dual_left ha

Premises used: Antitone.dual_left, isGLB_of_tendsto_atBot, OrderDual
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : CompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : Nonempty β
inst_4 : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
⊢ Tendsto f atTop (𝓝 a) → iSup f = a

Tactic:
tendsto_nhds_unique (tendsto_atTop_iSup hf)

Premises used: tendsto_atTop_iSup, tendsto_nhds_unique
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
β : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : CompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : Nonempty β
inst_4 : SemilatticeSup β
f : β → α
a : α
hf : Antitone f
⊢ Tendsto f atTop (𝓝 a) → iInf f = a

Tactic:
tendsto_nhds_unique (tendsto_atTop_iInf hf)

Premises used: tendsto_atTop_iInf, tendsto_nhds_unique
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : Preorder ι₂
inst_1 : CompleteLattice α
l : Filter ι₁
inst_2 : l.NeBot
f : ι₂ → α
φ : ι₁ → ι₂
hf : Monotone f
hφ : Tendsto φ l atTop
⊢ Eq.{u_5 + 1} (α := α) (⨆ (i : ι₂), f i) (⨆ (i : ι₁), f (φ i))

Tactic:
le_antisymm
    (iSup_mono' fun i =>
      Exists.imp (fun j (hj : i ≤ φ j) => hf hj) (hφ.eventually <| eventually_ge_atTop i).exists)
    (iSup_mono' fun i => ⟨φ i, le_rfl⟩)

Premises used: le_rfl, iSup_mono', Exists.imp, Filter.Eventually.exists, le_antisymm, Filter.Tendsto.eventually, Exists.intro, Filter.eventually_ge_atTop