awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLinearOrder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
if : ∀ (hb : BddAbove (range f)), Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)
if₁ : ∀ (hb : ¬BddAbove (range f)), Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)
if₂ : ∀ (hb : BddAbove (range f)), Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)
if₃ if₄ : ∀ (hb : ¬BddAbove (range f)), Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)
⊢ Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)

Tactic:
if hb : BddAbove (range f) then
    exact hf.ciSup_comp_tendsto_atTop hb hg
  else
    rw [iSup, iSup, csSup_of_not_bddAbove, csSup_of_not_bddAbove hb]
    rwa [BddAbove, ← Function.comp_def f g, hf.upperBounds_range_comp_tendsto_atTop hg]

Premises used: iSup, csSup_of_not_bddAbove, BddAbove, Monotone.upperBounds_range_comp_tendsto_atTop, Function.comp_def, Set.range
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLinearOrder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atBot
⊢ Eq.{u_5 + 1} (α := γ) (⨅ (a : α), f (g a)) (⨅ (b : β), f b)

Tactic:
hf.dual.ciSup_comp_tendsto_atTop_of_linearOrder hg

Premises used: iInf, Monotone.dual, OrderDual, Monotone.ciSup_comp_tendsto_atTop_of_linearOrder
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLinearOrder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Antitone f
g : α → β
hg : Tendsto g l atTop
⊢ Eq.{u_5 + 1} (α := γ) (⨅ (a : α), f (g a)) (⨅ (b : β), f b)

Tactic:
hf.dual_left.ciInf_comp_tendsto_atBot_of_linearOrder hg

Premises used: Antitone.dual_left, OrderDual, Monotone.ciInf_comp_tendsto_atBot_of_linearOrder
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLinearOrder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Antitone f
g : α → β
hg : Tendsto g l atBot
⊢ Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)

Tactic:
hf.dual_left.ciSup_comp_tendsto_atTop_of_linearOrder hg

Premises used: Antitone.dual_left, OrderDual, Monotone.ciSup_comp_tendsto_atTop_of_linearOrder
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLattice γ
inst_2 : OrderTop γ
l : Filter α
inst_3 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
⊢ Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)

Tactic:
hf.ciSup_comp_tendsto_atTop (OrderTop.bddAbove _) hg

Premises used: OrderTop.bddAbove, Monotone.ciSup_comp_tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLattice γ
inst_2 : OrderBot γ
l : Filter α
inst_3 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atBot
⊢ Eq.{u_5 + 1} (α := γ) (⨅ (a : α), f (g a)) (⨅ (b : β), f b)

Tactic:
hf.ciInf_comp_tendsto_atBot (OrderBot.bddBelow _) hg

Premises used: Monotone.ciInf_comp_tendsto_atBot, OrderBot.bddBelow
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLattice γ
inst_2 : OrderTop γ
l : Filter α
inst_3 : l.NeBot
f : β → γ
hf : Antitone f
g : α → β
hg : Tendsto g l atBot
⊢ Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)

Tactic:
hf.ciSup_comp_tendsto_atBot (OrderTop.bddAbove _) hg

Premises used: OrderTop.bddAbove, Antitone.ciSup_comp_tendsto_atBot
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : ConditionallyCompleteLattice γ
inst_2 : OrderBot γ
l : Filter α
inst_3 : l.NeBot
f : β → γ
hf : Antitone f
g : α → β
hg : Tendsto g l atTop
⊢ Eq.{u_5 + 1} (α := γ) (⨅ (a : α), f (g a)) (⨅ (b : β), f b)

Tactic:
hf.ciInf_comp_tendsto_atTop (OrderBot.bddBelow _) hg

Premises used: Antitone.ciInf_comp_tendsto_atTop, OrderBot.bddBelow
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
l : Filter α
inst_1 : l.NeBot
s : β → Set γ
hs : Monotone s
f : α → β
hf : Tendsto f l atTop
⊢ Eq.{u_5 + 1} (α := Set γ) (⋃ (a : α), s (f a)) (⋃ (b : β), s b)

Tactic:
hs.iSup_comp_tendsto_atTop hf

Premises used: Monotone.iSup_comp_tendsto_atTop, Set.iUnion
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
l : Filter α
inst_1 : l.NeBot
s : β → Set γ
hs : Monotone s
f : α → β
hf : Tendsto f l atBot
⊢ Eq.{u_5 + 1} (α := Set γ) (⋂ (a : α), s (f a)) (⋂ (b : β), s b)

Tactic:
hs.iInf_comp_tendsto_atBot hf

Premises used: Set.iInter, Monotone.iInf_comp_tendsto_atBot
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
l : Filter α
inst_1 : l.NeBot
s : β → Set γ
hs : Antitone s
f : α → β
hf : Tendsto f l atTop
⊢ Eq.{u_5 + 1} (α := Set γ) (⋂ (a : α), s (f a)) (⋂ (b : β), s b)

Tactic:
hs.iInf_comp_tendsto_atTop hf

Premises used: Set.iInter, Antitone.iInf_comp_tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
l : Filter α
inst_1 : l.NeBot
s : β → Set γ
hs : Antitone s
f : α → β
hf : Tendsto f l atBot
⊢ Eq.{u_5 + 1} (α := Set γ) (⋃ (a : α), s (f a)) (⋃ (b : β), s b)

Tactic:
hs.iSup_comp_tendsto_atBot hf

Premises used: Antitone.iSup_comp_tendsto_atBot, Set.iUnion
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Countable α
⊢ IsCountablyGenerated.{u_1} (α := α) atTop

Tactic:
isCountablyGenerated_seq _

Premises used: Filter.isCountablyGenerated_seq, Filter.atTop
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Countable α
⊢ IsCountablyGenerated.{u_1} (α := α) atBot

Tactic:
isCountablyGenerated_seq _

Premises used: Filter.isCountablyGenerated_seq, Filter.atBot
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : IsCountablyGenerated.{u_1} (α := α) atTop
inst_2 : Preorder β
inst_3 : IsCountablyGenerated.{u_2} (α := β) atTop
rw : (SProd.sprod (α := Filter α) (β := Filter β) atTop atTop).IsCountablyGenerated
⊢ IsCountablyGenerated (α := α × β) atTop

Tactic:
rw [← prod_atTop_atTop_eq]

Premises used: Filter.prod_atTop_atTop_eq
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : IsCountablyGenerated.{u_1} (α := α) atTop
inst_2 : Preorder β
inst_3 : IsCountablyGenerated.{u_2} (α := β) atTop
⊢ (SProd.sprod (α := Filter α) (β := Filter β) atTop atTop).IsCountablyGenerated

Tactic:
infer_instance
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : IsCountablyGenerated.{u_1} (α := α) atBot
inst_2 : Preorder β
inst_3 : IsCountablyGenerated.{u_2} (α := β) atBot
rw : (SProd.sprod (α := Filter α) (β := Filter β) atBot atBot).IsCountablyGenerated
⊢ IsCountablyGenerated (α := α × β) atBot

Tactic:
rw [← prod_atBot_atBot_eq]

Premises used: Filter.prod_atBot_atBot_eq
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : IsCountablyGenerated.{u_1} (α := α) atBot
inst_2 : Preorder β
inst_3 : IsCountablyGenerated.{u_2} (α := β) atBot
⊢ (SProd.sprod (α := Filter α) (β := Filter β) atBot atBot).IsCountablyGenerated

Tactic:
infer_instance
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
inst_3 : Countable α
⊢ HasCountableBasis atTop (fun (x : α) ↦ True) Ici

Tactic:
{ atTop_basis with countable := to_countable _ }

Premises used: Filter.HasCountableBasis.mk, Filter.atTop_basis, setOf, True, Set.to_countable
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
inst : Preorder α
inst_1 : IsCodirectedOrder α
inst_2 : Nonempty α
inst_3 : Countable α
⊢ HasCountableBasis atBot (fun (x : α) ↦ True) Iic

Tactic:
{ atBot_basis with countable := to_countable _ }

Premises used: Filter.HasCountableBasis.mk, setOf, Filter.atBot_basis, True, Set.to_countable
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
inst : f.IsCountablyGenerated
inst_1 : f.NeBot
obtain : ∀ (B : ℕ → Set α) (h : f.HasAntitoneBasis B), ∃ (x : ℕ → α), Tendsto x atTop f
⊢ ∃ (x : ℕ → α), Tendsto x atTop f

Tactic:
obtain ⟨B, h⟩ := f.exists_antitone_basis

Premises used: Filter.exists_antitone_basis
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
inst : f.IsCountablyGenerated
inst_1 : f.NeBot
B : ℕ → Set α
h : f.HasAntitoneBasis B
choose : ∀ (x : (n : ℕ) → α) (hx : ∀ (n : ℕ), x n ∈ B n), ∃ (x : ℕ → α), Tendsto x atTop f
⊢ ∃ (x : ℕ → α), Tendsto x atTop f

Tactic:
choose x hx using fun n => Filter.nonempty_of_mem (h.mem n)

Premises used: Filter.nonempty_of_mem, Filter.HasAntitoneBasis.mem
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
inst : f.IsCountablyGenerated
inst_1 : f.NeBot
B : ℕ → Set α
h : f.HasAntitoneBasis B
x : (n : ℕ) → α
hx : ∀ (n : ℕ), x n ∈ B n
⊢ ∃ (x : ℕ → α), Tendsto x atTop f

Tactic:
⟨x, h.tendsto hx⟩

Premises used: Filter.HasAntitoneBasis.tendsto, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
inst : f.IsCountablyGenerated
inst_1 : f.NeBot
B : ℕ → Set α
h : f.HasAntitoneBasis B
x : (n : ℕ) → α
hx : ∀ (n : ℕ), x n ∈ B n
⊢ ∃ (x : ℕ → α), Tendsto x atTop f

Tactic:
exact ⟨x, h.tendsto hx⟩
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
obtain : ∀ (ys : ℕ → α) (h : Tendsto ys atTop atTop), ∃ (xs : ℕ → α), Monotone xs ∧ Tendsto xs atTop atTop
⊢ ∃ (xs : ℕ → α), Monotone xs ∧ Tendsto xs atTop atTop

Tactic:
obtain ⟨ys, h⟩ := exists_seq_tendsto (atTop : Filter α)

Premises used: Filter.atTop, Filter.exists_seq_tendsto
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
choose :
  ∀ (c : (a b : α) → α) (hleft : ∀ (a b : α), a ≤ c a b) (hright : ∀ (a b : α), b ≤ c a b),
    ∃ (xs : ℕ → α), Monotone xs ∧ Tendsto xs atTop atTop
⊢ ∃ (xs : ℕ → α), Monotone xs ∧ Tendsto xs atTop atTop

Tactic:
choose c hleft hright using exists_ge_ge (α := α)

Premises used: exists_ge_ge
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
c : (a b : α) → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun (n : ℕ) ↦ List.foldl (fun (x : α) (n : ℕ) ↦ c x (ys n)) (ys 0) (List.range n)
n : ℕ
⊢ xs (n + 1) = c (xs n) (ys n)

Tactic:
simp [xs, List.range_succ]

Premises used: List.range_succ
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
c : (a b : α) → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun (n : ℕ) ↦ List.foldl (fun (x : α) (n : ℕ) ↦ c x (ys n)) (ys 0) (List.range n)
⊢ ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)

Tactic:
have hsucc (n : ℕ) : xs (n + 1) = c (xs n) (ys n) := by simp [xs, List.range_succ]
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
c : (a b : α) → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun (n : ℕ) ↦ List.foldl (fun (x : α) (n : ℕ) ↦ c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
⊢ ∃ (xs : ℕ → α), Monotone xs ∧ Tendsto xs atTop atTop

Tactic:
⟨xs, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
c : (a b : α) → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun (n : ℕ) ↦ List.foldl (fun (x : α) (n : ℕ) ↦ c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
refine_1 : Monotone xs
refine_2 : Tendsto xs atTop atTop
⊢ ∃ (xs : ℕ → α), Monotone xs ∧ Tendsto xs atTop atTop

Tactic:
refine ⟨xs, ?_, ?_⟩
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
c : (a b : α) → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun (n : ℕ) ↦ List.foldl (fun (x : α) (n : ℕ) ↦ c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
⊢ Monotone xs

Tactic:
monotone_nat_of_le_succ fun n ↦ ?_

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
c : (a b : α) → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun (n : ℕ) ↦ List.foldl (fun (x : α) (n : ℕ) ↦ c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
refine_1 : ∀ (n : ℕ), xs n ≤ xs (n + 1)
⊢ Monotone xs

Tactic:
refine monotone_nat_of_le_succ fun n ↦ ?_

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
c : (a b : α) → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun (n : ℕ) ↦ List.foldl (fun (x : α) (n : ℕ) ↦ c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
refine_1 : xs n ≤ c (xs n) (ys n)
⊢ xs n ≤ xs (n + 1)

Tactic:
rw [hsucc]
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
c : (a b : α) → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun (n : ℕ) ↦ List.foldl (fun (x : α) (n : ℕ) ↦ c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ xs n ≤ c (xs n) (ys n)

Tactic:
apply hleft
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
c : (a b : α) → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun (n : ℕ) ↦ List.foldl (fun (x : α) (n : ℕ) ↦ c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
⊢ Tendsto xs atTop atTop

Tactic:
(tendsto_add_atTop_iff_nat 1).1 <| tendsto_atTop_mono (fun n ↦ ?_) h

Premises used: Filter.tendsto_atTop_mono, Iff.mp, Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
c : (a b : α) → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun (n : ℕ) ↦ List.foldl (fun (x : α) (n : ℕ) ↦ c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
refine_2 : ∀ (n : ℕ), ys n ≤ xs (n + 1)
⊢ Tendsto xs atTop atTop

Tactic:
refine (tendsto_add_atTop_iff_nat 1).1 <| tendsto_atTop_mono (fun n ↦ ?_) h

Premises used: Filter.tendsto_atTop_mono, Iff.mp, Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
c : (a b : α) → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun (n : ℕ) ↦ List.foldl (fun (x : α) (n : ℕ) ↦ c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
refine_2 : ys n ≤ c (xs n) (ys n)
⊢ ys n ≤ xs (n + 1)

Tactic:
rw [hsucc]
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
c : (a b : α) → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun (n : ℕ) ↦ List.foldl (fun (x : α) (n : ℕ) ↦ c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ ys n ≤ c (xs n) (ys n)

Tactic:
apply hright
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsCodirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atBot
⊢ ∃ (xs : ℕ → α), Antitone xs ∧ Tendsto xs atTop atBot

Tactic:
exists_seq_monotone_tendsto_atTop_atTop αᵒᵈ

Premises used: setOf, Antitone, Filter.exists_seq_monotone_tendsto_atTop_atTop, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst : k.IsCountablyGenerated
⊢ Tendsto f k l ↔ ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l

Tactic:
⟨fun h x hx => h.comp hx, fun H s hs => ?_⟩

Premises used: Iff.intro, Filter.Tendsto.comp
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst : k.IsCountablyGenerated
refine : ∀ (H : ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l) (s : Set β) (hs : s ∈ l), s ∈ map f k
⊢ Tendsto f k l ↔ ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l

Tactic:
refine ⟨fun h x hx => h.comp hx, fun H s hs => ?_⟩
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst : k.IsCountablyGenerated
H : ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l
s : Set β
hs : s ∈ l
contrapose! : ∀ (H : s ∉ map f k), ∃ (x : ℕ → α), Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
⊢ s ∈ map f k

Tactic:
contrapose! H
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
⊢ (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot

Tactic:
simpa [neBot_iff, inf_principal_eq_bot]

Premises used: Filter.inf_principal_eq_bot, Filter.neBot_iff
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
⊢ (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot

Tactic:
have : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ)) := by simpa [neBot_iff, inf_principal_eq_bot]
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
rcases :
  ∀ (x : ℕ → α) (hx : Tendsto x atTop (k ⊓ 𝓟 (f ⁻¹' sᶜ))), ∃ (x : ℕ → α), Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
⊢ ∃ (x : ℕ → α), Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l

Tactic:
rcases (k ⊓ 𝓟 (f ⁻¹' sᶜ)).exists_seq_tendsto with ⟨x, hx⟩

Premises used: Compl.compl, Set.preimage, Filter.principal, Filter.exists_seq_tendsto, Min.min
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop (k ⊓ 𝓟 (f ⁻¹' sᶜ))
⊢ Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ

Tactic:
rw [tendsto_inf, tendsto_principal] at hx

Premises used: Filter.tendsto_inf, Filter.tendsto_principal
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
⊢ ∃ (x : ℕ → α), Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l

Tactic:
⟨x, hx.1, fun h => ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
refine : ∀ (h : Tendsto (f ∘ x) atTop l), False
⊢ ∃ (x : ℕ → α), Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l

Tactic:
refine ⟨x, hx.1, fun h => ?_⟩
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
h : Tendsto (f ∘ x) atTop l
rcases : ∀ (N : ℕ) (hnotMem : x N ∈ f ⁻¹' sᶜ) (hmem : (f ∘ x) N ∈ s), False
⊢ False

Tactic:
rcases (hx.2.and (h hs)).exists with ⟨N, hnotMem, hmem⟩

Premises used: Filter.Eventually.and, Filter.Eventually.exists, And.right
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
h : Tendsto (f ∘ x) atTop l
N : ℕ
hnotMem : x N ∈ f ⁻¹' sᶜ
hmem : (f ∘ x) N ∈ s
⊢ False

Tactic:
hnotMem hmem
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst : k.IsCountablyGenerated
s : Set β
hs : s ∈ l
H : s ∉ map f k
this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
x : ℕ → α
hx : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
h : Tendsto (f ∘ x) atTop l
N : ℕ
hnotMem : x N ∈ f ⁻¹' sᶜ
hmem : (f ∘ x) N ∈ s
⊢ False

Tactic:
exact hnotMem hmem
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
β : Type u_2
f : α → β
k : Filter α
l : Filter β
inst : k.IsCountablyGenerated
⊢ (∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l) → Tendsto f k l

Tactic:
tendsto_iff_seq_tendsto.2

Premises used: Iff.mpr, Filter.tendsto_iff_seq_tendsto
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst : l.IsCountablyGenerated
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)

Tactic:
simpa using tendsto_iff_seq_tendsto (f := id) (l := 𝓟 {x | p x})

Premises used: Filter.tendsto_iff_seq_tendsto