awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : IsOrderedCancelAddMonoid R
inst_3 : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
refine : ∀ (s : R), ∀ᶠ (a : α) in l, s ≤ f a • r
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x • r) l atTop

Tactic:
refine tendsto_atTop.mpr fun s => ?_

Premises used: Iff.mpr, Filter.tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : IsOrderedCancelAddMonoid R
inst_3 : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
s : R
obtain : ∀ (n : ℕ) (hn : s ≤ n • r), ∀ᶠ (a : α) in l, s ≤ f a • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Tactic:
obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr

Premises used: Archimedean.arch
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : IsOrderedCancelAddMonoid R
inst_3 : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Tactic:
(tendsto_atTop.mp hf n).mono fun a ha => hn.trans (nsmul_le_nsmul_left hr.le ha)

Premises used: LT.lt.le, Filter.tendsto_atTop, nsmul_le_nsmul_left, Filter.Eventually.mono, Iff.mp, LE.le.trans
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommMonoid R
inst_1 : LinearOrder R
inst_2 : IsOrderedCancelAddMonoid R
inst_3 : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Tactic:
exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (nsmul_le_nsmul_left hr.le ha)

Premises used: LT.lt.le, Filter.tendsto_atTop, nsmul_le_nsmul_left, Filter.Eventually.mono, Iff.mp, LE.le.trans
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℕ
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x • r) l atBot

Tactic:
simpa using hf.atTop_nsmul_const (neg_pos.2 hr)

Premises used: Iff.mpr, neg_pos, Filter.Tendsto.atTop_nsmul_const
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x • r) l atTop

Tactic:
tendsto_atTop.mpr fun s => ?_

Premises used: Iff.mpr, Filter.tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
refine : ∀ (s : R), ∀ᶠ (a : α) in l, s ≤ f a • r
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x • r) l atTop

Tactic:
refine tendsto_atTop.mpr fun s => ?_

Premises used: Iff.mpr, Filter.tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
obtain : ∀ (n : ℕ) (hn : s ≤ n • r), ∀ᶠ (a : α) in l, s ≤ f a • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Tactic:
obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr

Premises used: Archimedean.arch
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ s ≤ HSMul.hSMul (α := ℤ) (↑n : ℤ) r

Tactic:
simpa
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ s ≤ HSMul.hSMul (α := ℤ) (↑n : ℤ) r

Tactic:
replace hn : s ≤ (n : ℤ) • r := by simpa
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ HSMul.hSMul (α := ℤ) (↑n : ℤ) r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Tactic:
(tendsto_atTop.mp hf n).mono fun a ha => hn.trans (zsmul_le_zsmul_left hr.le ha)

Premises used: zsmul_le_zsmul_left, LT.lt.le, Filter.tendsto_atTop, Nat.cast, Filter.Eventually.mono, Iff.mp, LE.le.trans
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ HSMul.hSMul (α := ℤ) (↑n : ℤ) r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Tactic:
exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (zsmul_le_zsmul_left hr.le ha)

Premises used: zsmul_le_zsmul_left, LT.lt.le, Filter.tendsto_atTop, Nat.cast, Filter.Eventually.mono, Iff.mp, LE.le.trans
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x • r) l atBot

Tactic:
simpa using hf.atTop_zsmul_const (neg_pos.2 hr)

Premises used: Iff.mpr, neg_pos, Filter.Tendsto.atTop_zsmul_const
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atBot
simp :
  ∀ (hf : Tendsto (β := ℤ) (fun (x : α) ↦ -f x) l atTop), Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ -f x • r) l atTop
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x • r) l atBot

Tactic:
simp only [← tendsto_neg_atTop_iff, ← neg_zsmul] at hf ⊢

Premises used: neg_zsmul, Filter.tendsto_neg_atTop_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto (β := ℤ) (fun (x : α) ↦ -f x) l atTop
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ -f x • r) l atTop

Tactic:
hf.atTop_zsmul_const hr

Premises used: Filter.Tendsto.atTop_zsmul_const
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto (β := ℤ) (fun (x : α) ↦ -f x) l atTop
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ -f x • r) l atTop

Tactic:
exact hf.atTop_zsmul_const hr

Premises used: Filter.Tendsto.atTop_zsmul_const
-- Module: Mathlib.Order.Filter.AtTopBot.Archimedean
Goal:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst : AddCommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
f : α → ℤ
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ f x • r) l atTop

Tactic:
simpa using hf.atBot_zsmul_const (neg_pos.2 hr)

Premises used: Iff.mpr, neg_pos, Filter.Tendsto.atBot_zsmul_const
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
⊢ HasAntitoneBasis.{u_3, u_3} (α := α) atTop Ici

Tactic:
.iInf_principal fun _ _ ↦ Ici_subset_Ici.2

Premises used: Iff.mpr, Filter.HasAntitoneBasis.iInf_principal, Set.Ici_subset_Ici, Filter.atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
⊢ HasBasis atTop (fun (x : α) ↦ True) Ici

Tactic:
hasAntitoneBasis_atTop.1

Premises used: Filter.HasAntitoneBasis.toHasBasis, Filter.hasAntitoneBasis_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
inst_3 : NoMaxOrder α
⊢ HasBasis atTop (fun (x : α) ↦ True) Ioi

Tactic:
atTop_basis.to_hasBasis (fun a ha => ⟨a, ha, Ioi_subset_Ici_self⟩) fun a ha =>
    (exists_gt a).imp fun _b hb => ⟨ha, Ici_subset_Ioi.2 hb⟩

Premises used: Iff.mpr, Filter.atTop_basis, Set.Ioi_subset_Ici_self, NoMaxOrder.exists_gt, Exists.imp, And.intro, Exists.intro, Filter.HasBasis.to_hasBasis, Set.Ici_subset_Ioi
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
⊢ Nonempty α

Tactic:
have : Nonempty α := ⟨a⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
this : Nonempty α
⊢ HasBasis atTop (fun (x : α) ↦ a < x) Ioi

Tactic:
atTop_basis_Ioi.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩

Premises used: trivial, Filter.atTop_basis_Ioi, Set.Subset.rfl, And.intro, Exists.intro, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
this : Nonempty α
refine : ∀ (b : α), True → ∃ (i' : α), a < i' ∧ Ioi i' ⊆ Ioi b
⊢ HasBasis atTop (fun (x : α) ↦ a < x) Ioi

Tactic:
refine atTop_basis_Ioi.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩

Premises used: trivial, Filter.atTop_basis_Ioi, Set.Subset.rfl, And.intro, Exists.intro, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
this : Nonempty α
b : α
h : True
obtain : ∀ (c : α) (hac : a ≤ c) (hbc : b ≤ c), ∃ (i' : α), a < i' ∧ Ioi i' ⊆ Ioi b
⊢ ∃ (i' : α), a < i' ∧ Ioi i' ⊆ Ioi b

Tactic:
obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b

Premises used: exists_ge_ge
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
this : Nonempty α
b : α
h : True
c : α
hac : a ≤ c
hbc : b ≤ c
obtain : ∀ (d : α) (hcd : c < d), ∃ (i' : α), a < i' ∧ Ioi i' ⊆ Ioi b
⊢ ∃ (i' : α), a < i' ∧ Ioi i' ⊆ Ioi b

Tactic:
obtain ⟨d, hcd⟩ := exists_gt c

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
this : Nonempty α
b : α
h : True
c : α
hac : a ≤ c
hbc : b ≤ c
d : α
hcd : c < d
⊢ ∃ (i' : α), a < i' ∧ Ioi i' ⊆ Ioi b

Tactic:
⟨d, hac.trans_lt hcd, Ioi_subset_Ioi (hbc.trans hcd.le)⟩

Premises used: LT.lt.le, And.intro, Exists.intro, Set.Ioi_subset_Ioi, LE.le.trans, LE.le.trans_lt
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
this : Nonempty α
b : α
h : True
c : α
hac : a ≤ c
hbc : b ≤ c
d : α
hcd : c < d
⊢ ∃ (i' : α), a < i' ∧ Ioi i' ⊆ Ioi b

Tactic:
exact ⟨d, hac.trans_lt hcd, Ioi_subset_Ioi (hbc.trans hcd.le)⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
⊢ Nonempty α

Tactic:
have : Nonempty α := ⟨a⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
this : Nonempty α
⊢ HasBasis atTop (fun (x : α) ↦ a ≤ x) Ici

Tactic:
atTop_basis.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩

Premises used: Filter.atTop_basis, trivial, Set.Subset.rfl, And.intro, Exists.intro, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
this : Nonempty α
refine : ∀ (b : α), True → ∃ (i' : α), a ≤ i' ∧ Ici i' ⊆ Ici b
⊢ HasBasis atTop (fun (x : α) ↦ a ≤ x) Ici

Tactic:
refine atTop_basis.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩

Premises used: Filter.atTop_basis, trivial, Set.Subset.rfl, And.intro, Exists.intro, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
this : Nonempty α
b : α
h : True
obtain : ∀ (c : α) (hac : a ≤ c) (hbc : b ≤ c), ∃ (i' : α), a ≤ i' ∧ Ici i' ⊆ Ici b
⊢ ∃ (i' : α), a ≤ i' ∧ Ici i' ⊆ Ici b

Tactic:
obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b

Premises used: exists_ge_ge
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
this : Nonempty α
b : α
h : True
c : α
hac : a ≤ c
hbc : b ≤ c
⊢ ∃ (i' : α), a ≤ i' ∧ Ici i' ⊆ Ici b

Tactic:
⟨c, hac, Ici_subset_Ici.2 hbc⟩

Premises used: Iff.mpr, Set.Ici_subset_Ici, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
this : Nonempty α
b : α
h : True
c : α
hac : a ≤ c
hbc : b ≤ c
⊢ ∃ (i' : α), a ≤ i' ∧ Ici i' ⊆ Ici b

Tactic:
exact ⟨c, hac, Ici_subset_Ici.2 hbc⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
⊢ NeBot.{u_3} (α := α) atTop

Tactic:
atTop_basis.neBot_iff.2 fun _ => nonempty_Ici

Premises used: Iff.mpr, Filter.atTop_basis, Filter.HasBasis.neBot_iff, Set.nonempty_Ici
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_6
inst : Preorder α
⊢ NeBot.{u_6} (α := α) atTop ↔ Nonempty α ∧ IsDirectedOrder α

Tactic:
⟨fun h ↦ ⟨nonempty_of_neBot atTop, ⟨fun x y ↦ ?_⟩⟩, fun ⟨h₁, h₂⟩ ↦ atTop_neBot⟩

Premises used: Filter.NeBot, Filter.atTop_neBot, Filter.nonempty_of_neBot, Filter.atTop, IsDirected.mk, And.intro, Iff.intro, _private.0.Filter.atTop_neBot_iff.match_1
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_6
inst : Preorder α
refine : ∀ (h : NeBot.{u_6} (α := α) atTop) (x y : α), ∃ (c : α), x ≤ c ∧ y ≤ c
⊢ NeBot.{u_6} (α := α) atTop ↔ Nonempty α ∧ IsDirectedOrder α

Tactic:
refine ⟨fun h ↦ ⟨nonempty_of_neBot atTop, ⟨fun x y ↦ ?_⟩⟩, fun ⟨h₁, h₂⟩ ↦ atTop_neBot⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_6
inst : Preorder α
h : NeBot.{u_6} (α := α) atTop
x y : α
⊢ ∃ (c : α), x ≤ c ∧ y ≤ c

Tactic:
((eventually_ge_atTop x).and (eventually_ge_atTop y)).exists

Premises used: Filter.Eventually.and, Filter.Eventually.exists, Filter.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_6
inst : Preorder α
h : NeBot.{u_6} (α := α) atTop
x y : α
⊢ ∃ (c : α), x ≤ c ∧ y ≤ c

Tactic:
exact ((eventually_ge_atTop x).and (eventually_ge_atTop y)).exists

Premises used: Filter.Eventually.and, Filter.Eventually.exists, Filter.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_6
inst : Preorder α
⊢ NeBot.{u_6} (α := α) atBot ↔ Nonempty α ∧ IsCodirectedOrder α

Tactic:
atTop_neBot_iff (α := αᵒᵈ)

Premises used: setOf, Filter.atBot, Set.Iic, Filter.atTop_neBot_iff, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
s : Set α
⊢ Membership.mem (γ := Filter α) atTop s ↔ ∃ (a : α), ∀ b ≥ a, b ∈ s

Tactic:
atTop_basis.mem_iff.trans <| exists_congr fun _ => iff_of_eq (true_and _)

Premises used: Filter.atTop_basis, Set.Ici, Filter.HasBasis.mem_iff, HasSubset.Subset, exists_congr, Iff.trans, true_and, iff_of_eq
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
p : α → Prop
inst_2 : Nonempty α
⊢ (∀ᶠ (x : α) in atTop, p x) ↔ ∃ (a : α), ∀ b ≥ a, p b

Tactic:
mem_atTop_sets

Premises used: Set.Mem, Filter.mem_atTop_sets, Filter.Eventually, setOf
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
p : α → Prop
inst_2 : Nonempty α
⊢ (∀ (i : α), True → ∃ x ∈ Ici i, p x) ↔ ∀ (a : α), ∃ b ≥ a, p b

Tactic:
simp
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
r : α → β → Prop
simp_rw : (∃ (a : α) (b : β), ∀ b_1 ≥ a, r b_1 b) ↔ ∃ (a : α), ∀ b ≥ a, ∃ (b_1 : β), ∀ a ≥ b, r a b_1
⊢ (∃ (b : β), ∀ᶠ (a : α) in atTop, r a b) ↔ ∀ᶠ (a₀ : α) in atTop, ∃ (b : β), ∀ a ≥ a₀, r a b

Tactic:
simp_rw [eventually_atTop, ← exists_comm (α := α)]

Premises used: exists_comm, Filter.eventually_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
r : α → β → Prop
⊢ (∃ (a : α) (b : β), ∀ b_1 ≥ a, r b_1 b) ↔ ∃ (a : α), ∀ b ≥ a, ∃ (b_1 : β), ∀ a ≥ b, r a b_1

Tactic:
exists_congr fun a ↦ .symm <| forall_ge_iff <| Monotone.exists fun _ _ _ hb H n hn ↦
    H n (hb.trans hn)

Premises used: Monotone.exists, exists_congr, LE.le.trans, Iff.symm, forall_ge_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
r : α → β → Prop
⊢ (∃ (a : α) (b : β), ∀ b_1 ≥ a, r b_1 b) ↔ ∃ (a : α), ∀ b ≥ a, ∃ (b_1 : β), ∀ a ≥ b, r a b_1

Tactic:
exact exists_congr fun a ↦ .symm <| forall_ge_iff <| Monotone.exists fun _ _ _ hb H n hn ↦
    H n (hb.trans hn)
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Nonempty α
f : α → β
⊢ map f atTop = ⨅ (a : α), 𝓟 (f '' {a' : α | a ≤ a'})

Tactic:
(atTop_basis.map f).eq_iInf

Premises used: Filter.atTop_basis, Set.Ici, Filter.HasBasis.map, Filter.HasBasis.eq_iInf
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
p : α → Prop
inst_2 : Nonempty α
inst_3 : NoMaxOrder α
⊢ (∀ (i : α), True → ∃ x ∈ Ioi i, p x) ↔ ∀ (a : α), ∃ b > a, p b

Tactic:
simp
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsCodirectedOrder α
inst_2 : Nonempty α
inst_3 : NoMinOrder α
⊢ HasBasis atBot (fun (x : α) ↦ True) Iio

Tactic:
atTop_basis_Ioi (α := αᵒᵈ)

Premises used: setOf, Filter.atTop_basis_Ioi, Filter.atBot, Set.Iic, OrderDual, Set.Iio
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsCodirectedOrder α
inst_2 : NoMinOrder α
a : α
⊢ HasBasis atBot (fun (x : α) ↦ x < a) Iio

Tactic:
atTop_basis_Ioi' (α := αᵒᵈ) a

Premises used: setOf, Filter.atTop_basis_Ioi', Filter.atBot, Set.Iic, OrderDual, Set.Iio
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsCodirectedOrder α
a : α
⊢ HasBasis atBot (fun (x : α) ↦ x ≤ a) Iic

Tactic:
atTop_basis' (α := αᵒᵈ) _

Premises used: setOf, Filter.atBot, Set.Iic, Filter.atTop_basis', OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsCodirectedOrder α
inst_2 : Nonempty α
⊢ HasBasis atBot (fun (x : α) ↦ True) Iic

Tactic:
atTop_basis (α := αᵒᵈ)

Premises used: Filter.atTop_basis, setOf, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsCodirectedOrder α
inst_2 : Nonempty α
⊢ NeBot.{u_3} (α := α) atBot

Tactic:
atTop_neBot (α := αᵒᵈ)

Premises used: setOf, Filter.atTop_neBot, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsCodirectedOrder α
inst_2 : Nonempty α
s : Set α
⊢ Membership.mem (γ := Filter α) atBot s ↔ ∃ (a : α), ∀ b ≤ a, b ∈ s

Tactic:
mem_atTop_sets (α := αᵒᵈ)

Premises used: Set.Mem, Filter.mem_atTop_sets, setOf, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsCodirectedOrder α
p : α → Prop
inst_2 : Nonempty α
⊢ (∀ᶠ (x : α) in atBot, p x) ↔ ∃ (a : α), ∀ b ≤ a, p b

Tactic:
mem_atBot_sets

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.mem_atBot_sets
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsCodirectedOrder α
p : α → Prop
inst_2 : Nonempty α
⊢ (∃ᶠ (x : α) in atBot, p x) ↔ ∀ (a : α), ∃ b ≤ a, p b

Tactic:
frequently_atTop (α := αᵒᵈ)

Premises used: Filter.frequently_atTop, setOf, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsCodirectedOrder α
inst_2 : Nonempty α
r : α → β → Prop
⊢ (∃ (b : β), ∀ᶠ (a : α) in atBot, r a b) ↔ ∀ᶠ (a₀ : α) in atBot, ∃ (b : β), ∀ a ≤ a₀, r a b

Tactic:
exists_eventually_atTop (α := αᵒᵈ)

Premises used: Filter.exists_eventually_atTop, setOf, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsCodirectedOrder α
inst_2 : Nonempty α
f : α → β
⊢ map f atBot = ⨅ (a : α), 𝓟 (f '' {a' : α | a' ≤ a})

Tactic:
map_atTop_eq (α := αᵒᵈ)

Premises used: setOf, Filter.map_atTop_eq, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsCodirectedOrder α
p : α → Prop
inst_2 : Nonempty α
inst_3 : NoMinOrder α
⊢ (∃ᶠ (x : α) in atBot, p x) ↔ ∀ (a : α), ∃ b < a, p b

Tactic:
frequently_atTop' (α := αᵒᵈ)

Premises used: Filter.frequently_atTop', setOf, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
P : ℕ → Prop
h : ∃ᶠ (n : ℕ) in atTop, P n
⊢ ∀ (a : ℕ), ∃ b > a, P b

Tactic:
rw [frequently_atTop'] at h

Premises used: Filter.frequently_atTop'
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
P : ℕ → Prop
h : ∀ (a : ℕ), ∃ b > a, P b
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
Nat.exists_strictMono_subsequence h

Premises used: Nat.exists_strictMono_subsequence
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
P : ℕ → Prop
h : ∀ (a : ℕ), ∃ b > a, P b
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
exact Nat.exists_strictMono_subsequence h

Premises used: Nat.exists_strictMono_subsequence
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
P : ℕ → Prop
h : ∀ᶠ (n : ℕ) in atTop, P n
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
extraction_of_frequently_atTop h.frequently

Premises used: Filter.extraction_of_frequently_atTop, Filter.Eventually.frequently
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
P : ℕ → ℕ → Prop
h : ∀ (n : ℕ), ∃ᶠ (k : ℕ) in atTop, P n k
⊢ ∀ (n a : ℕ), ∃ b > a, P n b

Tactic:
simp only [frequently_atTop'] at h

Premises used: Filter.frequently_atTop'
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
P : ℕ → ℕ → Prop
h : ∀ (n a : ℕ), ∃ b > a, P n b
choose :
  ∀ (u : (n a : ℕ) → ℕ) (hu : ∀ (n a : ℕ), u n a > a) (hu' : ∀ (n a : ℕ), P n (u n a)),
    ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)

Tactic:
choose u hu hu' using h
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
P : ℕ → ℕ → Prop
u : (n a : ℕ) → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
h :
  (StrictMono (β := ℕ) fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v) ∧
    ∀ (n : ℕ), P n ((fun (n : ℕ) ↦ (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v : ℕ)) n)
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)

Tactic:
use (fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v : ℕ → ℕ)

Premises used: Nat.recOn
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
P : ℕ → ℕ → Prop
u : (n a : ℕ) → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
h : StrictMono (β := ℕ) fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v
h₁ : ∀ (n : ℕ), P n (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v)
⊢ (StrictMono (β := ℕ) fun (n : ℕ) ↦ Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v) ∧
    ∀ (n : ℕ), P n ((fun (n : ℕ) ↦ (Nat.recOn (motive := fun (x : ℕ) ↦ ℕ) n (u 0 0) fun (n v : ℕ) ↦ u (n + 1) v : ℕ)) n)

Tactic:
constructor