awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
⊢ Eq.{u_2 + 1} (α := Filter G) (map Inv.inv atTop) atBot

Tactic:
(OrderIso.inv G).map_atTop

Premises used: OrderIso.inv, setOf, Filter.atBot, Set.Iic, OrderDual, OrderIso.map_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
⊢ Eq.{u_2 + 1} (α := Filter G) (comap Inv.inv atBot) atTop

Tactic:
(OrderIso.inv G).comap_atTop

Premises used: OrderIso.comap_atTop, OrderIso.inv, setOf, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
⊢ Eq.{u_2 + 1} (α := Filter G) (comap Inv.inv atTop) atBot

Tactic:
(OrderIso.inv G).comap_atBot

Premises used: Set.Ici, OrderIso.inv, setOf, Filter.atTop, OrderIso.comap_atBot, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
⊢ Tendsto.{u_2, u_2} (α := G) Inv.inv atTop atBot

Tactic:
(OrderIso.inv G).tendsto_atTop

Premises used: OrderIso.inv, setOf, OrderIso.tendsto_atTop, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
⊢ Tendsto.{u_2, u_2} (α := G) Inv.inv atBot atTop

Tactic:
tendsto_inv_atTop_atBot (G := Gᵒᵈ)

Premises used: Set.Ici, Filter.tendsto_inv_atTop_atBot, setOf, Filter.atTop, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f : α → G
⊢ Tendsto.{u_1, u_2} (β := G) (fun (x : α) ↦ (f x)⁻¹) l atTop ↔ Tendsto f l atBot

Tactic:
(OrderIso.inv G).tendsto_atBot_iff

Premises used: Set.Ici, OrderIso.inv, setOf, Filter.atTop, OrderIso.tendsto_atBot_iff, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f : α → G
⊢ Tendsto.{u_1, u_2} (β := G) (fun (x : α) ↦ (f x)⁻¹) l atBot ↔ Tendsto f l atTop

Tactic:
(OrderIso.inv G).tendsto_atTop_iff

Premises used: OrderIso.tendsto_atTop_iff, OrderIso.inv, setOf, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f : G → α
⊢ Tendsto (fun (x : G) ↦ f x⁻¹) atTop l ↔ Tendsto f atBot l

Tactic:
simp [← Function.comp_def, Tendsto, ← map_map, map_inv_atTop]

Premises used: Filter.map_map, Filter.map_inv_atTop, Function.comp_def, Filter.Tendsto
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
α : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
l : Filter α
f : G → α
⊢ Tendsto (fun (x : G) ↦ f x⁻¹) atBot l ↔ Tendsto f atTop l

Tactic:
simp [← Function.comp_def, Tendsto, ← map_map, map_inv_atBot]

Premises used: Filter.map_map, Filter.map_inv_atBot, Function.comp_def, Filter.Tendsto
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
⊢ Tendsto.{u_2, u_2} (α := G) mabs atTop atTop

Tactic:
tendsto_atTop_mono le_mabs_self tendsto_id

Premises used: Filter.tendsto_id, Filter.tendsto_atTop_mono, le_mabs_self
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
⊢ Tendsto.{u_2, u_2} (α := G) mabs atBot atTop

Tactic:
tendsto_atTop_mono inv_le_mabs tendsto_inv_atBot_atTop

Premises used: inv_le_mabs, Filter.tendsto_atTop_mono, Filter.tendsto_inv_atBot_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
⊢ Eq.{u_2 + 1} (α := Filter G) (comap mabs atTop) (atBot ⊔ atTop)

Tactic:
le_antisymm (((atTop_basis.comap _).le_basis_iff (atBot_basis.sup atTop_basis)).2 ?_)
      (sup_le tendsto_mabs_atBot_atTop.le_comap tendsto_mabs_atTop_atTop.le_comap)

Premises used: Iff.mpr, Filter.Tendsto.le_comap, Filter.atTop_basis, Filter.tendsto_mabs_atTop_atTop, Filter.atBot_basis, Filter.HasBasis.le_basis_iff, Filter.tendsto_mabs_atBot_atTop, Filter.HasBasis.comap, le_antisymm, sup_le, Filter.HasBasis.sup
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
le_antisymm : ∀ (i' : G × G), True ∧ True → ∃ (i : G), True ∧ mabs ⁻¹' Ici i ⊆ Iic i'.1 ∪ Ici i'.2
⊢ Eq.{u_2 + 1} (α := Filter G) (comap mabs atTop) (atBot ⊔ atTop)

Tactic:
refine
    le_antisymm (((atTop_basis.comap _).le_basis_iff (atBot_basis.sup atTop_basis)).2 ?_)
      (sup_le tendsto_mabs_atBot_atTop.le_comap tendsto_mabs_atTop_atTop.le_comap)

Premises used: Iff.mpr, Filter.Tendsto.le_comap, Filter.atTop_basis, Filter.tendsto_mabs_atTop_atTop, Filter.atBot_basis, Filter.HasBasis.le_basis_iff, Filter.tendsto_mabs_atBot_atTop, Filter.HasBasis.comap, le_antisymm, sup_le, Filter.HasBasis.sup
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
⊢ ∃ (i : G), True ∧ mabs ⁻¹' Ici i ⊆ Iic (a, b).1 ∪ Ici (a, b).2

Tactic:
⟨max (a⁻¹) b, trivial, fun x hx => ?_⟩

Premises used: trivial, Inv.inv, Max.max, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
refine : ∀ (x : G) (hx : x ∈ mabs ⁻¹' Ici (max a⁻¹ b)), x ∈ Iic (a, b).1 ∪ Ici (a, b).2
⊢ ∃ (i : G), True ∧ mabs ⁻¹' Ici i ⊆ Iic (a, b).1 ∪ Ici (a, b).2

Tactic:
refine ⟨max (a⁻¹) b, trivial, fun x hx => ?_⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b x : G
hx : x ∈ mabs ⁻¹' Ici (max a⁻¹ b)
⊢ x ≤ a ∧ x ≤ b⁻¹ ∨ a⁻¹ ≤ x ∧ b ≤ x

Tactic:
rw [mem_preimage, mem_Ici, le_mabs', max_le_iff, ← min_inv_inv', le_min_iff, inv_inv] at hx

Premises used: le_mabs', max_le_iff, inv_inv, Set.mem_Ici, min_inv_inv', le_min_iff, Set.mem_preimage
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b x : G
hx : x ≤ a ∧ x ≤ b⁻¹ ∨ a⁻¹ ≤ x ∧ b ≤ x
⊢ x ∈ Iic (a, b).1 ∪ Ici (a, b).2

Tactic:
hx.imp And.left And.right

Premises used: Set.union, Set.Mem, setOf, And.right, And.left, Or.imp
-- Module: Mathlib.Order.Filter.AtTopBot.Group
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b x : G
hx : x ≤ a ∧ x ≤ b⁻¹ ∨ a⁻¹ ≤ x ∧ b ≤ x
⊢ x ∈ Iic (a, b).1 ∪ Ici (a, b).2

Tactic:
exact hx.imp And.left And.right

Premises used: And.right, And.left, Or.imp
-- Module: Mathlib.Order.Filter.AtTopBot.Interval
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Tendsto (β := Finset α) (fun (p : α × α) ↦ Icc p.1 p.2) (SProd.sprod (α := Filter α) (β := Filter α) atBot atTop)
    atTop

Tactic:
simpa [tendsto_atTop, ← coe_subset, Set.subset_def, -eventually_and]
    using fun b i _ ↦ (eventually_le_atBot i).prod_mk (eventually_ge_atTop i)

Premises used: Filter.eventually_and, Set.subset_def, Filter.tendsto_atTop, Filter.Eventually.prod_mk, Filter.eventually_ge_atTop, Filter.eventually_le_atBot, Finset.coe_subset
-- Module: Mathlib.Order.Filter.AtTopBot.Interval
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : NoBotOrder α
⊢ Tendsto (β := Finset α) (fun (p : α × α) ↦ Ioc p.1 p.2) (SProd.sprod (α := Filter α) (β := Filter α) atBot atTop)
    atTop

Tactic:
simpa [tendsto_atTop, ← coe_subset, Set.subset_def, -eventually_and]
    using fun b i _ ↦ (eventually_lt_atBot i).prod_mk (eventually_ge_atTop i)

Premises used: Filter.eventually_and, Set.subset_def, Filter.tendsto_atTop, Filter.Eventually.prod_mk, Filter.eventually_lt_atBot, Filter.eventually_ge_atTop, Finset.coe_subset
-- Module: Mathlib.Order.Filter.AtTopBot.Interval
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : NoTopOrder α
⊢ Tendsto (β := Finset α) (fun (p : α × α) ↦ Ico p.1 p.2) (SProd.sprod (α := Filter α) (β := Filter α) atBot atTop)
    atTop

Tactic:
simpa [tendsto_atTop, ← coe_subset, Set.subset_def, -eventually_and]
    using fun b i _ ↦ (eventually_le_atBot i).prod_mk (eventually_gt_atTop i)

Premises used: Filter.eventually_and, Set.subset_def, Filter.tendsto_atTop, Filter.Eventually.prod_mk, Filter.eventually_le_atBot, Filter.eventually_gt_atTop, Finset.coe_subset
-- Module: Mathlib.Order.Filter.AtTopBot.Interval
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : NoBotOrder α
inst_3 : NoTopOrder α
⊢ Tendsto (β := Finset α) (fun (p : α × α) ↦ Ioo p.1 p.2) (SProd.sprod (α := Filter α) (β := Filter α) atBot atTop)
    atTop

Tactic:
simpa [tendsto_atTop, ← coe_subset, Set.subset_def, -eventually_and]
    using fun b i _ ↦ (eventually_lt_atBot i).prod_mk (eventually_gt_atTop i)

Premises used: Filter.eventually_and, Set.subset_def, Filter.tendsto_atTop, Filter.Eventually.prod_mk, Filter.eventually_lt_atBot, Filter.eventually_gt_atTop, Finset.coe_subset
-- Module: Mathlib.Order.Filter.AtTopBot.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : LocallyFiniteOrder α
⊢ Tendsto (β := Finset α) (fun (a : α) ↦ Icc (-a) a) atTop atTop

Tactic:
tendsto_Icc_atBot_prod_atTop.comp (tendsto_neg_atTop_atBot.prodMk tendsto_id)

Premises used: Filter.tendsto_id, Filter.tendsto_neg_atTop_atBot, Finset.Icc, Filter.Tendsto.prodMk, Filter.Tendsto.comp, Finset.tendsto_Icc_atBot_prod_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : LocallyFiniteOrder α
inst_4 : NoBotOrder α
⊢ Tendsto (β := Finset α) (fun (a : α) ↦ Ioc (-a) a) atTop atTop

Tactic:
tendsto_Ioc_atBot_prod_atTop.comp (tendsto_neg_atTop_atBot.prodMk tendsto_id)

Premises used: Filter.tendsto_id, Filter.tendsto_neg_atTop_atBot, Finset.tendsto_Ioc_atBot_prod_atTop, Filter.Tendsto.prodMk, Filter.Tendsto.comp, Finset.Ioc
-- Module: Mathlib.Order.Filter.AtTopBot.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : LocallyFiniteOrder α
inst_4 : NoTopOrder α
⊢ Tendsto (β := Finset α) (fun (a : α) ↦ Ico (-a) a) atTop atTop

Tactic:
tendsto_Ico_atBot_prod_atTop.comp (tendsto_neg_atTop_atBot.prodMk tendsto_id)

Premises used: Filter.tendsto_id, Filter.tendsto_neg_atTop_atBot, Finset.Ico, Finset.tendsto_Ico_atBot_prod_atTop, Filter.Tendsto.prodMk, Filter.Tendsto.comp
-- Module: Mathlib.Order.Filter.AtTopBot.Interval
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : LocallyFiniteOrder α
inst_4 : NoBotOrder α
inst_5 : NoTopOrder α
⊢ Tendsto (β := Finset α) (fun (a : α) ↦ Ioo (-a) a) atTop atTop

Tactic:
tendsto_Ioo_atBot_prod_atTop.comp (tendsto_neg_atTop_atBot.prodMk tendsto_id)

Premises used: Finset.tendsto_Ioo_atBot_prod_atTop, Filter.tendsto_id, Filter.tendsto_neg_atTop_atBot, Filter.Tendsto.prodMk, Filter.Tendsto.comp, Finset.Ioo
-- Module: Mathlib.Order.Filter.AtTopBot.Interval
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : LocallyFiniteOrder R
inst_4 : Archimedean R
⊢ Tendsto.{0, u_1} (β := Finset R) (fun (n : ℕ) ↦ Icc (-(↑n : R)) (↑n : R)) atTop atTop

Tactic:
tendsto_Icc_neg_atTop_atTop.comp tendsto_natCast_atTop_atTop

Premises used: Finset.tendsto_Icc_neg_atTop_atTop, Finset.Icc, tendsto_natCast_atTop_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Order.Filter.AtTopBot.Interval
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : LocallyFiniteOrder R
inst_4 : Archimedean R
inst_5 : Nontrivial R
⊢ Tendsto.{0, u_1} (β := Finset R) (fun (n : ℕ) ↦ Ioc (-(↑n : R)) (↑n : R)) atTop atTop

Tactic:
tendsto_Ioc_neg_atTop_atTop.comp tendsto_natCast_atTop_atTop

Premises used: Finset.tendsto_Ioc_neg_atTop_atTop, tendsto_natCast_atTop_atTop, Filter.Tendsto.comp, Finset.Ioc
-- Module: Mathlib.Order.Filter.AtTopBot.Interval
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : LocallyFiniteOrder R
inst_4 : Archimedean R
inst_5 : Nontrivial R
⊢ Tendsto.{0, u_1} (β := Finset R) (fun (n : ℕ) ↦ Ico (-(↑n : R)) (↑n : R)) atTop atTop

Tactic:
tendsto_Ico_neg_atTop_atTop.comp tendsto_natCast_atTop_atTop

Premises used: Finset.tendsto_Ico_neg_atTop_atTop, Finset.Ico, tendsto_natCast_atTop_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Order.Filter.AtTopBot.Interval
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : LocallyFiniteOrder R
inst_4 : Archimedean R
inst_5 : Nontrivial R
⊢ Tendsto.{0, u_1} (β := Finset R) (fun (n : ℕ) ↦ Ioo (-(↑n : R)) (↑n : R)) atTop atTop

Tactic:
tendsto_Ioo_neg_atTop_atTop.comp tendsto_natCast_atTop_atTop

Premises used: tendsto_natCast_atTop_atTop, Finset.tendsto_Ioo_neg_atTop_atTop, Filter.Tendsto.comp, Finset.Ioo
-- Module: Mathlib.Order.Filter.AtTopBot.Map
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
⊢ Eq.{u_3 + 1} (α := Filter α) (comap.{u_3, u_4} (β := β) (⇑e : (a : α) → β) atTop) atTop

Tactic:
simp [atTop, ← e.surjective.iInf_comp]

Premises used: OrderIso.surjective, Filter.atTop, Function.Surjective.iInf_comp
-- Module: Mathlib.Order.Filter.AtTopBot.Map
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
⊢ Eq.{u_3 + 1} (α := Filter α) (comap.{u_3, u_4} (β := β) (⇑e : (a : α) → β) atBot) atBot

Tactic:
e.dual.comap_atTop

Premises used: OrderIso.comap_atTop, setOf, OrderIso.dual, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Map
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
rw :
  Eq.{u_4 + 1} (α := Filter β)
    (map.{u_3, u_4} (α := α) (⇑e : (a : α) → β) (comap.{u_3, u_4} (β := β) (⇑e : (a : α) → β) atTop)) atTop
rw₁ rw₂ : Eq.{u_4 + 1} (α := Filter β) atTop atTop
⊢ Eq.{u_4 + 1} (α := Filter β) (map.{u_3, u_4} (α := α) (⇑e : (a : α) → β) atTop) atTop

Tactic:
rw [← e.comap_atTop, map_comap_of_surjective e.surjective]

Premises used: OrderIso.comap_atTop, OrderIso.surjective, Filter.map_comap_of_surjective
-- Module: Mathlib.Order.Filter.AtTopBot.Map
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
⊢ Eq.{u_4 + 1} (α := Filter β) (map.{u_3, u_4} (α := α) (⇑e : (a : α) → β) atBot) atBot

Tactic:
e.dual.map_atTop

Premises used: setOf, OrderIso.dual, Filter.atBot, Set.Iic, OrderDual, OrderIso.map_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Map
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
⊢ Tendsto.{u_3, u_4} (α := α) (β := β) (⇑e : (a : α) → β) atTop atTop

Tactic:
e.map_atTop.le

Premises used: Eq.le, Filter.Tendsto, OrderIso.map_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Map
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
⊢ Tendsto.{u_3, u_4} (α := α) (β := β) (⇑e : (a : α) → β) atBot atBot

Tactic:
e.map_atBot.le

Premises used: OrderIso.map_atBot, Eq.le, Filter.Tendsto
-- Module: Mathlib.Order.Filter.AtTopBot.Map
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder α
inst_1 : Preorder β
l : Filter γ
f : γ → α
e : α ≃o β
rw :
  Tendsto.{u_5, u_4} (β := β) (fun (x : γ) ↦ (e : (a : α) → β) (f x)) l atTop ↔
    Tendsto f l (comap.{u_3, u_4} (β := β) (⇑e : (a : α) → β) atTop)
rw₁ :
  Tendsto.{u_5, u_4} (β := β) (fun (x : γ) ↦ (e : (a : α) → β) (f x)) l atTop ↔
    Tendsto.{u_5, u_4} (β := β) ((⇑e : (a : α) → β) ∘ f) l atTop
rw₂ rw₃ :
  Tendsto.{u_5, u_4} (β := β) (fun (x : γ) ↦ (e : (a : α) → β) (f x)) l atTop ↔
    Tendsto.{u_5, u_4} (β := β) (fun (x : γ) ↦ (e : (a : α) → β) (f x)) l atTop
⊢ Tendsto.{u_5, u_4} (β := β) (fun (x : γ) ↦ (e : (a : α) → β) (f x)) l atTop ↔ Tendsto f l atTop

Tactic:
rw [← e.comap_atTop, tendsto_comap_iff, Function.comp_def]

Premises used: OrderIso.comap_atTop, Filter.tendsto_comap_iff, Function.comp_def
-- Module: Mathlib.Order.Filter.AtTopBot.Map
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder α
inst_1 : Preorder β
l : Filter γ
f : γ → α
e : α ≃o β
⊢ Tendsto.{u_5, u_4} (β := β) (fun (x : γ) ↦ (e : (a : α) → β) (f x)) l atBot ↔ Tendsto f l atBot

Tactic:
e.dual.tendsto_atTop_iff

Premises used: OrderIso.tendsto_atTop_iff, setOf, OrderIso.dual, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.ModEq
Goal:
n : ℕ
h : n ≠ 0
d m : ℕ
⊢ ((fun (a : ℕ) ↦ a + d) ∘ fun (x : ℕ) ↦ n • id x) m ≡ d [MOD n]

Tactic:
simp [Nat.modEq_iff_dvd]

Premises used: Nat.modEq_iff_dvd
-- Module: Mathlib.Order.Filter.AtTopBot.ModEq
Goal:
d n : ℕ
h : d < n
⊢ ∃ᶠ (m : ℕ) in atTop, m % n = d

Tactic:
simpa only [Nat.ModEq, mod_eq_of_lt h] using frequently_modEq h.ne_bot d

Premises used: Nat.mod_eq_of_lt, Nat.ModEq, Nat.frequently_modEq, LT.lt.ne_bot
-- Module: Mathlib.Order.Filter.AtTopBot.ModEq
Goal:
⊢ ∃ᶠ (m : ℕ) in atTop, Even m

Tactic:
simpa only [even_iff] using frequently_mod_eq zero_lt_two

Premises used: Nat.frequently_mod_eq, Nat.even_iff, zero_lt_two
-- Module: Mathlib.Order.Filter.AtTopBot.ModEq
Goal:
⊢ ∃ᶠ (m : ℕ) in atTop, Odd m

Tactic:
simpa only [odd_iff] using frequently_mod_eq one_lt_two

Premises used: one_lt_two, Nat.frequently_mod_eq, Nat.odd_iff
-- Module: Mathlib.Order.Filter.AtTopBot.ModEq
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
h : ∀ᶠ (n : ℕ) in atTop, 0 ≤ a ^ n
⊢ 0 ≤ a

Tactic:
let ⟨_n, ho, hn⟩ := (Nat.frequently_odd.and_eventually h).exists
  ho.pow_nonneg_iff.1 hn

Premises used: _private.0.Filter.nonneg_of_eventually_pow_nonneg.match_1, Odd.pow_nonneg_iff, Nat.frequently_odd, LE.le, Filter.Frequently.and_eventually, Filter.Frequently.exists, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : Filter α
f g : α → M
hf : 1 ≤ᶠ[l] f
hg : Tendsto g l atTop
⊢ Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop

Tactic:
tendsto_atTop_mono' l (hf.mono fun _ ↦ le_mul_of_one_le_left') hg

Premises used: le_mul_of_one_le_left', Filter.Eventually.mono, Filter.tendsto_atTop_mono'
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : Filter α
f g : α → M
hf : f ≤ᶠ[l] 1
hg : Tendsto g l atBot
⊢ Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atBot

Tactic:
hg.one_eventuallyLE_mul_atTop (M := Mᵒᵈ) hf

Premises used: setOf, Filter.atBot, Set.Iic, OrderDual, Filter.Tendsto.one_eventuallyLE_mul_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : Filter α
f g : α → M
hf : ∀ (x : α), 1 ≤ f x
hg : Tendsto g l atTop
⊢ Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop

Tactic:
hg.one_eventuallyLE_mul_atTop (.of_forall hf)

Premises used: Filter.Eventually.of_forall, Filter.Tendsto.one_eventuallyLE_mul_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : Filter α
f g : α → M
hf : ∀ (x : α), f x ≤ 1
hg : Tendsto g l atBot
⊢ Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atBot

Tactic:
hg.eventuallyLE_one_mul_atBot (.of_forall hf)

Premises used: Filter.Eventually.of_forall, Filter.Tendsto.eventuallyLE_one_mul_atBot
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : Filter α
f g : α → M
hf : Tendsto f l atTop
hg : 1 ≤ᶠ[l] g
⊢ Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop

Tactic:
tendsto_atTop_mono' l (hg.mono fun _ => le_mul_of_one_le_right') hf

Premises used: Filter.Eventually.mono, Filter.tendsto_atTop_mono', le_mul_of_one_le_right'
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : Filter α
f g : α → M
hf : Tendsto f l atBot
hg : g ≤ᶠ[l] 1
⊢ Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atBot

Tactic:
hf.atTop_mul_one_eventuallyLE (M := Mᵒᵈ) hg

Premises used: setOf, Filter.Tendsto.atTop_mul_one_eventuallyLE, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : Filter α
f g : α → M
hf : Tendsto f l atTop
hg : ∀ (x : α), 1 ≤ g x
⊢ Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop

Tactic:
hf.atTop_mul_one_eventuallyLE <| .of_forall hg

Premises used: Filter.Eventually.of_forall, Filter.Tendsto.atTop_mul_one_eventuallyLE
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : Filter α
f g : α → M
hf : Tendsto f l atBot
hg : ∀ (x : α), g x ≤ 1
⊢ Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atBot

Tactic:
hf.atBot_mul_eventuallyLE_one (.of_forall hg)

Premises used: Filter.Eventually.of_forall, Filter.Tendsto.atBot_mul_eventuallyLE_one
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : Filter α
f g : α → M
hf : Tendsto f l atTop
hg : Tendsto g l atTop
⊢ Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop

Tactic:
hf.atTop_mul_one_eventuallyLE <| hg.eventually_ge_atTop 1

Premises used: Filter.Tendsto.atTop_mul_one_eventuallyLE, OfNat.ofNat, Filter.Tendsto.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : Filter α
f g : α → M
hf : Tendsto f l atBot
hg : Tendsto g l atBot
⊢ Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atBot

Tactic:
hf.atTop_mul_atTop (M := Mᵒᵈ) hg

Premises used: setOf, Filter.atBot, Set.Iic, Filter.Tendsto.atTop_mul_atTop, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : Filter α
f : α → M
hf : Tendsto f l atTop
n : ℕ
hn : 0 < n
⊢ Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x ^ n) l atTop

Tactic:
tendsto_atTop_mono' _ ((hf.eventually_ge_atTop 1).mono fun x hx ↦ ?_) hf

Premises used: Filter.Eventually.mono, Filter.tendsto_atTop_mono', OfNat.ofNat, Filter.Tendsto.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : Filter α
f : α → M
hf : Tendsto f l atTop
n : ℕ
hn : 0 < n
refine : ∀ (x : α) (hx : 1 ≤ f x), f x ≤ (fun (x : α) ↦ f x ^ n) x
⊢ Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x ^ n) l atTop

Tactic:
refine tendsto_atTop_mono' _ ((hf.eventually_ge_atTop 1).mono fun x hx ↦ ?_) hf

Premises used: Filter.Eventually.mono, Filter.tendsto_atTop_mono', OfNat.ofNat, Filter.Tendsto.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : Filter α
f : α → M
hf : Tendsto f l atTop
n : ℕ
hn : 0 < n
x : α
hx : 1 ≤ f x
⊢ f x ≤ (fun (x : α) ↦ f x ^ n) x

Tactic:
simpa only [pow_one] using pow_le_pow_right' hx hn

Premises used: pow_one, pow_le_pow_right'
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedMonoid M
l : Filter α
f : α → M
hf : Tendsto f l atBot
n : ℕ
hn : 0 < n
⊢ Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x ^ n) l atBot

Tactic:
Tendsto.atTop_pow (M := Mᵒᵈ) hf hn

Premises used: setOf, Filter.Tendsto.atTop_pow, Filter.atBot, Set.Iic, OrderDual