awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
hr : r < 0
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
simp [hr, hr.not_gt, tendsto_const_mul_atTop_of_neg]

Premises used: Filter.tendsto_const_mul_atTop_of_neg, LT.lt.not_gt
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
inst_3 : l.NeBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ 0 * f x) l atTop ↔
    LT.lt.{u_1} (α := α) 0 0 ∧ Tendsto f l atTop ∨ LT.lt.{u_1} (α := α) 0 0 ∧ Tendsto f l atBot

Tactic:
simp [not_tendsto_const_atTop]

Premises used: Filter.not_tendsto_const_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
hr : 0 < r
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
simp [hr, hr.not_gt, tendsto_const_mul_atTop_of_pos]

Premises used: LT.lt.not_gt, Filter.tendsto_const_mul_atTop_of_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atTop_iff]

Premises used: mul_comm, Filter.tendsto_const_mul_atTop_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x / r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atTop_iff]

Premises used: Filter.tendsto_mul_const_atTop_iff, div_eq_mul_inv
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

Tactic:
simp only [← tendsto_neg_atTop_iff, ← mul_neg, tendsto_const_mul_atTop_iff, neg_neg]

Premises used: neg_neg, Filter.tendsto_neg_atTop_iff, mul_neg, Filter.tendsto_const_mul_atTop_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atBot_iff]

Premises used: Filter.tendsto_const_mul_atBot_iff, mul_comm
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x / r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atBot_iff]

Premises used: div_eq_mul_inv, Filter.tendsto_mul_const_atBot_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop ↔ r < 0

Tactic:
simp [tendsto_const_mul_atTop_iff, h, h.not_tendsto disjoint_atBot_atTop]

Premises used: Filter.disjoint_atBot_atTop, Filter.Tendsto.not_tendsto, Filter.tendsto_const_mul_atTop_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * r) l atTop ↔ r < 0

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atTop_iff_neg h]

Premises used: Filter.tendsto_const_mul_atTop_iff_neg, mul_comm
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x / r) l atTop ↔ r < 0

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atTop_iff_neg h]

Premises used: Filter.tendsto_mul_const_atTop_iff_neg, div_eq_mul_inv
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atBot ↔ 0 < r

Tactic:
simp [tendsto_const_mul_atBot_iff, h, h.not_tendsto disjoint_atBot_atTop]

Premises used: Filter.tendsto_const_mul_atBot_iff, Filter.disjoint_atBot_atTop, Filter.Tendsto.not_tendsto
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * r) l atBot ↔ 0 < r

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atBot_iff_pos h]

Premises used: mul_comm, Filter.tendsto_const_mul_atBot_iff_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x / r) l atBot ↔ 0 < r

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atBot_iff_pos h]

Premises used: div_eq_mul_inv, Filter.tendsto_mul_const_atBot_iff_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atBot ↔ r < 0

Tactic:
simp [tendsto_const_mul_atBot_iff, h, h.not_tendsto disjoint_atTop_atBot]

Premises used: Filter.tendsto_const_mul_atBot_iff, Filter.Tendsto.not_tendsto, Filter.disjoint_atTop_atBot
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * r) l atBot ↔ r < 0

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atBot_iff_neg h]

Premises used: Filter.tendsto_const_mul_atBot_iff_neg, mul_comm
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst_3 : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x / r) l atBot ↔ r < 0

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atBot_iff_neg h]

Premises used: div_eq_mul_inv, Filter.tendsto_mul_const_atBot_iff_neg
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atBot

Tactic:
(tendsto_const_mul_atBot_of_neg hr).2 hf

Premises used: Iff.mpr, Filter.tendsto_const_mul_atBot_of_neg
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * r) l atBot

Tactic:
(tendsto_mul_const_atBot_of_neg hr).2 hf

Premises used: Iff.mpr, Filter.tendsto_mul_const_atBot_of_neg
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x / r) l atBot

Tactic:
(tendsto_div_const_atBot_of_neg hr).2 hf

Premises used: Iff.mpr, Filter.tendsto_div_const_atBot_of_neg
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
hf : Tendsto f l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atBot

Tactic:
(tendsto_const_mul_atBot_of_pos hr).2 hf

Premises used: Iff.mpr, Filter.tendsto_const_mul_atBot_of_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
hf : Tendsto f l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * r) l atBot

Tactic:
(tendsto_mul_const_atBot_of_pos hr).2 hf

Premises used: Iff.mpr, Filter.tendsto_mul_const_atBot_of_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : 0 < r
hf : Tendsto f l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x / r) l atBot

Tactic:
(tendsto_div_const_atBot_of_pos hr).2 hf

Premises used: Iff.mpr, Filter.tendsto_div_const_atBot_of_pos
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ r * f x) l atTop

Tactic:
(tendsto_const_mul_atTop_of_neg hr).2 hf

Premises used: Iff.mpr, Filter.tendsto_const_mul_atTop_of_neg
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * r) l atTop

Tactic:
(tendsto_mul_const_atTop_of_neg hr).2 hf

Premises used: Iff.mpr, Filter.tendsto_mul_const_atTop_of_neg
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
n : ℕ
hn : n ≠ 0
hc : c < 0
⊢ Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atBot

Tactic:
(tendsto_pow_atTop hn).const_mul_atTop_of_neg hc

Premises used: Filter.Tendsto.const_mul_atTop_of_neg, Filter.tendsto_pow_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Field
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
c : α
n : ℕ
⊢ Tendsto (β := α) (fun (x : α) ↦ c * x ^ n) atTop atBot ↔ n ≠ 0 ∧ c < 0

Tactic:
simp only [← tendsto_neg_atTop_iff, ← neg_mul, tendsto_const_mul_pow_atTop_iff, neg_pos]

Premises used: neg_pos, Filter.tendsto_const_mul_pow_atTop_iff, neg_mul, Filter.tendsto_neg_atTop_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
⊢ (∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in atTop, p x

Tactic:
⟨fun h ↦ h.mono fun x hx ↦ hx x le_rfl, fun h ↦ ?_⟩

Premises used: le_rfl, Filter.Eventually.mono, Iff.intro
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
refine : ∀ (h : ∀ᶠ (x : α) in atTop, p x), ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
⊢ (∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in atTop, p x

Tactic:
refine ⟨fun h ↦ h.mono fun x hx ↦ hx x le_rfl, fun h ↦ ?_⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
rcases :
  ∀ (S : Set α) (hSf : S.Finite) (hS : ∀ ⦃x : α⦄, Membership.mem (γ := Set α) (⋂ i ∈ S, Ici i) x → p x),
    ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y

Tactic:
rcases (hasBasis_iInf_principal_finite _).eventually_iff.1 h with ⟨S, hSf, hS⟩

Premises used: Filter.hasBasis_iInf_principal_finite, Iff.mp, Filter.HasBasis.eventually_iff
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
hS : ∀ ⦃x : α⦄, Membership.mem (γ := Set α) (⋂ i ∈ S, Ici i) x → p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y

Tactic:
mem_iInf_of_iInter hSf (V := fun x ↦ Ici x.1) (fun _ ↦ Subset.rfl) fun x hx y hy ↦ ?_

Premises used: Set.Mem, Filter.Eventually, Filter.mem_iInf_of_iInter, Set.Subset.rfl
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
hS : ∀ ⦃x : α⦄, Membership.mem (γ := Set α) (⋂ i ∈ S, Ici i) x → p x
refine :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) (⋂ (i : (↑S : Type u_3)), (fun (x : (↑S : Type u_3)) ↦ Ici (↑x : α)) i) x)
    (y : α) (hy : x ≤ y), p y
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y

Tactic:
refine mem_iInf_of_iInter hSf (V := fun x ↦ Ici x.1) (fun _ ↦ Subset.rfl) fun x hx y hy ↦ ?_
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
hS : ∀ ⦃x : α⦄, Membership.mem (γ := Set α) (⋂ i ∈ S, Ici i) x → p x
x : α
hx : Membership.mem (γ := Set α) (⋂ (i : (↑S : Type u_3)), (fun (x : (↑S : Type u_3)) ↦ Ici (↑x : α)) i) x
y : α
hy : x ≤ y
⊢ ∀ ⦃x : α⦄, (∀ (i : α) (i_1 : i ∈ S), x ∈ Ici i) → p x

Tactic:
simp only [mem_iInter] at hS hx

Premises used: Set.mem_iInter
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
hS : ∀ ⦃x : α⦄, Membership.mem (γ := Set α) (⋂ i ∈ S, Ici i) x → p x
x : α
hx : Membership.mem (γ := Set α) (⋂ (i : (↑S : Type u_3)), (fun (x : (↑S : Type u_3)) ↦ Ici (↑x : α)) i) x
y : α
hy : x ≤ y
hS₁ : ∀ ⦃x : α⦄, (∀ (i : α) (i_1 : i ∈ S), x ∈ Ici i) → p x
⊢ ∀ (i : (↑S : Type u_3)), x ∈ Ici (↑i : α)

Tactic:
simp only [mem_iInter] at hS hx

Premises used: Set.mem_iInter
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
x y : α
hy : x ≤ y
hS : ∀ ⦃x : α⦄, (∀ (i : α) (i_1 : i ∈ S), x ∈ Ici i) → p x
hx : ∀ (i : (↑S : Type u_3)), x ∈ Ici (↑i : α)
⊢ p y

Tactic:
hS fun z hz ↦ le_trans (hx ⟨z, hz⟩) hy

Premises used: Subtype.mk, le_trans
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
x y : α
hy : x ≤ y
hS : ∀ ⦃x : α⦄, (∀ (i : α) (i_1 : i ∈ S), x ∈ Ici i) → p x
hx : ∀ (i : (↑S : Type u_3)), x ∈ Ici (↑i : α)
⊢ p y

Tactic:
exact hS fun z hz ↦ le_trans (hx ⟨z, hz⟩) hy

Premises used: Subtype.mk, le_trans
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
inst : Preorder α
p : α → Prop
⊢ (∀ᶠ (x : α) in atBot, ∀ y ≤ x, p y) ↔ ∀ᶠ (x : α) in atBot, p x

Tactic:
eventually_forall_ge_atTop (α := αᵒᵈ)

Premises used: setOf, Filter.atBot, Set.Iic, OrderDual, Filter.eventually_forall_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, p x
⊢ ∀ᶠ (x : β) in atBot, ∀ y ≤ x, p y

Tactic:
rw [← Filter.eventually_forall_le_atBot] at h_evtl

Premises used: Filter.eventually_forall_le_atBot
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, ∀ y ≤ x, p y
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y

Tactic:
(h_evtl.comap f).filter_mono hf.le_comap

Premises used: Filter.Tendsto.le_comap, Filter.Eventually.filter_mono, Filter.Eventually.comap
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
p : β → Prop
f : α → β
hf : Tendsto f l atBot
h_evtl : ∀ᶠ (x : β) in atBot, ∀ y ≤ x, p y
⊢ ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y

Tactic:
exact (h_evtl.comap f).filter_mono hf.le_comap

Premises used: Filter.Tendsto.le_comap, Filter.Eventually.filter_mono, Filter.Eventually.comap
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N : ℕ
⊢ ∃ k ≤ N, ∀ l ≤ N, u l ≤ u k

Tactic:
exists_max_image _ u (finite_le_nat N) ⟨N, le_refl N⟩

Premises used: le_refl, Set.Mem, Set.exists_max_image, Exists.intro, Set.finite_le_nat
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N : ℕ
obtain : ∀ (k : ℕ) (hku : ∀ l ≤ N, u l ≤ u k), ∃ n ≥ N, ∀ k < n, u k < u n
⊢ ∃ n ≥ N, ∀ k < n, u k < u n

Tactic:
obtain ⟨k : ℕ, - : k ≤ N, hku : ∀ l ≤ N, u l ≤ u k⟩ : ∃ k ≤ N, ∀ l ≤ N, u l ≤ u k :=
    exists_max_image _ u (finite_le_nat N) ⟨N, le_refl N⟩

Premises used: le_refl, Set.exists_max_image, Exists.intro, Set.finite_le_nat
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
⊢ ∃ n ≥ N, u k < u n

Tactic:
have ex : ∃ n ≥ N, u k < u n := exists_lt_of_tendsto_atTop hu _ _
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
rcases :
  ∀ (n : ℕ) (hn_min : ∀ m < n, ¬(m ≥ N ∧ u k < u m)) (hnN : n ≥ N) (hnk : u k < u n),
    ∃ n ≥ N, u k < u n ∧ ∀ m < n, N ≤ m → u m ≤ u k
⊢ ∃ n ≥ N, u k < u n ∧ ∀ m < n, N ≤ m → u m ≤ u k

Tactic:
rcases Nat.findX ex with ⟨n, ⟨hnN, hnk⟩, hn_min⟩

Premises used: Nat.findX
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
n : ℕ
hn_min : ∀ m < n, ¬(m ≥ N ∧ u k < u m)
hnN : n ≥ N
hnk : u k < u n
⊢ ∀ m < n, ∀ (_ : m ≥ N), u m ≤ u k

Tactic:
push Not at hn_min

Premises used: Not
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ m < n, ∀ (_ : m ≥ N), u m ≤ u k
⊢ ∃ n ≥ N, u k < u n ∧ ∀ m < n, N ≤ m → u m ≤ u k

Tactic:
⟨n, hnN, hnk, hn_min⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ m < n, ∀ (_ : m ≥ N), u m ≤ u k
⊢ ∃ n ≥ N, u k < u n ∧ ∀ m < n, N ≤ m → u m ≤ u k

Tactic:
exact ⟨n, hnN, hnk, hn_min⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
obtain : ∀ (n : ℕ) (hnN : n ≥ N) (hnk : u k < u n) (hn_min : ∀ m < n, N ≤ m → u m ≤ u k), ∃ n ≥ N, ∀ k < n, u k < u n
⊢ ∃ n ≥ N, ∀ k < n, u k < u n

Tactic:
obtain ⟨n : ℕ, hnN : n ≥ N, hnk : u k < u n, hn_min : ∀ m, m < n → N ≤ m → u m ≤ u k⟩ :
      ∃ n ≥ N, u k < u n ∧ ∀ m, m < n → N ≤ m → u m ≤ u k := by
    rcases Nat.findX ex with ⟨n, ⟨hnN, hnk⟩, hn_min⟩
    push Not at hn_min
    exact ⟨n, hnN, hnk, hn_min⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ m < n, N ≤ m → u m ≤ u k
right : ∀ k < n, u k < u n
⊢ ∃ n ≥ N, ∀ k < n, u k < u n

Tactic:
use n, hnN
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ m < n, N ≤ m → u m ≤ u k
⊢ ∀ k < n, u k < u n

Tactic:
grind
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMinOrder β
u : ℕ → β
hu : Tendsto u atTop atBot
⊢ ∀ (N : ℕ), ∃ n ≥ N, ∀ k < n, u n < u k

Tactic:
@high_scores βᵒᵈ _ _ _ hu

Premises used: Filter.high_scores
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
⊢ ∃ᶠ (n : ℕ) in atTop, ∀ k < n, u k < u n

Tactic:
simpa [frequently_atTop] using high_scores hu

Premises used: Filter.high_scores, Filter.frequently_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMinOrder β
u : ℕ → β
hu : Tendsto u atTop atBot
⊢ ∃ᶠ (n : ℕ) in atTop, ∀ k < n, u n < u k

Tactic:
@frequently_high_scores βᵒᵈ _ _ _ hu

Premises used: Filter.frequently_high_scores
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
β : Type u_4
inst : LinearOrder β
inst_1 : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ StrictMono (u ∘ φ)

Tactic:
let ⟨φ, h, h'⟩ := extraction_of_frequently_atTop (frequently_high_scores hu)
  ⟨φ, h, fun _ m hnm => h' m _ (h hnm)⟩

Premises used: StrictMono, Filter.frequently_high_scores, Function.comp, Exists, _private.0.Filter.strictMono_subseq_of_tendsto_atTop.match_1, Filter.extraction_of_frequently_atTop, And, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
u : ℕ → ℕ
hu : ∀ (n : ℕ), n ≤ u n
⊢ ∃ (φ : ℕ → ℕ), StrictMono φ ∧ StrictMono (u ∘ φ)

Tactic:
strictMono_subseq_of_tendsto_atTop (tendsto_atTop_mono hu tendsto_id)

Premises used: Filter.tendsto_id, Filter.tendsto_atTop_mono, Filter.strictMono_subseq_of_tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ k < n, ∀ᶠ (a : ℕ) in atTop, p (n * a + k)
simp : ∀ (hp : ∀ k < n, ∃ (a : ℕ), ∀ b ≥ a, p (n * b + k)), ∃ (a : ℕ), ∀ b ≥ a, p b
⊢ ∀ᶠ (a : ℕ) in atTop, p a

Tactic:
simp only [eventually_atTop] at hp ⊢

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ k < n, ∃ (a : ℕ), ∀ b ≥ a, p (n * b + k)
choose! : ∀ (N : (k : ℕ) → ℕ) (hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)), ∃ (a : ℕ), ∀ b ≥ a, p b
⊢ ∃ (a : ℕ), ∀ b ≥ a, p b

Tactic:
choose! N hN using hp
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : (k : ℕ) → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
⊢ ∃ (a : ℕ), ∀ b ≥ a, p b

Tactic:
⟨(Finset.range n).sup (n * N ·), fun b hb => ?_⟩

Premises used: HMul.hMul, Finset.range, Exists.intro, Finset.sup
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : (k : ℕ) → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
refine : ∀ (b : ℕ) (hb : b ≥ (Finset.range n).sup fun (x : ℕ) ↦ n * N x), p b
⊢ ∃ (a : ℕ), ∀ b ≥ a, p b

Tactic:
refine ⟨(Finset.range n).sup (n * N ·), fun b hb => ?_⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : (k : ℕ) → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun (x : ℕ) ↦ n * N x
rw : p (n * (b / n) + b % n)
⊢ p b

Tactic:
rw [← Nat.div_add_mod b n]

Premises used: Nat.div_add_mod
-- Module: Mathlib.Order.Filter.AtTopBot.Finite
Goal:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : (k : ℕ) → ℕ
hN : ∀ k < n, ∀ b ≥ N k, p (n * b + k)
b : ℕ
hb : b ≥ (Finset.range n).sup fun (x : ℕ) ↦ n * N x
have : ∀ (hlt : b % n < n), p (n * (b / n) + b % n)
⊢ p (n * (b / n) + b % n)

Tactic:
have hlt := Nat.mod_lt b hn.bot_lt