awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f : α → M
C : M
hf : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ C * f x) l atTop
⊢ Tendsto f l atTop

Tactic:
tendsto_atTop.2 fun b ↦ (tendsto_atTop.1 hf (C * b)).mono fun _ ↦ le_of_mul_le_mul_left'

Premises used: Iff.mpr, HMul.hMul, Filter.tendsto_atTop, Filter.Eventually.mono, Iff.mp, le_of_mul_le_mul_left'
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f : α → M
C : M
hf : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ C * f x) l atBot
⊢ Tendsto f l atBot

Tactic:
hf.atTop_of_const_mul (M := Mᵒᵈ)

Premises used: Filter.Tendsto.atTop_of_const_mul, setOf, 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 : IsOrderedCancelMonoid M
l : Filter α
f : α → M
C : M
hf : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * C) l atTop
⊢ Tendsto f l atTop

Tactic:
tendsto_atTop.2 fun b => (tendsto_atTop.1 hf (b * C)).mono fun _ => le_of_mul_le_mul_right'

Premises used: Iff.mpr, HMul.hMul, Filter.tendsto_atTop, le_of_mul_le_mul_right', Filter.Eventually.mono, Iff.mp
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f : α → M
C : M
hf : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * C) l atBot
⊢ Tendsto f l atBot

Tactic:
hf.atTop_of_mul_const (M := Mᵒᵈ)

Premises used: setOf, Filter.Tendsto.atTop_of_mul_const, 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 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hf : IsBoundedUnder (fun (x1 x2 : M) ↦ x1 ≤ x2) l f
hfg : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
obtain : ∀ (C : M) (hC : ∀ᶠ (x : M) in map f l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C), Tendsto g l atTop
⊢ Tendsto g l atTop

Tactic:
obtain ⟨C, hC⟩ := hf
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hfg : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map f l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C
⊢ Tendsto g l atTop

Tactic:
.atTop_of_const_mul C <| tendsto_atTop_mono' l ?_ hfg

Premises used: Filter.Tendsto.atTop_of_const_mul, 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 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hfg : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map f l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C
refine : EventuallyLE.{u_1, u_2} (β := M) l (fun (x : α) ↦ f x * g x) fun (x : α) ↦ C * g x
⊢ Tendsto g l atTop

Tactic:
refine .atTop_of_const_mul C <| tendsto_atTop_mono' l ?_ hfg

Premises used: 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 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hfg : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map f l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C
x : α
h : (fun (x1 x2 : M) ↦ x1 ≤ x2) (f x) C
dsimp : f x * g x ≤ C * g x
⊢ LE.le.{u_2} (α := M) ((fun (x : α) ↦ f x * g x) x) ((fun (x : α) ↦ C * g x) x)

Tactic:
dsimp
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hfg : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map f l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C
x : α
h : (fun (x1 x2 : M) ↦ x1 ≤ x2) (f x) C
⊢ f x * g x ≤ C * g x

Tactic:
gcongr
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hfg : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map f l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C
⊢ EventuallyLE.{u_1, u_2} (β := M) l (fun (x : α) ↦ f x * g x) fun (x : α) ↦ C * g x

Tactic:
exact (eventually_map.mp hC).mono fun _ _ ↦ by dsimp; gcongr

Premises used: Filter.eventually_map, Filter.Eventually.mono, Iff.mp
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hf : IsBoundedUnder (fun (x1 x2 : M) ↦ x1 ≥ x2) l f
h : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atBot
⊢ Tendsto g l atBot

Tactic:
h.atTop_of_isBoundedUnder_le_mul (M := Mᵒᵈ) hf

Premises used: setOf, Filter.atBot, Filter.Tendsto.atTop_of_isBoundedUnder_le_mul, 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 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hf : ∃ (C : M), ∀ (x : α), f x ≤ C
hfg : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
⊢ Tendsto g l atTop

Tactic:
hfg.atTop_of_isBoundedUnder_le_mul <| hf.imp fun _C hC ↦ eventually_map.mpr <| .of_forall hC

Premises used: Iff.mpr, Filter.Eventually.of_forall, Exists.imp, Filter.eventually_map, Filter.Tendsto.atTop_of_isBoundedUnder_le_mul
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hf : ∃ (C : M), ∀ (x : α), C ≤ f x
hfg : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atBot
⊢ Tendsto g l atBot

Tactic:
Tendsto.atTop_of_le_const_mul (M := Mᵒᵈ) hf hfg

Premises used: setOf, Filter.atBot, Filter.Tendsto.atTop_of_le_const_mul, 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 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hg : IsBoundedUnder (fun (x1 x2 : M) ↦ x1 ≤ x2) l g
h : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
obtain : ∀ (C : M) (hC : ∀ᶠ (x : M) in map g l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C), Tendsto f l atTop
⊢ Tendsto f l atTop

Tactic:
obtain ⟨C, hC⟩ := hg
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
h : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map g l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C
⊢ Tendsto f l atTop

Tactic:
.atTop_of_mul_const C <| tendsto_atTop_mono' l ?_ h

Premises used: Filter.Tendsto.atTop_of_mul_const, 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 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
h : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map g l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C
refine : EventuallyLE.{u_1, u_2} (β := M) l (fun (x : α) ↦ f x * g x) fun (x : α) ↦ f x * C
⊢ Tendsto f l atTop

Tactic:
refine .atTop_of_mul_const C <| tendsto_atTop_mono' l ?_ h

Premises used: 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 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
h : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map g l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C
x : α
h_1 : (fun (x1 x2 : M) ↦ x1 ≤ x2) (g x) C
dsimp : f x * g x ≤ f x * C
⊢ LE.le.{u_2} (α := M) ((fun (x : α) ↦ f x * g x) x) ((fun (x : α) ↦ f x * C) x)

Tactic:
dsimp
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
h : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map g l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C
x : α
h_1 : (fun (x1 x2 : M) ↦ x1 ≤ x2) (g x) C
⊢ f x * g x ≤ f x * C

Tactic:
gcongr
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
h : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map g l, (fun (x1 x2 : M) ↦ x1 ≤ x2) x C
⊢ EventuallyLE.{u_1, u_2} (β := M) l (fun (x : α) ↦ f x * g x) fun (x : α) ↦ f x * C

Tactic:
exact (eventually_map.mp hC).mono fun _ _ ↦ by dsimp; gcongr

Premises used: Filter.eventually_map, Filter.Eventually.mono, Iff.mp
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hg : IsBoundedUnder (fun (x1 x2 : M) ↦ x1 ≥ x2) l g
h : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atBot
⊢ Tendsto f l atBot

Tactic:
h.atTop_of_mul_isBoundedUnder_le (M := Mᵒᵈ) hg

Premises used: Filter.Tendsto.atTop_of_mul_isBoundedUnder_le, setOf, 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 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hg : ∃ (C : M), ∀ (x : α), g x ≤ C
hfg : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atTop
⊢ Tendsto f l atTop

Tactic:
hfg.atTop_of_mul_isBoundedUnder_le <| hg.imp fun _C hC ↦ eventually_map.mpr <| .of_forall hC

Premises used: Iff.mpr, Filter.Tendsto.atTop_of_mul_isBoundedUnder_le, Filter.Eventually.of_forall, Exists.imp, Filter.eventually_map
-- Module: Mathlib.Order.Filter.AtTopBot.Monoid
Goal:
α : Type u_1
M : Type u_2
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hg : ∃ (C : M), ∀ (x : α), C ≤ g x
hfg : Tendsto.{u_1, u_2} (β := M) (fun (x : α) ↦ f x * g x) l atBot
⊢ Tendsto f l atBot

Tactic:
Tendsto.atTop_of_mul_le_const (M := Mᵒᵈ) hg hfg

Premises used: setOf, Filter.Tendsto.atTop_of_mul_le_const, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
inl : IsEmpty α → SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop
inr : Nonempty α → SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop
⊢ SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
h : IsEmpty α
⊢ SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop

Tactic:
subsingleton
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
h : Nonempty α
inr : IsEmpty β → SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop
inr₁ : Nonempty β → SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop
⊢ SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop

Tactic:
cases isEmpty_or_nonempty β

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
h : Nonempty α
h_1 : IsEmpty β
⊢ SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop

Tactic:
subsingleton
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
h : Nonempty α
h_1 : Nonempty β
⊢ SProd.sprod (α := Filter α) (β := Filter β) atTop atTop = atTop

Tactic:
simpa [atTop, prod_iInf_left, prod_iInf_right, iInf_prod] using iInf_comm

Premises used: Filter.prod_iInf_left, Filter.prod_iInf_right, Filter.atTop, iInf_comm, iInf_prod
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
ι : Type u_1
ι' : Type u_2
hf : Monotone (β := Finset (ι × ι')) fun (p : Prod.{u_1, u_2} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
h : ∀ (b : Finset (ι × ι')), ∃ (a : Prod.{u_1, u_2} (Finset ι) (Finset ι')), b ≤ a.1 ×ˢ a.2
⊢ Tendsto (β := Finset (ι × ι')) (fun (p : Prod.{u_1, u_2} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2) atTop atTop

Tactic:
apply Monotone.tendsto_atTop_atTop

Premises used: Monotone.tendsto_atTop_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
ι : Type u_1
ι' : Type u_2
p q : Prod.{u_1, u_2} (Finset ι) (Finset ι')
hpq : p ≤ q
⊢ LE.le (α := Finset (ι × ι')) ((fun (p : Prod.{u_1, u_2} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2) p)
    ((fun (p : Prod.{u_1, u_2} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2) q)

Tactic:
simpa using Finset.product_subset_product hpq.1 hpq.2

Premises used: Finset.product_subset_product, And.right, And.left
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
ι : Type u_1
ι' : Type u_2
b : Finset (ι × ι')
h : b ≤ (Finset.image Prod.fst b, Finset.image Prod.snd b).1 ×ˢ (Finset.image Prod.fst b, Finset.image Prod.snd b).2
⊢ ∃ (a : Prod.{u_1, u_2} (Finset ι) (Finset ι')), b ≤ a.1 ×ˢ a.2

Tactic:
use (Finset.image Prod.fst b, Finset.image Prod.snd b)

Premises used: Prod.mk, Prod.fst, Prod.snd, Finset.image
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
ι : Type u_1
ι' : Type u_2
b : Finset (ι × ι')
⊢ b ≤ (Finset.image Prod.fst b, Finset.image Prod.snd b).1 ×ˢ (Finset.image Prod.fst b, Finset.image Prod.snd b).2

Tactic:
Finset.subset_product

Premises used: Multiset.toFinset, Set.Mem, setOf, Finset.subset_product, Finset.image
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
ι : Type u_1
ι' : Type u_2
b : Finset (ι × ι')
⊢ b ≤ (Finset.image Prod.fst b, Finset.image Prod.snd b).1 ×ˢ (Finset.image Prod.fst b, Finset.image Prod.snd b).2

Tactic:
exact Finset.subset_product

Premises used: Finset.subset_product
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
ι : Type u_1
ι' : Type u_2
hf : Monotone (β := Finset (ι × ι')) fun (p : Prod.{u_1, u_2} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
h h₁ : ∀ (b : Finset (ι × ι')), ∃ (a : Prod.{u_1, u_2} (Finset ι) (Finset ι')), b ≤ a.1 ×ˢ a.2
⊢ Tendsto (β := Finset (ι × ι')) (fun (p : Prod.{u_1, u_2} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2) atTop atTop

Tactic:
classical
  apply Monotone.tendsto_atTop_atTop
  · intro p q hpq
    simpa using Finset.product_subset_product hpq.1 hpq.2
  · intro b
    use (Finset.image Prod.fst b, Finset.image Prod.snd b)
    exact Finset.subset_product

Premises used: Finset.subset_product, Monotone.tendsto_atTop_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
⊢ SProd.sprod (α := Filter α) (β := Filter β) atBot atBot = atBot

Tactic:
@prod_atTop_atTop_eq αᵒᵈ βᵒᵈ _ _

Premises used: Set.Mem, setOf, Filter.atBot, Filter.prod_atTop_atTop_eq, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α₁ : Type u_6
α₂ : Type u_7
β₁ : Type u_8
β₂ : Type u_9
inst : Preorder β₁
inst_1 : Preorder β₂
u₁ : β₁ → α₁
u₂ : β₂ → α₂
rw :
  map (fun (p : β₁ × β₂) ↦ (u₁ p.1, u₂ p.2)) (SProd.sprod (α := Filter β₁) (β := Filter β₂) atTop atTop) =
    map (Prod.map u₁ u₂) atTop
rw₁ : map (fun (p : β₁ × β₂) ↦ (u₁ p.1, u₂ p.2)) atTop = map (Prod.map u₁ u₂) atTop
rw₂ rw₃ :
  Eq (α := Filter (α₁ × α₂)) (map (fun (p : β₁ × β₂) ↦ (u₁ p.1, u₂ p.2)) atTop)
    (map (fun (p : β₁ × β₂) ↦ (u₁ p.1, u₂ p.2)) atTop)
⊢ map u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop

Tactic:
rw [prod_map_map_eq, prod_atTop_atTop_eq, Prod.map_def]

Premises used: Filter.prod_atTop_atTop_eq, Filter.prod_map_map_eq, Prod.map_def
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α₁ : Type u_6
α₂ : Type u_7
β₁ : Type u_8
β₂ : Type u_9
inst : Preorder β₁
inst_1 : Preorder β₂
u₁ : β₁ → α₁
u₂ : β₂ → α₂
⊢ map u₁ atBot ×ˢ map u₂ atBot = map (Prod.map u₁ u₂) atBot

Tactic:
@prod_map_atTop_eq _ _ β₁ᵒᵈ β₂ᵒᵈ _ _ _ _

Premises used: Set.Mem, setOf, Filter.prod_map_atTop_eq, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
inst : Preorder α
rw : Tendsto (fun (a : α) ↦ (a, a)) atBot (SProd.sprod (α := Filter α) (β := Filter α) atBot atBot)
⊢ Tendsto (β := α × α) (fun (a : α) ↦ (a, a)) atBot atBot

Tactic:
rw [← prod_atBot_atBot_eq]

Premises used: Filter.prod_atBot_atBot_eq
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
inst : Preorder α
⊢ Tendsto (fun (a : α) ↦ (a, a)) atBot (SProd.sprod (α := Filter α) (β := Filter α) atBot atBot)

Tactic:
tendsto_id.prodMk tendsto_id

Premises used: Filter.tendsto_id, Filter.Tendsto.prodMk
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
inst : Preorder α
⊢ Tendsto (fun (a : α) ↦ (a, a)) atBot (SProd.sprod (α := Filter α) (β := Filter α) atBot atBot)

Tactic:
exact tendsto_id.prodMk tendsto_id

Premises used: Filter.tendsto_id, Filter.Tendsto.prodMk
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
inst : Preorder α
rw : Tendsto (fun (a : α) ↦ (a, a)) atTop (SProd.sprod (α := Filter α) (β := Filter α) atTop atTop)
⊢ Tendsto (β := α × α) (fun (a : α) ↦ (a, a)) atTop atTop

Tactic:
rw [← prod_atTop_atTop_eq]

Premises used: Filter.prod_atTop_atTop_eq
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
inst : Preorder α
⊢ Tendsto (fun (a : α) ↦ (a, a)) atTop (SProd.sprod (α := Filter α) (β := Filter α) atTop atTop)

Tactic:
tendsto_id.prodMk tendsto_id

Premises used: Filter.tendsto_id, Filter.Tendsto.prodMk
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
inst : Preorder α
⊢ Tendsto (fun (a : α) ↦ (a, a)) atTop (SProd.sprod (α := Filter α) (β := Filter α) atTop atTop)

Tactic:
exact tendsto_id.prodMk tendsto_id

Premises used: Filter.tendsto_id, Filter.Tendsto.prodMk
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
rw : Tendsto (Prod.map f g) (F ×ˢ G) (SProd.sprod (α := Filter γ) (β := Filter γ) atBot atBot)
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atBot

Tactic:
rw [← prod_atBot_atBot_eq]

Premises used: Filter.prod_atBot_atBot_eq
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (SProd.sprod (α := Filter γ) (β := Filter γ) atBot atBot)

Tactic:
hf.prodMap hg

Premises used: Filter.Tendsto.prodMap
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atBot
hg : Tendsto g G atBot
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (SProd.sprod (α := Filter γ) (β := Filter γ) atBot atBot)

Tactic:
exact hf.prodMap hg

Premises used: Filter.Tendsto.prodMap
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
rw : Tendsto (Prod.map f g) (F ×ˢ G) (SProd.sprod (α := Filter γ) (β := Filter γ) atTop atTop)
⊢ Tendsto (Prod.map f g) (F ×ˢ G) atTop

Tactic:
rw [← prod_atTop_atTop_eq]

Premises used: Filter.prod_atTop_atTop_eq
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (SProd.sprod (α := Filter γ) (β := Filter γ) atTop atTop)

Tactic:
hf.prodMap hg

Premises used: Filter.Tendsto.prodMap
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder γ
F : Filter α
G : Filter β
f : α → γ
g : β → γ
hf : Tendsto f F atTop
hg : Tendsto g G atTop
⊢ Tendsto (Prod.map f g) (F ×ˢ G) (SProd.sprod (α := Filter γ) (β := Filter γ) atTop atTop)

Tactic:
exact hf.prodMap hg

Premises used: Filter.Tendsto.prodMap
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
γ : Type u_5
inst : Preorder α
inst_1 : Preorder γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
rw : Tendsto (Prod.map f g) (SProd.sprod (α := Filter α) (β := Filter α) atBot atBot) atBot
⊢ Tendsto (Prod.map f g) atBot atBot

Tactic:
rw [← prod_atBot_atBot_eq]

Premises used: Filter.prod_atBot_atBot_eq
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
γ : Type u_5
inst : Preorder α
inst_1 : Preorder γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) (SProd.sprod (α := Filter α) (β := Filter α) atBot atBot) atBot

Tactic:
hf.prod_map_prod_atBot hg

Premises used: Filter.Tendsto.prod_map_prod_atBot
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
γ : Type u_5
inst : Preorder α
inst_1 : Preorder γ
f g : α → γ
hf : Tendsto f atBot atBot
hg : Tendsto g atBot atBot
⊢ Tendsto (Prod.map f g) (SProd.sprod (α := Filter α) (β := Filter α) atBot atBot) atBot

Tactic:
exact hf.prod_map_prod_atBot hg

Premises used: Filter.Tendsto.prod_map_prod_atBot
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
γ : Type u_5
inst : Preorder α
inst_1 : Preorder γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
rw : Tendsto (Prod.map f g) (SProd.sprod (α := Filter α) (β := Filter α) atTop atTop) atTop
⊢ Tendsto (Prod.map f g) atTop atTop

Tactic:
rw [← prod_atTop_atTop_eq]

Premises used: Filter.prod_atTop_atTop_eq
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
γ : Type u_5
inst : Preorder α
inst_1 : Preorder γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) (SProd.sprod (α := Filter α) (β := Filter α) atTop atTop) atTop

Tactic:
hf.prod_map_prod_atTop hg

Premises used: Filter.Tendsto.prod_map_prod_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
γ : Type u_5
inst : Preorder α
inst_1 : Preorder γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) (SProd.sprod (α := Filter α) (β := Filter α) atTop atTop) atTop

Tactic:
exact hf.prod_map_prod_atTop hg

Premises used: Filter.Tendsto.prod_map_prod_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsCodirectedOrder α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ (a : α), ∀ (k l : α), k ≤ a → l ≤ a → p (k, l)

Tactic:
simp [← prod_atBot_atBot_eq, (@atBot_basis α _ _).prod_self.eventually_iff]

Premises used: Filter.HasBasis.prod_self, Filter.atBot_basis, Filter.HasBasis.eventually_iff, Filter.prod_atBot_atBot_eq
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsDirectedOrder α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atTop, p x) ↔ ∃ (a : α), ∀ (k l : α), a ≤ k → a ≤ l → p (k, l)

Tactic:
eventually_atBot_prod_self (α := αᵒᵈ)

Premises used: Set.Ici, setOf, Filter.atTop, OrderDual, Filter.eventually_atBot_prod_self
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsCodirectedOrder α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ (a : α), ∀ k ≤ a, ∀ l ≤ a, p (k, l)

Tactic:
simp only [eventually_atBot_prod_self, forall_cond_comm]

Premises used: forall_cond_comm, Filter.eventually_atBot_prod_self
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsDirectedOrder α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atTop, p x) ↔ ∃ (a : α), ∀ k ≥ a, ∀ l ≥ a, p (k, l)

Tactic:
simp only [eventually_atTop_prod_self, forall_cond_comm]

Premises used: forall_cond_comm, Filter.eventually_atTop_prod_self
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop, p x
⊢ ∀ᶠ (x : α × β) in SProd.sprod (α := Filter α) (β := Filter β) atTop atTop, p x

Tactic:
rw [← prod_atTop_atTop_eq] at hp

Premises used: Filter.prod_atTop_atTop_eq