awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : (a b : α) → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
this : IsDirectedOrder.{u_3} (↑s : Type u_3)
c : α
hc : c ≥ a
⊢ ∃ (x : { x : α // x ∈ s }), (↑x : α) = c ∧ ∀ (a : { x : α // x ∈ s }), (↑a : α) ≤ c ↔ a ≤ x

Tactic:
⟨⟨c, h hc⟩, rfl, fun _ ↦ .rfl⟩

Premises used: Iff.rfl, Subtype.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : (a b : α) → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
this : IsDirectedOrder.{u_3} (↑s : Type u_3)
c : α
hc : c ≥ a
⊢ ∃ (x : { x : α // x ∈ s }), (↑x : α) = c ∧ ∀ (a : { x : α // x ∈ s }), (↑a : α) ≤ c ↔ a ≤ x

Tactic:
exact ⟨⟨c, h hc⟩, rfl, fun _ ↦ .rfl⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
⊢ Eq (α := Filter ℤ) (map Nat.cast atTop) atTop

Tactic:
map_atTop_eq_of_gc_preorder (fun _ _ ↦ Int.ofNat_le.2) 0 fun n hn ↦ ?_

Premises used: Iff.mpr, Filter.map_atTop_eq_of_gc_preorder, Int.ofNat_le, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
refine : ∀ (n : ℤ) (hn : n ≥ 0), ∃ (x : ℕ), (↑x : ℤ) = n ∧ ∀ (a : ℕ), (↑a : ℤ) ≤ n ↔ a ≤ x
⊢ Eq (α := Filter ℤ) (map Nat.cast atTop) atTop

Tactic:
refine map_atTop_eq_of_gc_preorder (fun _ _ ↦ Int.ofNat_le.2) 0 fun n hn ↦ ?_

Premises used: Iff.mpr, Filter.map_atTop_eq_of_gc_preorder, Int.ofNat_le, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
n : ℤ
hn : n ≥ 0
⊢ 0 ≤ n

Tactic:
hn
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
n : ℤ
hn : n ≥ 0
lift : ∀ (n : ℕ), ∃ (x : ℕ), Eq (α := ℤ) (↑x : ℤ) (↑n : ℤ) ∧ ∀ (a : ℕ), LE.le (α := ℤ) (↑a : ℤ) (↑n : ℤ) ↔ a ≤ x
⊢ ∃ (x : ℕ), (↑x : ℤ) = n ∧ ∀ (a : ℕ), (↑a : ℤ) ≤ n ↔ a ≤ x

Tactic:
lift n to ℕ using hn
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
n : ℕ
⊢ ∃ (x : ℕ), Eq (α := ℤ) (↑x : ℤ) (↑n : ℤ) ∧ ∀ (a : ℕ), LE.le (α := ℤ) (↑a : ℤ) (↑n : ℤ) ↔ a ≤ x

Tactic:
⟨n, rfl, fun _ ↦ Int.ofNat_le⟩

Premises used: And.intro, Exists.intro, Int.ofNat_le, rfl
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
n : ℕ
⊢ ∃ (x : ℕ), Eq (α := ℤ) (↑x : ℤ) (↑n : ℤ) ∧ ∀ (a : ℕ), LE.le (α := ℤ) (↑a : ℤ) (↑n : ℤ) ↔ a ≤ x

Tactic:
exact ⟨n, rfl, fun _ ↦ Int.ofNat_le⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
⊢ Eq.{u_3 + 1} (α := Filter α) (map (α := { x : α // x ∈ Ici a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop)
    atTop

Tactic:
map_val_atTop_of_Ici_subset Subset.rfl

Premises used: Filter.map_val_atTop_of_Ici_subset, Set.Subset.rfl
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
⊢ Eq.{u_3 + 1} (α := Filter α) (map (α := { x : α // x ∈ Ioi a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop)
    atTop

Tactic:
let ⟨_b, hb⟩ := exists_gt a
  map_val_atTop_of_Ici_subset <| Ici_subset_Ioi.2 hb

Premises used: Iff.mpr, Filter.map, _private.0.Filter.map_val_Ioi_atTop.match_1, NoMaxOrder.exists_gt, Filter.map_val_atTop_of_Ici_subset, Filter.atTop, Subtype.val, Eq, Set.Ici_subset_Ioi
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
inl :
  ∀ (h : IsEmpty.{u_3 + 1} (↑(Ioi a) : Type u_3)),
    Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop)
inr :
  ∀ (b : α) (hb : b ∈ Ioi a),
    Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop)
⊢ Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop)

Tactic:
rcases isEmpty_or_nonempty (Ioi a) with h | ⟨⟨b, hb⟩⟩

Premises used: Set.Ioi, Set.Elem, isEmpty_or_nonempty
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
h : IsEmpty.{u_3 + 1} (↑(Ioi a) : Type u_3)
⊢ Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop)

Tactic:
subsingleton
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a b : α
hb : b ∈ Ioi a
inr :
  Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop
    (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a))
      (map (α := { x : α // x ∈ Ioi a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop))
inr₁ inr₂ : Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop atTop
⊢ Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ioi a }) atTop (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop)

Tactic:
rw [← map_val_atTop_of_Ici_subset (Ici_subset_Ioi.2 hb), comap_map Subtype.coe_injective]

Premises used: Iff.mpr, Filter.comap_map, Filter.map_val_atTop_of_Ici_subset, Subtype.coe_injective, Set.Ici_subset_Ioi
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
rw :
  Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ici a }) atTop
    (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a))
      (map (α := { x : α // x ∈ Ici a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop))
rw₁ rw₂ : Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ici a }) atTop atTop
⊢ Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Ici a }) atTop (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop)

Tactic:
rw [← map_val_Ici_atTop a, comap_map Subtype.coe_injective]

Premises used: Filter.comap_map, Filter.map_val_Ici_atTop, Subtype.coe_injective
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsCodirectedOrder α
inst_2 : NoMinOrder α
a : α
⊢ Eq.{u_3 + 1} (α := Filter α) (map (α := { x : α // x ∈ Iio a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Iio a)) atBot)
    atBot

Tactic:
map_val_Ioi_atTop (OrderDual.toDual a)

Premises used: OrderDual.toDual, Set.Mem, setOf, Filter.map_val_Ioi_atTop, Filter.atBot, Set.Iic, OrderDual, Set.Iio, DFunLike.coe
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsCodirectedOrder α
a : α
⊢ Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Iio a }) atBot (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Iio a)) atBot)

Tactic:
atTop_Ioi_eq (OrderDual.toDual a)

Premises used: OrderDual.toDual, Set.Mem, setOf, Filter.atTop_Ioi_eq, Filter.atBot, Set.Iic, OrderDual, Set.Iio, DFunLike.coe
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsCodirectedOrder α
a : α
⊢ Eq.{u_3 + 1} (α := Filter α) (map (α := { x : α // x ∈ Iic a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) atBot)
    atBot

Tactic:
map_val_Ici_atTop (OrderDual.toDual a)

Premises used: OrderDual.toDual, Set.Mem, setOf, Filter.map_val_Ici_atTop, Filter.atBot, Set.Iic, OrderDual, DFunLike.coe
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
inst : Preorder α
inst_1 : IsCodirectedOrder α
a : α
⊢ Eq.{u_3 + 1} (α := Filter { x : α // x ∈ Iic a }) atBot (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) atBot)

Tactic:
atTop_Ici_eq (OrderDual.toDual a)

Premises used: OrderDual.toDual, Filter.atTop_Ici_eq, Set.Mem, setOf, Filter.atBot, Set.Iic, OrderDual, DFunLike.coe
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
f : β → (↑(Ioi a) : Type u_3)
l : Filter β
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop) ↔
    Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
rw₁ :
  Tendsto (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a) ∘ f) l atTop ↔
    Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
rw₂ rw₃ :
  Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop ↔
    Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
⊢ Tendsto f l atTop ↔ Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop

Tactic:
rw [atTop_Ioi_eq, tendsto_comap_iff, Function.comp_def]

Premises used: Filter.atTop_Ioi_eq, Filter.tendsto_comap_iff, Function.comp_def
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsCodirectedOrder α
a : α
f : β → (↑(Iio a) : Type u_3)
l : Filter β
⊢ Tendsto f l atBot ↔ Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atBot

Tactic:
tendsto_Ioi_atTop (α := αᵒᵈ)

Premises used: setOf, Filter.tendsto_Ioi_atTop, Filter.atBot, Set.Iic, OrderDual, Set.Iio
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
f : β → (↑(Ici a) : Type u_3)
l : Filter β
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop) ↔
    Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
rw₁ :
  Tendsto (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a) ∘ f) l atTop ↔
    Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
rw₂ rw₃ :
  Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop ↔
    Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop
⊢ Tendsto f l atTop ↔ Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atTop

Tactic:
rw [atTop_Ici_eq, tendsto_comap_iff, Function.comp_def]

Premises used: Filter.atTop_Ici_eq, Filter.tendsto_comap_iff, Function.comp_def
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsCodirectedOrder α
a : α
f : β → (↑(Iic a) : Type u_3)
l : Filter β
⊢ Tendsto f l atBot ↔ Tendsto.{u_4, u_3} (β := α) (fun (x : β) ↦ (↑(f x) : α)) l atBot

Tactic:
tendsto_Ici_atTop (α := αᵒᵈ)

Premises used: setOf, Filter.atBot, Set.Iic, OrderDual, Filter.tendsto_Ici_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : NoMaxOrder α
a : α
f : α → β
l : Filter β
rw :
  Tendsto (fun (x : (↑(Ioi a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
    Tendsto f (map (α := { x : α // x ∈ Ioi a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop) l
rw₁ :
  Tendsto (fun (x : (↑(Ioi a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
    Tendsto (α := { x : α // x ∈ Ioi a }) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Ioi a)) atTop l
rw₂ rw₃ :
  Tendsto (fun (x : (↑(Ioi a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
    Tendsto (fun (x : { x : α // x ∈ Ioi a }) ↦ f (↑x : α)) atTop l
⊢ Tendsto (fun (x : (↑(Ioi a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔ Tendsto f atTop l

Tactic:
rw [← map_val_Ioi_atTop a, tendsto_map'_iff, Function.comp_def]

Premises used: Filter.tendsto_map'_iff, Function.comp_def, Filter.map_val_Ioi_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
f : α → β
l : Filter β
rw :
  Tendsto (fun (x : (↑(Ici a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
    Tendsto f (map (α := { x : α // x ∈ Ici a }) (Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop) l
rw₁ :
  Tendsto (fun (x : (↑(Ici a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
    Tendsto (α := { x : α // x ∈ Ici a }) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Ici a)) atTop l
rw₂ rw₃ :
  Tendsto (fun (x : (↑(Ici a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔
    Tendsto (fun (x : { x : α // x ∈ Ici a }) ↦ f (↑x : α)) atTop l
⊢ Tendsto (fun (x : (↑(Ici a) : Type u_3)) ↦ f (↑x : α)) atTop l ↔ Tendsto f atTop l

Tactic:
rw [← map_val_Ici_atTop a, tendsto_map'_iff, Function.comp_def]

Premises used: Filter.tendsto_map'_iff, Filter.map_val_Ici_atTop, Function.comp_def
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsCodirectedOrder α
inst_2 : NoMinOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun (x : (↑(Iio a) : Type u_3)) ↦ f (↑x : α)) atBot l ↔ Tendsto f atBot l

Tactic:
tendsto_comp_val_Ioi_atTop (α := αᵒᵈ)

Premises used: setOf, Filter.atBot, Set.Iic, OrderDual, Filter.tendsto_comp_val_Ioi_atTop, Set.Iio
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : IsCodirectedOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun (x : (↑(Iic a) : Type u_3)) ↦ f (↑x : α)) atBot l ↔ Tendsto f atBot l

Tactic:
tendsto_comp_val_Ici_atTop (α := αᵒᵈ)

Premises used: setOf, Filter.tendsto_comp_val_Ici_atTop, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
k a : ℕ
h : a ≥ k
rw rw₁ : a ≤ a
⊢ a ≤ (fun (x : ℕ) ↦ x - k) a + k

Tactic:
rw [Nat.sub_add_cancel h]

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
k b : ℕ
h : b ≥ 0
rw rw₁ : b ≤ b
⊢ b ≤ (fun (x : ℕ) ↦ x + k) b - k

Tactic:
rw [Nat.add_sub_cancel_right]

Premises used: Nat.add_sub_cancel_right
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
k : ℕ
⊢ Tendsto (β := ℕ) (fun (a : ℕ) ↦ a + k) atTop atTop

Tactic:
le_of_eq (map_add_atTop_eq_nat k)

Premises used: Filter.Tendsto, Filter.map_add_atTop_eq_nat, le_of_eq
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
k : ℕ
⊢ Tendsto (β := ℕ) (fun (a : ℕ) ↦ a - k) atTop atTop

Tactic:
le_of_eq (map_sub_atTop_eq_nat k)

Premises used: Filter.map_sub_atTop_eq_nat, Filter.Tendsto, le_of_eq
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
f : ℕ → α
l : Filter α
k : ℕ
rw : Tendsto f (map (fun (n : ℕ) ↦ n + k) atTop) l ↔ Tendsto f atTop l
rw₁ rw₂ : Tendsto f atTop l ↔ Tendsto f atTop l
⊢ Tendsto (α := ℕ) (f ∘ fun (n : ℕ) ↦ n + k) atTop l ↔ Tendsto f atTop l

Tactic:
rw [← tendsto_map'_iff, map_add_atTop_eq_nat]

Premises used: Filter.tendsto_map'_iff, Filter.map_add_atTop_eq_nat
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
k : ℕ
hk : 0 < k
a b : ℕ
h : b ≥ 1
rw rw₁ : a ≤ k * b + (k - 1) ↔ a ≤ (fun (b : ℕ) ↦ k * b + (k - 1)) b
⊢ a / k ≤ b ↔ a ≤ (fun (b : ℕ) ↦ k * b + (k - 1)) b

Tactic:
rw [Nat.div_le_iff_le_mul_add_pred hk]

Premises used: Nat.div_le_iff_le_mul_add_pred
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
k : ℕ
hk : 0 < k
b : ℕ
h : b ≥ 1
rw : k - 1 < k
⊢ b ≤ (fun (b : ℕ) ↦ k * b + (k - 1)) b / k

Tactic:
rw [Nat.mul_add_div hk, Nat.div_eq_of_lt, Nat.add_zero]

Premises used: Nat.mul_add_div, Nat.add_zero, Nat.div_eq_of_lt
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
k : ℕ
hk : 0 < k
b : ℕ
h : b ≥ 1
⊢ k - 1 < k

Tactic:
lia
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_6
β : Type u_7
inst : SemilatticeInf α
f g : β → α
F : Filter β
hf : Tendsto f F atTop
hg : Tendsto g F atTop
rw :
  ∀ (hf : ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ f a) (hg : ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ g a) (b : α),
    ∀ᶠ (a : β) in F, b ≤ f a ⊓ g a
⊢ Tendsto.{u_7, u_6} (β := α) (fun (x : β) ↦ f x ⊓ g x) F atTop

Tactic:
rw [Filter.tendsto_atTop] at *

Premises used: Filter.tendsto_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_6
β : Type u_7
inst : SemilatticeInf α
f g : β → α
F : Filter β
hf : ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ f a
hg : ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ g a
⊢ ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ f a ⊓ g a

Tactic:
simp [eventually_and, hf, hg]

Premises used: Filter.eventually_and
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_6
β : Type u_7
inst : SemilatticeSup α
f g : β → α
F : Filter β
hf : Tendsto f F atBot
hg : Tendsto g F atBot
rw :
  ∀ (hf : ∀ (b : α), ∀ᶠ (a : β) in F, f a ≤ b) (hg : ∀ (b : α), ∀ᶠ (a : β) in F, g a ≤ b) (b : α),
    ∀ᶠ (a : β) in F, f a ⊔ g a ≤ b
⊢ Tendsto.{u_7, u_6} (β := α) (fun (x : β) ↦ f x ⊔ g x) F atBot

Tactic:
rw [Filter.tendsto_atBot] at *

Premises used: Filter.tendsto_atBot
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_6
β : Type u_7
inst : SemilatticeSup α
f g : β → α
F : Filter β
hf : ∀ (b : α), ∀ᶠ (a : β) in F, f a ≤ b
hg : ∀ (b : α), ∀ᶠ (a : β) in F, g a ≤ b
⊢ ∀ (b : α), ∀ᶠ (a : β) in F, f a ⊔ g a ≤ b

Tactic:
simp [eventually_and, hf, hg]

Premises used: Filter.eventually_and
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
inst_1 : l.NeBot
f : α → β
inst_2 : NoMaxOrder β
h : Tendsto f l atTop
M : β
hM : M ∈ upperBounds (range f)
⊢ ∀ (x : α), f x ≤ M

Tactic:
aesop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
inst_1 : l.NeBot
f : α → β
inst_2 : NoMaxOrder β
h : Tendsto f l atTop
M : β
hM : M ∈ upperBounds (range f)
⊢ ∀ (x : α), f x ≤ M

Tactic:
have : ∀ x, f x ≤ M := by aesop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
inst_1 : l.NeBot
f : α → β
inst_2 : NoMaxOrder β
h : Tendsto f l atTop
M : β
hM : M ∈ upperBounds (range f)
this : ∀ (x : α), f x ≤ M
⊢ ∅ = f ⁻¹' Ioi M

Tactic:
aesop (add forward safe not_le_of_gt)

Premises used: not_le_of_gt
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
inst_1 : l.NeBot
f : α → β
inst_2 : NoMaxOrder β
h : Tendsto f l atTop
M : β
hM : M ∈ upperBounds (range f)
this : ∀ (x : α), f x ≤ M
⊢ ∅ = f ⁻¹' Ioi M

Tactic:
have : ∅ = f ⁻¹' Ioi M := by aesop (add forward safe not_le_of_gt)
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
inst_1 : l.NeBot
f : α → β
inst_2 : NoMaxOrder β
h : Tendsto f l atTop
M : β
hM : M ∈ upperBounds (range f)
this_1 : ∀ (x : α), f x ≤ M
this : ∅ = f ⁻¹' Ioi M
apply : ∅ ∈ l
⊢ False

Tactic:
apply Filter.empty_notMem l

Premises used: Filter.empty_notMem
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
inst_1 : l.NeBot
f : α → β
inst_2 : NoMaxOrder β
h : Tendsto f l atTop
M : β
hM : M ∈ upperBounds (range f)
this_1 : ∀ (x : α), f x ≤ M
this : ∅ = f ⁻¹' Ioi M
⊢ ∅ ∈ l

Tactic:
aesop (add safe Ioi_mem_atTop)

Premises used: Filter.Ioi_mem_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
inst_1 : l.NeBot
f : α → β
inst_2 : NoMinOrder β
h : Tendsto f l atBot
⊢ ¬BddBelow (range f)

Tactic:
not_bddAbove_of_tendsto_atTop (β := βᵒᵈ) h

Premises used: Filter.not_bddAbove_of_tendsto_atTop, lowerBounds, Set.Mem, setOf, BddBelow, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder ι
l : Filter α
s : ι → Set α
hl : l.HasAntitoneBasis s
t : Set α
ht : t ∈ l
⊢ ∀ᶠ (i : ι) in atTop, s i ⊆ t

Tactic:
let ⟨i, _, hi⟩ := hl.1.mem_iff.1 ht
  (eventually_ge_atTop i).mono fun _j hj => (hl.antitone hj).trans hi

Premises used: _private.0.Filter.HasAntitoneBasis.eventually_subset.match_1, Filter.HasBasis.mem_iff, Filter.HasAntitoneBasis.toHasBasis, Filter.Eventually, HasSubset.Subset, Filter.Eventually.mono, Filter.atTop, Iff.mp, Filter.eventually_ge_atTop, Filter.HasAntitoneBasis.antitone, LE.le.trans
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder ι
l : Filter α
s : ι → Set α
hl : l.HasAntitoneBasis s
φ : ι → α
h : ∀ (i : ι), φ i ∈ s i
⊢ Tendsto φ atTop l

Tactic:
fun _t ht => mem_map.2 <| (hl.eventually_subset ht).mono fun i hi => hi (h i)

Premises used: Iff.mpr, Filter.Eventually.mono, Filter.HasAntitoneBasis.eventually_subset, Filter.Tendsto, Filter.mem_map
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Nonempty ι
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Preorder ι'
l : Filter α
s : ι' → Set α
hs : l.HasAntitoneBasis s
φ : ι → ι'
φ_mono : Monotone φ
hφ : Tendsto φ atTop atTop
⊢ l.HasAntitoneBasis (s ∘ φ)

Tactic:
⟨hs.1.to_hasBasis
      (fun n _ => (hφ.eventually_ge_atTop n).exists.imp fun _m hm => ⟨trivial, hs.antitone hm⟩)
      fun n _ => ⟨φ n, trivial, Subset.rfl⟩,
    hs.antitone.comp_monotone φ_mono⟩

Premises used: trivial, Filter.HasAntitoneBasis.toHasBasis, Antitone.comp_monotone, Exists.imp, Filter.HasAntitoneBasis.mk, Filter.Eventually.exists, Set.Subset.rfl, And.intro, Exists.intro, Filter.HasAntitoneBasis.antitone, Filter.Tendsto.eventually_ge_atTop, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
α : Type u_3
l : Filter α
s : ℕ → Set α
hs : l.HasAntitoneBasis s
φ : ℕ → ℕ
hφ : StrictMono φ
⊢ l.HasAntitoneBasis (s ∘ φ)

Tactic:
hs.comp_mono hφ.monotone hφ.tendsto_atTop

Premises used: StrictMono.monotone, StrictMono.tendsto_atTop, Filter.HasAntitoneBasis.comp_mono
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
ι : Type u_6
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : Tendsto x atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
choose :
  ∀ (ns : (a : ℕ) → ℕ) (hge : ∀ (a : ℕ), ns a ≥ a) (hns : ∀ (a : ℕ), p (x (ns a))),
    ∃ (ns : ℕ → ℕ), Tendsto (fun (n : ℕ) ↦ x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))
⊢ ∃ (ns : ℕ → ℕ), Tendsto (fun (n : ℕ) ↦ x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))

Tactic:
choose ns hge hns using frequently_atTop.1 h

Premises used: Filter.frequently_atTop, Iff.mp
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
ι : Type u_6
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : Tendsto x atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
ns : (a : ℕ) → ℕ
hge : ∀ (a : ℕ), ns a ≥ a
hns : ∀ (a : ℕ), p (x (ns a))
⊢ ∃ (ns : ℕ → ℕ), Tendsto (fun (n : ℕ) ↦ x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))

Tactic:
⟨ns, h_tendsto.comp (tendsto_atTop_mono hge tendsto_id), hns⟩

Premises used: Filter.tendsto_id, Filter.tendsto_atTop_mono, And.intro, Exists.intro, Filter.Tendsto.comp
-- Module: Mathlib.Order.Filter.AtTopBot.Basic
Goal:
ι : Type u_6
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : Tendsto x atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
ns : (a : ℕ) → ℕ
hge : ∀ (a : ℕ), ns a ≥ a
hns : ∀ (a : ℕ), p (x (ns a))
⊢ ∃ (ns : ℕ → ℕ), Tendsto (fun (n : ℕ) ↦ x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))

Tactic:
exact ⟨ns, h_tendsto.comp (tendsto_atTop_mono hge tendsto_id), hns⟩
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
f : α → M
g : β → M
h_eq :
  ∀ (u : Finset β),
    ∃ (v : Finset α),
      ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), u ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', g x) (∏ b ∈ v', f b)
⊢ LE.le.{u_3} (α := Filter M) (map (fun (s : Finset α) ↦ ∏ b ∈ s, f b) atTop)
    (map (fun (s : Finset β) ↦ ∏ x ∈ s, g x) atTop)

Tactic:
((atTop_basis.map _).le_basis_iff (atTop_basis.map _)).2 fun b _ => ?_

Premises used: Iff.mpr, Filter.atTop_basis, Filter.HasBasis.le_basis_iff, Filter.HasBasis.map
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
f : α → M
g : β → M
h_eq :
  ∀ (u : Finset β),
    ∃ (v : Finset α),
      ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), u ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', g x) (∏ b ∈ v', f b)
refine :
  ∀ (b : Finset β),
    True →
      ∃ (i : Finset α),
        True ∧
          Subset.{u_3} (α := Set M) ((fun (s : Finset α) ↦ ∏ b ∈ s, f b) '' Set.Ici i)
            ((fun (s : Finset β) ↦ ∏ x ∈ s, g x) '' Set.Ici b)
⊢ LE.le.{u_3} (α := Filter M) (map (fun (s : Finset α) ↦ ∏ b ∈ s, f b) atTop)
    (map (fun (s : Finset β) ↦ ∏ x ∈ s, g x) atTop)

Tactic:
refine ((atTop_basis.map _).le_basis_iff (atTop_basis.map _)).2 fun b _ => ?_

Premises used: Iff.mpr, Filter.atTop_basis, Filter.HasBasis.le_basis_iff, Filter.HasBasis.map
-- Module: Mathlib.Order.Filter.AtTopBot.BigOperators
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : CommMonoid M
f : α → M
g : β → M
h_eq :
  ∀ (u : Finset β),
    ∃ (v : Finset α),
      ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), u ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', g x) (∏ b ∈ v', f b)
b : Finset β
h : True
let :
  ∀ (v : Finset α)
    (hv :
      ∀ (v' : Finset α), v ⊆ v' → ∃ (u' : Finset β), b ⊆ u' ∧ Eq.{u_3 + 1} (α := M) (∏ x ∈ u', g x) (∏ b ∈ v', f b)),
    ∃ (i : Finset α),
      True ∧
        Subset.{u_3} (α := Set M) ((fun (s : Finset α) ↦ ∏ b ∈ s, f b) '' Set.Ici i)
          ((fun (s : Finset β) ↦ ∏ x ∈ s, g x) '' Set.Ici b)
⊢ ∃ (i : Finset α),
    True ∧
      Subset.{u_3} (α := Set M) ((fun (s : Finset α) ↦ ∏ b ∈ s, f b) '' Set.Ici i)
        ((fun (s : Finset β) ↦ ∏ x ∈ s, g x) '' Set.Ici b)

Tactic:
let ⟨v, hv⟩ := h_eq b