awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CompleteLattice (goal)
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
hb : ¬BddAbove (range f)
rwa : ¬Set.Nonempty.{u_5} (α := γ) (upperBounds (range fun (a : α) ↦ f (g a)))
rwa₁ : ¬(upperBounds (range (f ∘ g))).Nonempty
⊢ ¬BddAbove.{u_5} (α := γ) (range fun (a : α) ↦ f (g a))
have rwa₂ : ¬(upperBounds (range f)).Nonempty
Tactic: rwa [BddAbove, ← Function.comp_def f g, hf.upperBounds_range_comp_tendsto_atTop hg]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CompleteLattice (goal)
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
⊢ Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)
have if : ∀ (hb : BddAbove (range f)), 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]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CompleteLattice (goal)
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)
⊢ Eq.{u_5 + 1} (α := γ) (⨆ (a : α), f (g a)) (⨆ (b : β), f b)
have if₁ : ∀ (hb : ¬BddAbove (range f)), 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]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : IsCountablyGenerated.{u_1} (α := α) atTop
inst_2 : Preorder β
inst_3 : IsCountablyGenerated.{u_2} (α := β) atTop
⊢ IsCountablyGenerated (α := α × β) atTop
have rw : (SProd.sprod (α := Filter α) (β := Filter β) atTop atTop).IsCountablyGenerated
Tactic: rw [← prod_atTop_atTop_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : IsCountablyGenerated.{u_1} (α := α) atBot
inst_2 : Preorder β
inst_3 : IsCountablyGenerated.{u_2} (α := β) atBot
⊢ IsCountablyGenerated (α := α × β) atBot
have rw : (SProd.sprod (α := Filter α) (β := Filter β) atBot atBot).IsCountablyGenerated
Tactic: rw [← prod_atBot_atBot_eq]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
α : Type u_1
f : Filter α
inst : f.IsCountablyGenerated
inst_1 : f.NeBot
⊢ ∃ (x : ℕ → α), Tendsto x atTop f
have obtain : ∀ (B : ℕ → Set α) (h : f.HasAntitoneBasis B), ∃ (x : ℕ → α), Tendsto x atTop f
Tactic: obtain ⟨B, h⟩ := f.exists_antitone_basis
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
α : Type u_1
f : Filter α
inst : f.IsCountablyGenerated
inst_1 : f.NeBot
B : ℕ → Set α
h : f.HasAntitoneBasis B
⊢ ∃ (x : ℕ → α), Tendsto x atTop f
have choose : ∀ (x : (n : ℕ) → α) (hx : ∀ (n : ℕ), x n ∈ B n), ∃ (x : ℕ → α), Tendsto x atTop f
Tactic: choose x hx using fun n => Filter.nonempty_of_mem (h.mem n)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
⊢ ∃ (xs : ℕ → α), Monotone xs ∧ Tendsto xs atTop atTop
have obtain : ∀ (ys : ℕ → α) (h : Tendsto ys atTop atTop), ∃ (xs : ℕ → α), Monotone xs ∧ Tendsto xs atTop atTop
Tactic: obtain ⟨ys, h⟩ := exists_seq_tendsto (atTop : Filter α)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
α : Type u_3
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : IsCountablyGenerated.{u_3} (α := α) atTop
ys : ℕ → α
h : Tendsto ys atTop atTop
⊢ ∃ (xs : ℕ → α), Monotone xs ∧ Tendsto xs atTop atTop
have 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
Tactic: choose c hleft hright using exists_ge_ge (α := α)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (hypothesis)
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)
⊢ ∃ (xs : ℕ → α), Monotone xs ∧ Tendsto xs atTop atTop
have hsucc : ∀ (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]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
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
have refine_1 : Monotone xs
Tactic: refine ⟨xs, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
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
⊢ ∃ (xs : ℕ → α), Monotone xs ∧ Tendsto xs atTop atTop
have refine_2 : Tendsto xs atTop atTop
Tactic: refine ⟨xs, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
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
have refine_1 : ∀ (n : ℕ), xs n ≤ xs (n + 1)
Tactic: refine monotone_nat_of_le_succ fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
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 ≤ xs (n + 1)
have refine_1 : xs n ≤ c (xs n) (ys n)
Tactic: rw [hsucc]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
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
have refine_2 : ∀ (n : ℕ), ys n ≤ xs (n + 1)
Tactic: refine (tendsto_add_atTop_iff_nat 1).1 <| tendsto_atTop_mono (fun n ↦ ?_) h
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
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 ≤ xs (n + 1)
have refine_2 : ys n ≤ c (xs n) (ys n)
Tactic: rw [hsucc]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
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
have refine : ∀ (H : ∀ (x : ℕ → α), Tendsto x atTop k → Tendsto (f ∘ x) atTop l) (s : Set β) (hs : s ∈ l), s ∈ map f k
Tactic: refine ⟨fun h x hx => h.comp hx, fun H s hs => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
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
⊢ s ∈ map f k
have contrapose! : ∀ (H : s ∉ map f k), ∃ (x : ℕ → α), Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (hypothesis)
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
⊢ ∃ (x : ℕ → α), Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
have this : (k ⊓ 𝓟 (f ⁻¹' sᶜ)).NeBot
Tactic: have : NeBot (k ⊓ 𝓟 (f ⁻¹' sᶜ)) := by simpa [neBot_iff, inf_principal_eq_bot]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
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 : ℕ → α), Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
have rcases : ∀ (x : ℕ → α) (hx : Tendsto x atTop (k ⊓ 𝓟 (f ⁻¹' sᶜ))), ∃ (x : ℕ → α), Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
Tactic: rcases (k ⊓ 𝓟 (f ⁻¹' sᶜ)).exists_seq_tendsto with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (hypothesis)
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ᶜ))
⊢ ∃ (x : ℕ → α), Tendsto x atTop k ∧ ¬Tendsto (f ∘ x) atTop l
have hx₁ : Tendsto x atTop k ∧ ∀ᶠ (a : ℕ) in atTop, x a ∈ f ⁻¹' sᶜ
Tactic: rw [tendsto_inf, tendsto_principal] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
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
have refine : ∀ (h : Tendsto (f ∘ x) atTop l), False
Tactic: refine ⟨x, hx.1, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
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
⊢ False
have rcases : ∀ (N : ℕ) (hnotMem : x N ∈ f ⁻¹' sᶜ) (hmem : (f ∘ x) N ∈ s), False
Tactic: rcases (hx.2.and (h hs)).exists with ⟨N, hnotMem, hmem⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
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)
have simp : (¬∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, ¬p (x n)) ↔
  ∃ (x : ℕ → ι), Tendsto x atTop l ∧ ¬∀ᶠ (x_1 : ℕ) in atTop, ¬p (x x_1)
Tactic: simp only [Filter.Frequently, eventually_iff_seq_eventually (l := l)]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst : l.IsCountablyGenerated
⊢ (¬∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, ¬p (x n)) ↔
    ∃ (x : ℕ → ι), Tendsto x atTop l ∧ ¬∀ᶠ (x_1 : ℕ) in atTop, ¬p (x x_1)
have push : (∃ (x : ℕ → ι), Tendsto x atTop l ∧ ∃ᶠ (x_1 : ℕ) in atTop, p (x x_1)) ↔
  ∃ (x : ℕ → ι), Tendsto x atTop l ∧ ∃ᶠ (x_1 : ℕ) in atTop, p (x x_1)
Tactic: push Not
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (hypothesis)
Goal:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst : l.IsCountablyGenerated
h : ∃ᶠ (n : ι) in l, p n
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)
have h₁ : ∃ (x : ℕ → ι), Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
Tactic: rw [frequently_iff_seq_frequently] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst : l.IsCountablyGenerated
h : ∃ (x : ℕ → ι), Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)
have obtain : ∀ (x : ℕ → ι) (hx_tendsto : Tendsto x atTop l) (hx_freq : ∃ᶠ (n : ℕ) in atTop, p (x n)),
  ∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)
Tactic: obtain ⟨x, hx_tendsto, hx_freq⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst : l.IsCountablyGenerated
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)
have obtain : ∀ (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)
Tactic: obtain ⟨n_to_n, h_tendsto, h_freq⟩ := subseq_forall_of_frequently hx_tendsto hx_freq
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst : l.IsCountablyGenerated
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ (ms : ℕ → ℕ), Tendsto (fun (n : ℕ) ↦ x (ns (ms n))) atTop f
⊢ Tendsto x l f
have contrapose! : ∀ (hxy : ¬Tendsto x l f),
  ∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (ms : ℕ → ℕ), ¬Tendsto (fun (n : ℕ) ↦ x (ns (ms n))) atTop f
Tactic: contrapose! hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst : l.IsCountablyGenerated
hxy : ¬Tendsto x l f
⊢ ∃ s ∈ f, ∃ᶠ (n : ι) in l, x n ∉ s
have rwa : ∀ (hxy : ∃ s ∈ f, ∃ᶠ (x_1 : ι) in l, x x_1 ∉ s), ∃ s ∈ f, ∃ᶠ (n : ι) in l, x n ∉ s
Tactic: rwa [not_tendsto_iff_exists_frequently_notMem] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst : l.IsCountablyGenerated
hxy : ¬Tendsto x l f
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (ms : ℕ → ℕ), ¬Tendsto (fun (n : ℕ) ↦ x (ns (ms n))) atTop f
have obtain : ∀ (s : Set α) (hs : s ∈ f) (hfreq : ∃ᶠ (n : ι) in l, x n ∉ s),
  ∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (ms : ℕ → ℕ), ¬Tendsto (fun (n : ℕ) ↦ x (ns (ms n))) atTop f
Tactic: obtain ⟨s, hs, hfreq⟩ : ∃ s ∈ f, ∃ᶠ n in l, x n ∉ s := by
    rwa [not_tendsto_iff_exists_frequently_notMem] at hxy
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst : l.IsCountablyGenerated
hxy : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, x n ∉ s
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (ms : ℕ → ℕ), ¬Tendsto (fun (n : ℕ) ↦ x (ns (ms n))) atTop f
have obtain : ∀ (y : ℕ → ι) (hy_tendsto : Tendsto y atTop l) (hy_freq : ∀ (n : ℕ), x (y n) ∉ s),
  ∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (ms : ℕ → ℕ), ¬Tendsto (fun (n : ℕ) ↦ x (ns (ms n))) atTop f
Tactic: obtain ⟨y, hy_tendsto, hy_freq⟩ := exists_seq_forall_of_frequently hfreq
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst : l.IsCountablyGenerated
hxy : ¬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
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (ms : ℕ → ℕ), ¬Tendsto (fun (n : ℕ) ↦ x (ns (ms n))) atTop f
have refine : ∀ (ms : ℕ → ℕ) (hms_tendsto : Tendsto (fun (n : ℕ) ↦ x (y (ms n))) atTop f), False
Tactic: refine ⟨y, hy_tendsto, fun ms hms_tendsto ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst : l.IsCountablyGenerated
hxy : ¬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
have rcases : ∀ (n : ℕ) (hn : x (y (ms n)) ∈ s), False
Tactic: rcases (hms_tendsto.eventually_mem hs).exists with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
g : Filter ι
inst : g.IsCountablyGenerated
u : ι → α
f : Filter α
inst_1 : f.IsCountablyGenerated
hx : (f ⊓ map u g).NeBot
⊢ ∃ (θ : ℕ → ι), Tendsto θ atTop g ∧ Tendsto (u ∘ θ) atTop f
have hx₁ : (comap u f ⊓ g).NeBot
Tactic: rw [← Filter.push_pull', map_neBot_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
α : Type u_1
ι : Type u_3
g : Filter ι
inst : g.IsCountablyGenerated
u : ι → α
f : Filter α
inst_1 : f.IsCountablyGenerated
hx : (comap u f ⊓ g).NeBot
⊢ ∃ (θ : ℕ → ι), Tendsto θ atTop g ∧ Tendsto (u ∘ θ) atTop f
have obtain : ∀ (θ : ℕ → ι) (hθ : Tendsto θ atTop (comap u f ⊓ g)), ∃ (θ : ℕ → ι), Tendsto θ atTop g ∧ Tendsto (u ∘ θ) atTop f
Tactic: obtain ⟨θ, hθ⟩ := exists_seq_tendsto (comap u f ⊓ g)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
α : Type u_1
f : Filter α
inst : f.IsCountablyGenerated
u : ℕ → α
hx : (f ⊓ map u atTop).NeBot
⊢ ∃ (θ : ℕ → ℕ), StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
have obtain : ∀ (φ : ℕ → ℕ) (hφ : Tendsto φ atTop atTop ∧ Tendsto (u ∘ φ) atTop f),
  ∃ (θ : ℕ → ℕ), StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
Tactic: obtain ⟨φ, hφ⟩ := exists_seq_comp_tendsto hx
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.CountablyGenerated (goal)
Goal:
α : Type u_1
f : Filter α
inst : f.IsCountablyGenerated
u : ℕ → α
hx : (f ⊓ map u atTop).NeBot
φ : ℕ → ℕ
hφ : Tendsto φ atTop atTop ∧ Tendsto (u ∘ φ) atTop f
⊢ ∃ (θ : ℕ → ℕ), StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
have obtain : ∀ (ψ : ℕ → ℕ) (hψ : StrictMono ψ) (hψφ : StrictMono (φ ∘ ψ)), ∃ (θ : ℕ → ℕ), StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
Tactic: obtain ⟨ψ, hψ, hψφ⟩ : ∃ ψ : ℕ → ℕ, StrictMono ψ ∧ StrictMono (φ ∘ ψ) :=
    strictMono_subseq_of_tendsto_atTop hφ.1
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
h : ∃ᶠ (x : α) in atTop, p x
a : α
⊢ ∃ (b : α), a ≤ b ∧ p b
have rw : ∀ (h : ¬∀ᶠ (x : α) in atTop, ¬p x) (a : α), ∃ (b : α), a ≤ b ∧ p b
Tactic: rw [Filter.Frequently] at h
Cleared hypotheses: h, a
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
h : ¬∀ᶠ (x : α) in atTop, ¬p x
a : α
⊢ ∃ (b : α), a ≤ b ∧ p b
have contrapose! : ∀ (h : ∀ (b : α) (_ : a ≤ b), ¬p b), ∀ᶠ (x : α) in atTop, ¬p x
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ atTop = generate (Ici '' s)
have rw : generate (range Ici) = generate (Ici '' s)
Tactic: rw [atTop_eq_generate_Ici]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ generate (range Ici) = generate (Ici '' s)
have a : generate (range Ici) ≤ generate (Ici '' s)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
a : generate (range Ici) ≤ generate (Ici '' s)
⊢ generate (range Ici) = generate (Ici '' s)
have a₁ : generate (Ici '' s) ≤ generate (range Ici)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ generate (range Ici) ≤ generate (Ici '' s)
have a : Ici '' s ⊆ sets (generate (range Ici))
Tactic: rw [le_generate_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ generate (Ici '' s) ≤ generate (range Ici)
have a : range Ici ⊆ (generate (Ici '' s)).sets
Tactic: rw [le_generate_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x : α
⊢ Ici x ∈ (generate (Ici '' s)).sets
have a : ∀ (y : α) (ys : y ∈ s) (hy : x ≤ y), Ici x ∈ (generate (Ici '' s)).sets
Tactic: rcases hs x with ⟨y, ys, hy⟩
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (hypothesis)
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x y : α
ys : y ∈ s
hy : x ≤ y
⊢ Ici x ∈ (generate (Ici '' s)).sets
have A : Ici y ∈ generate (Ici '' s)
Tactic: have A : Ici y ∈ generate (Ici '' s) := mem_generate_of_mem (mem_image_of_mem _ ys)
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (hypothesis)
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x y : α
ys : y ∈ s
hy : x ≤ y
A : Ici y ∈ generate (Ici '' s)
⊢ Ici x ∈ (generate (Ici '' s)).sets
have B : Ici y ⊆ Ici x
Tactic: have B : Ici y ⊆ Ici x := Ici_subset_Ici.2 hy
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ atTop = generate (Ici '' s)
have refine : ∀ (x : α), ∃ y ∈ s, x ≤ y
Tactic: refine atTop_eq_generate_of_forall_exists_le fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
hs : ¬BddAbove s
x : α
⊢ ∃ y ∈ s, x ≤ y
have obtain : ∀ (y : α) (hy : y ∈ s) (hy' : x < y), ∃ y ∈ s, x ≤ y
Tactic: obtain ⟨y, hy, hy'⟩ := not_bddAbove_iff.mp hs x
-- Lean 4 proof step from Mathlib.Order.Filter.AtTopBot.Defs (goal)
Goal:
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst : Preorder ι
s : ι → Set α
inst_1 : (i : ι) → DecidablePred fun (x : α) ↦ x ∈ s i
inst_2 : DecidablePred fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
hs : Monotone s
f g : (a : α) → β a
a : α
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a
have inl : ∀ (i : ι) (hi : a ∈ s i),
  ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a
Tactic: rcases em (∃ i, a ∈ s i) with ⟨i, hi⟩ | ha