awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst : l.IsCountablyGenerated
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)
⊢ (∃ᶠ (n : ι) in l, p n) ↔ ∃ (x : ℕ → ι), Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)

Tactic:
simp only [Filter.Frequently, eventually_iff_seq_eventually (l := l)]

Premises used: Filter.eventually_iff_seq_eventually, Filter.Frequently
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst : l.IsCountablyGenerated
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)
⊢ (¬∀ (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:
push Not

Premises used: Not
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst : l.IsCountablyGenerated
⊢ (∃ (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:
rfl
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst : l.IsCountablyGenerated
h : ∃ᶠ (n : ι) in l, p n
⊢ ∃ (x : ℕ → ι), Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)

Tactic:
rw [frequently_iff_seq_frequently] at h

Premises used: Filter.frequently_iff_seq_frequently
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst : l.IsCountablyGenerated
h : ∃ (x : ℕ → ι), Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
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)
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)

Tactic:
obtain ⟨x, hx_tendsto, hx_freq⟩ := h
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
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)
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)
⊢ ∃ (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

Premises used: Filter.subseq_forall_of_frequently
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
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)
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:
⟨x ∘ n_to_n, h_tendsto, h_freq⟩

Premises used: Function.comp, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
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)
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:
exact ⟨x ∘ n_to_n, h_tendsto, h_freq⟩
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst : l.IsCountablyGenerated
⊢ (∃ᶠ (n : ι) in l, p n) ↔ ∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)

Tactic:
⟨exists_seq_forall_of_frequently, fun ⟨_ns, hnsl, hpns⟩ ↦
    hnsl.frequently <| Frequently.of_forall hpns⟩

Premises used: Filter.Frequently.of_forall, Filter.Tendsto.frequently, Filter.Frequently, Filter.exists_seq_forall_of_frequently, Iff.intro, _private.0.Filter.frequently_iff_seq_forall.match_1
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
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
contrapose! :
  ∀ (hxy : ¬Tendsto x l f),
    ∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (ms : ℕ → ℕ), ¬Tendsto (fun (n : ℕ) ↦ x (ns (ms n))) atTop f
⊢ Tendsto x l f

Tactic:
contrapose! hxy
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst : l.IsCountablyGenerated
hxy : ¬Tendsto x l f
rwa rwa₁ rwa₂ rwa₃ : ∀ (hxy : ∃ s ∈ f, ∃ᶠ (x_1 : ι) in l, x x_1 ∉ s), ∃ s ∈ f, ∃ᶠ (n : ι) in l, x n ∉ s
⊢ ∃ s ∈ f, ∃ᶠ (n : ι) in l, x n ∉ s

Tactic:
rwa [not_tendsto_iff_exists_frequently_notMem] at hxy

Premises used: Filter.not_tendsto_iff_exists_frequently_notMem
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst : l.IsCountablyGenerated
hxy : ¬Tendsto x l f
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
⊢ ∃ (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
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
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
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
⊢ ∃ (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

Premises used: Filter.exists_seq_forall_of_frequently
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
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

Tactic:
⟨y, hy_tendsto, fun ms hms_tendsto ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
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
refine : ∀ (ms : ℕ → ℕ) (hms_tendsto : Tendsto (fun (n : ℕ) ↦ x (y (ms n))) atTop f), False
⊢ ∃ (ns : ℕ → ι), Tendsto ns atTop l ∧ ∀ (ms : ℕ → ℕ), ¬Tendsto (fun (n : ℕ) ↦ x (ns (ms n))) atTop f

Tactic:
refine ⟨y, hy_tendsto, fun ms hms_tendsto ↦ ?_⟩
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
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
rcases : ∀ (n : ℕ) (hn : x (y (ms n)) ∈ s), False
⊢ False

Tactic:
rcases (hms_tendsto.eventually_mem hs).exists with ⟨n, hn⟩

Premises used: Filter.Tendsto.eventually_mem, Filter.Eventually.exists
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
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
n : ℕ
hn : x (y (ms n)) ∈ s
⊢ False

Tactic:
absurd hn <| hy_freq _

Premises used: absurd
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
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
n : ℕ
hn : x (y (ms n)) ∈ s
⊢ False

Tactic:
exact absurd hn <| hy_freq _

Premises used: absurd
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
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
⊢ (comap u f ⊓ g).NeBot

Tactic:
rw [← Filter.push_pull', map_neBot_iff] at hx

Premises used: Filter.push_pull', Filter.map_neBot_iff
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
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
obtain :
  ∀ (θ : ℕ → ι) (hθ : Tendsto θ atTop (comap u f ⊓ g)), ∃ (θ : ℕ → ι), Tendsto θ atTop g ∧ Tendsto (u ∘ θ) atTop f
⊢ ∃ (θ : ℕ → ι), Tendsto θ atTop g ∧ Tendsto (u ∘ θ) atTop f

Tactic:
obtain ⟨θ, hθ⟩ := exists_seq_tendsto (comap u f ⊓ g)

Premises used: Filter.exists_seq_tendsto, Min.min, Filter.comap
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
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
θ : ℕ → ι
hθ : Tendsto θ atTop (comap u f ⊓ g)
⊢ ∃ (θ : ℕ → ι), Tendsto θ atTop g ∧ Tendsto (u ∘ θ) atTop f

Tactic:
⟨θ, (tendsto_inf.1 hθ).2, tendsto_comap_iff.1 (tendsto_inf.1 hθ).1⟩

Premises used: Filter.tendsto_inf, Filter.tendsto_comap_iff, And.right, And.left, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
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
θ : ℕ → ι
hθ : Tendsto θ atTop (comap u f ⊓ g)
⊢ ∃ (θ : ℕ → ι), Tendsto θ atTop g ∧ Tendsto (u ∘ θ) atTop f

Tactic:
exact ⟨θ, (tendsto_inf.1 hθ).2, tendsto_comap_iff.1 (tendsto_inf.1 hθ).1⟩
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
inst : f.IsCountablyGenerated
u : ℕ → α
hx : (f ⊓ map u atTop).NeBot
obtain :
  ∀ (φ : ℕ → ℕ) (hφ : Tendsto φ atTop atTop ∧ Tendsto (u ∘ φ) atTop f),
    ∃ (θ : ℕ → ℕ), StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
⊢ ∃ (θ : ℕ → ℕ), StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Tactic:
obtain ⟨φ, hφ⟩ := exists_seq_comp_tendsto hx

Premises used: Filter.exists_seq_comp_tendsto
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
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 ψ ∧ StrictMono (φ ∘ ψ)

Tactic:
strictMono_subseq_of_tendsto_atTop hφ.1

Premises used: Filter.strictMono_subseq_of_tendsto_atTop, And.left
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
inst : f.IsCountablyGenerated
u : ℕ → α
hx : (f ⊓ map u atTop).NeBot
φ : ℕ → ℕ
hφ : Tendsto φ atTop atTop ∧ Tendsto (u ∘ φ) atTop f
obtain :
  ∀ (ψ : ℕ → ℕ) (hψ : StrictMono ψ) (hψφ : StrictMono (φ ∘ ψ)), ∃ (θ : ℕ → ℕ), StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
⊢ ∃ (θ : ℕ → ℕ), StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Tactic:
obtain ⟨ψ, hψ, hψφ⟩ : ∃ ψ : ℕ → ℕ, StrictMono ψ ∧ StrictMono (φ ∘ ψ) :=
    strictMono_subseq_of_tendsto_atTop hφ.1

Premises used: Filter.strictMono_subseq_of_tendsto_atTop, And.left
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
inst : f.IsCountablyGenerated
u : ℕ → α
hx : (f ⊓ map u atTop).NeBot
φ : ℕ → ℕ
hφ : Tendsto φ atTop atTop ∧ Tendsto (u ∘ φ) atTop f
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψφ : StrictMono (φ ∘ ψ)
⊢ ∃ (θ : ℕ → ℕ), StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Tactic:
⟨φ ∘ ψ, hψφ, hφ.2.comp hψ.tendsto_atTop⟩

Premises used: Function.comp, StrictMono.tendsto_atTop, And.right, And.intro, Exists.intro, Filter.Tendsto.comp
-- Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Goal:
α : Type u_1
f : Filter α
inst : f.IsCountablyGenerated
u : ℕ → α
hx : (f ⊓ map u atTop).NeBot
φ : ℕ → ℕ
hφ : Tendsto φ atTop atTop ∧ Tendsto (u ∘ φ) atTop f
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψφ : StrictMono (φ ∘ ψ)
⊢ ∃ (θ : ℕ → ℕ), StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Tactic:
exact ⟨φ ∘ ψ, hψφ, hφ.2.comp hψ.tendsto_atTop⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
a : α
⊢ Membership.mem (γ := Filter α) atTop {b : α | a ≤ b}

Tactic:
mem_iInf_of_mem a <| Subset.refl _

Premises used: Set.Subset.refl, Set.Mem, Filter.mem_iInf_of_mem
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
a : α
⊢ Membership.mem (γ := Filter α) atTop (Ici a)

Tactic:
mem_atTop a

Premises used: Set.Ici, Set.Mem, Filter.mem_atTop, setOf
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
inst_1 : NoTopOrder α
x : α
⊢ Membership.mem (γ := Filter α) atTop (Ioi x)

Tactic:
let ⟨z, hz⟩ := exists_not_le x
  mem_of_superset (inter_mem (mem_atTop x) (mem_atTop z))
    fun _ ⟨hxy, hzy⟩ => lt_of_le_not_ge hxy fun hyx => hz (hzy.trans hyx)

Premises used: Set.Ioi, Filter.mem_atTop, Filter.inter_mem, _private.0.Filter.Ioi_mem_atTop.match_2, Membership.mem, Filter.atTop, lt_of_le_not_ge, NoTopOrder.exists_not_le, _private.0.Filter.Ioi_mem_atTop.match_1, LE.le.trans, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
a : α
⊢ ∀ᶠ (x : α) in atTop, a ≤ x

Tactic:
mem_atTop a

Premises used: Set.Mem, Filter.mem_atTop, Filter.Eventually, setOf
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
inst_1 : NoTopOrder α
a : α
⊢ ∀ᶠ (x : α) in atTop, a < x

Tactic:
Ioi_mem_atTop a

Premises used: Set.Ioi, Set.Mem, Filter.Eventually, setOf, Filter.Ioi_mem_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
inst_1 : NoTopOrder α
a : α
⊢ ∀ᶠ (x : α) in atTop, x ≠ a

Tactic:
(eventually_gt_atTop a).mono fun _ => ne_of_gt

Premises used: ne_of_gt, Filter.Eventually.mono, Filter.eventually_gt_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
a : α
ha : IsTop a
⊢ atTop = 𝓟 (Ici a)

Tactic:
(iInf_le _ _).antisymm <| le_iInf fun b ↦ principal_mono.2 <| Ici_subset_Ici.2 <| ha b

Premises used: Iff.mpr, Filter.principal_mono, le_iInf, LE.le.antisymm, Set.Ici_subset_Ici, Filter.atTop, iInf_le
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
⊢ Eq.{u_3 + 1} (α := Filter α) atTop (generate (range Ici))

Tactic:
simp only [generate_eq_biInf, atTop, iInf_range]

Premises used: iInf_range, Filter.atTop, Filter.generate_eq_biInf
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
h : ∃ᶠ (x : α) in atTop, p x
a : α
rw : ∀ (h : ¬∀ᶠ (x : α) in atTop, ¬p x) (a : α), ∃ (b : α), a ≤ b ∧ p b
⊢ ∃ (b : α), a ≤ b ∧ p b

Tactic:
rw [Filter.Frequently] at h

Premises used: Filter.Frequently
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
h : ¬∀ᶠ (x : α) in atTop, ¬p x
a : α
contrapose! : ∀ (h : ∀ (b : α) (_ : a ≤ b), ¬p b), ∀ᶠ (x : α) in atTop, ¬p x
⊢ ∃ (b : α), a ≤ b ∧ p b

Tactic:
contrapose! h
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
a : α
h : ∀ (b : α) (_ : a ≤ b), ¬p b
⊢ ∀ᶠ (x : α) in atTop, ¬p x

Tactic:
(eventually_ge_atTop a).mono h

Premises used: Filter.Eventually.mono, Filter.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
a : α
h : ∀ (b : α) (_ : a ≤ b), ¬p b
⊢ ∀ᶠ (x : α) in atTop, ¬p x

Tactic:
exact (eventually_ge_atTop a).mono h

Premises used: Filter.Eventually.mono, Filter.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
rw : generate (range Ici) = generate (Ici '' s)
⊢ atTop = generate (Ici '' s)

Tactic:
rw [atTop_eq_generate_Ici]

Premises used: Filter.atTop_eq_generate_Ici
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
a : generate (range Ici) ≤ generate (Ici '' s)
a₁ : generate (Ici '' s) ≤ generate (range Ici)
⊢ generate (range Ici) = generate (Ici '' s)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
a : Ici '' s ⊆ sets (generate (range Ici))
⊢ generate (range Ici) ≤ generate (Ici '' s)

Tactic:
rw [le_generate_iff]

Premises used: Filter.le_generate_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
y : α
⊢ Membership.mem (γ := Set (Set α)) (sets (generate (range Ici))) (Ici y)

Tactic:
mem_generate_of_mem ⟨y, rfl⟩

Premises used: Filter.mem_generate_of_mem, Exists.intro, rfl
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
y : α
⊢ Membership.mem (γ := Set (Set α)) (sets (generate (range Ici))) (Ici y)

Tactic:
exact mem_generate_of_mem ⟨y, rfl⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
a : range Ici ⊆ (generate (Ici '' s)).sets
⊢ generate (Ici '' s) ≤ generate (range Ici)

Tactic:
rw [le_generate_iff]

Premises used: Filter.le_generate_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x : α
a : ∀ (y : α) (ys : y ∈ s) (hy : x ≤ y), Ici x ∈ (generate (Ici '' s)).sets
⊢ Ici x ∈ (generate (Ici '' s)).sets

Tactic:
rcases hs x with ⟨y, ys, hy⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
x y : α
ys : y ∈ s
hy : x ≤ y
⊢ Ici y ∈ generate (Ici '' s)

Tactic:
have A : Ici y ∈ generate (Ici '' s) := mem_generate_of_mem (mem_image_of_mem _ ys)
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
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 y ⊆ Ici x

Tactic:
have B : Ici y ⊆ Ici x := Ici_subset_Ici.2 hy
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
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)
B : Ici y ⊆ Ici x
⊢ Ici x ∈ (generate (Ici '' s)).sets

Tactic:
sets_of_superset (generate (Ici '' s)) A B

Premises used: Set.Ici, Filter.sets_of_superset, Set.image, Filter.generate
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
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)
B : Ici y ⊆ Ici x
⊢ Ici x ∈ (generate (Ici '' s)).sets

Tactic:
exact sets_of_superset (generate (Ici '' s)) A B

Premises used: Set.Ici, Filter.sets_of_superset, Set.image, Filter.generate
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ atTop = generate (Ici '' s)

Tactic:
atTop_eq_generate_of_forall_exists_le fun x ↦ ?_

Premises used: Filter.atTop_eq_generate_of_forall_exists_le
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
hs : ¬BddAbove s
refine : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ atTop = generate (Ici '' s)

Tactic:
refine atTop_eq_generate_of_forall_exists_le fun x ↦ ?_

Premises used: Filter.atTop_eq_generate_of_forall_exists_le
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
hs : ¬BddAbove s
x : α
obtain : ∀ (y : α) (hy : y ∈ s) (hy' : x < y), ∃ y ∈ s, x ≤ y
⊢ ∃ y ∈ s, x ≤ y

Tactic:
obtain ⟨y, hy, hy'⟩ := not_bddAbove_iff.mp hs x

Premises used: Iff.mp, not_bddAbove_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
hs : ¬BddAbove s
x y : α
hy : y ∈ s
hy' : x < y
⊢ ∃ y ∈ s, x ≤ y

Tactic:
⟨y, hy, hy'.le⟩

Premises used: LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
Goal:
α : Type u_3
inst : LinearOrder α
s : Set α
hs : ¬BddAbove s
x y : α
hy : y ∈ s
hy' : x < y
⊢ ∃ y ∈ s, x ≤ y

Tactic:
exact ⟨y, hy, hy'.le⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
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 : α
inl :
  ∀ (i : ι) (hi : a ∈ s i),
    ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a
inr :
  ∀ (ha : ¬∃ (i : ι), a ∈ s i),
    ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a
⊢ ∀ᶠ (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

Premises used: Membership.mem, Exists, em
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
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 : ι
hi : a ∈ s i
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a

Tactic:
(eventually_ge_atTop i).mono fun j hij ↦ ?_

Premises used: Filter.Eventually.mono, Filter.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
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 : ι
hi : a ∈ s i
inl : ∀ (j : ι) (hij : i ≤ j), (s j).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a

Tactic:
refine (eventually_ge_atTop i).mono fun j hij ↦ ?_

Premises used: Filter.Eventually.mono, Filter.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
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 : ι
hi : a ∈ s i
j : ι
hij : i ≤ j
⊢ (s j).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a

Tactic:
simp only [Set.piecewise_eq_of_mem, hs hij hi, subset_iUnion _ _ hi]

Premises used: Set.piecewise_eq_of_mem, Set.subset_iUnion
-- Module: Mathlib.Order.Filter.AtTopBot.Defs
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 : α
ha : ¬∃ (i : ι), a ∈ s i
inr : ∀ (i : ι), (s i).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise (β := β) f g a = piecewise (β := β) (⋃ (i : ι), s i) f g a

Tactic:
filter_upwards with i