awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in SProd.sprod (α := Filter α) (β := Filter β) atTop atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)

Tactic:
hp.curry

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

Tactic:
exact hp.curry

Premises used: Filter.Eventually.curry
-- Module: Mathlib.Order.Filter.AtTopBot.Prod
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atBot, p x
⊢ ∀ᶠ (k : α) in atBot, ∀ᶠ (l : β) in atBot, p (k, l)

Tactic:
@eventually_atTop_curry αᵒᵈ βᵒᵈ _ _ _ hp

Premises used: setOf, Filter.eventually_atTop_curry, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atTop

Tactic:
tendsto_atTop_mono' _ ?_ hg

Premises used: Filter.tendsto_atTop_mono'
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
refine : g ≤ᶠ[l] fun (x : β) ↦ f x * g x
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atTop

Tactic:
refine tendsto_atTop_mono' _ ?_ hg

Premises used: Filter.tendsto_atTop_mono'
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
a : β
⊢ 0 ≤ g a → 1 ≤ f a → g a ≤ f a * g a

Tactic:
le_mul_of_one_le_left

Premises used: le_mul_of_one_le_left
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ 0 ≤ g x) x} x →
          Membership.mem (γ := Set β)
            {x : β |
              Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ 1 ≤ f x) x} x →
                Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ g x ≤ (fun (x : β) ↦ f x * g x) x) x} x}
            x}
      a
h₁ h₂ : ∀ (a : β), 0 ≤ g a → 1 ≤ f a → g a ≤ f a * g a
⊢ g ≤ᶠ[l] fun (x : β) ↦ f x * g x

Tactic:
filter_upwards [hg.eventually (eventually_ge_atTop 0),
    hf.eventually (eventually_ge_atTop 1)] with _ using le_mul_of_one_le_left

Premises used: le_mul_of_one_le_left, Filter.Tendsto.eventually, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
⊢ Tendsto (β := α) (fun (x : α) ↦ x * x) atTop atTop

Tactic:
tendsto_id.atTop_mul_atTop₀ tendsto_id

Premises used: Filter.tendsto_id, Filter.Tendsto.atTop_mul_atTop₀
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
n : ℕ
hn : n ≠ 0
⊢ Tendsto (β := α) (fun (x : α) ↦ x ^ n) atTop atTop

Tactic:
tendsto_atTop_mono' _ ((eventually_ge_atTop 1).mono fun _x hx => le_self_pow₀ hx hn) tendsto_id

Premises used: Filter.tendsto_id, Filter.Eventually.mono, Filter.tendsto_atTop_mono', le_self_pow₀, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
inst : MonoidWithZero α
⊢ EventuallyEq.{0, u_1} (β := α) atTop (fun (n : ℕ) ↦ HPow.hPow (α := α) 0 n) fun (x : ℕ) ↦ 0

Tactic:
eventually_atTop.2 ⟨1, fun _n hn ↦ zero_pow <| Nat.one_le_iff_ne_zero.1 hn⟩

Premises used: Iff.mpr, Filter.EventuallyEq, Exists.intro, Iff.mp, Nat.one_le_iff_ne_zero, Filter.eventually_atTop, OfNat.ofNat, zero_pow
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * (Neg.neg ∘ g) x) l atTop

Tactic:
have := hf.atTop_mul_atTop₀ <| tendsto_neg_atBot_atTop.comp hg
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atBot
this : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * (Neg.neg ∘ g) x) l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atBot

Tactic:
simpa only [Function.comp_def, neg_mul_eq_mul_neg, neg_neg] using
    tendsto_neg_atTop_atBot.comp this

Premises used: Filter.tendsto_neg_atTop_atBot, neg_neg, Function.comp_def, neg_mul_eq_mul_neg, Filter.Tendsto.comp
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ -f x * g x) l atTop

Tactic:
have : Tendsto (fun x => -f x * g x) l atTop :=
    (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop₀ hg
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atTop
this : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ -f x * g x) l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atBot

Tactic:
simpa only [Function.comp_def, neg_mul_eq_neg_mul, neg_neg] using
    tendsto_neg_atTop_atBot.comp this

Premises used: Filter.tendsto_neg_atTop_atBot, neg_neg, Function.comp_def, neg_mul_eq_neg_mul, Filter.Tendsto.comp
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ -f x * -g x) l atTop

Tactic:
have : Tendsto (fun x => -f x * -g x) l atTop :=
    (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop₀ (tendsto_neg_atBot_atTop.comp hg)
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
β : Type u_2
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atBot
this : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ -f x * -g x) l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atTop

Tactic:
simpa only [neg_mul_neg] using this

Premises used: neg_mul_neg
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
c : α
hc : 0 < c
hf : Tendsto.{u_2, u_1} (β := α) (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 _x hx => le_of_mul_le_mul_left hx hc

Premises used: Iff.mpr, HMul.hMul, Filter.tendsto_atTop, Filter.Eventually.mono, le_of_mul_le_mul_left, Iff.mp
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
β : Type u_2
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
l : Filter β
f : β → α
c : α
hc : 0 < c
hf : Tendsto.{u_2, u_1} (β := α) (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 _x hx => le_of_mul_le_mul_right hx hc

Premises used: Iff.mpr, HMul.hMul, le_of_mul_le_mul_right, Filter.tendsto_atTop, Filter.Eventually.mono, Iff.mp
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n : ℕ
h : Tendsto (β := α) (fun (x : α) ↦ x ^ n) atTop atTop
hn : n = 0
⊢ False

Tactic:
simp only [hn, pow_zero, not_tendsto_const_atTop] at h

Premises used: pow_zero, Filter.not_tendsto_const_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
⊢ ¬Tendsto (β := α) (fun (x : α) ↦ HPow.hPow (β := ℕ) x 0) atTop atBot

Tactic:
simp [not_tendsto_const_atBot]

Premises used: Filter.not_tendsto_const_atBot
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
⊢ ∃ x ≥ 0, a < x * x

Tactic:
((eventually_ge_atTop 0).and (tendsto_mul_self_atTop.eventually (eventually_gt_atTop a))).exists

Premises used: Filter.Eventually.and, Filter.Eventually.exists, Filter.Tendsto.eventually, Filter.eventually_ge_atTop, Filter.tendsto_mul_self_atTop, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Ring
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a : R
⊢ ∃ x ≥ 0, a ≤ x * x

Tactic:
let ⟨x, hx0, hxa⟩ := exists_lt_mul_self a
  ⟨x, hx0, hxa.le⟩

Premises used: HMul.hMul, exists_lt_mul_self, Exists, GE.ge, LT.lt.le, LE.le, And, And.intro, Exists.intro, _private.0.exists_le_mul_self.match_1, OfNat.ofNat
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : NoTopOrder α
x : α
l : Filter β
inst_2 : l.NeBot
⊢ ¬Tendsto.{u_4, u_3} (β := α) (fun (x_1 : β) ↦ x) l atTop

Tactic:
tendsto_const_pure.not_tendsto (disjoint_pure_atTop x)

Premises used: Filter.Tendsto.not_tendsto, Filter.tendsto_const_pure, Filter.disjoint_pure_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
f : α → β
l : Filter α
hf : Tendsto f l atTop
c : β
⊢ ∀ᶠ (x : α) in l, c ≤ f x

Tactic:
hf.eventually (eventually_ge_atTop c)

Premises used: Filter.Tendsto.eventually, Filter.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
inst_1 : NoTopOrder β
f : α → β
l : Filter α
hf : Tendsto f l atTop
c : β
⊢ ∀ᶠ (x : α) in l, f x ≠ c

Tactic:
hf.eventually (eventually_ne_atTop c)

Premises used: Filter.eventually_ne_atTop, Filter.Tendsto.eventually
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
inst_1 : NoTopOrder β
f : α → β
l : Filter α
hf : Tendsto f l atTop
c : α
⊢ ∀ᶠ (x : α) in l, x ≠ c

Tactic:
(hf.eventually_ne_atTop (f c)).mono fun _ => ne_of_apply_ne f

Premises used: Filter.Tendsto.eventually_ne_atTop, ne_of_apply_ne, Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_6
inst : PartialOrder α
inst_1 : OrderTop α
rw : Eq.{u_6 + 1} (α := Filter α) (𝓟 (Ici ⊤)) (pure ⊤)
rw₁ : Eq (α := Filter α) (𝓟 {⊤}) (pure ⊤)
rw₂ rw₃ : Eq.{u_6 + 1} (α := Filter α) (pure ⊤) (pure ⊤)
⊢ Eq.{u_6 + 1} (α := Filter α) atTop (pure ⊤)

Tactic:
rw [isTop_top.atTop_eq, Ici_top, principal_singleton]

Premises used: IsTop.atTop_eq, Set.Ici_top, Filter.principal_singleton, isTop_top
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : OrderTop α
f : α → β
⊢ Tendsto f atTop (pure (f ⊤))

Tactic:
(OrderTop.atTop_eq α).symm ▸ tendsto_pure_pure _ _

Premises used: Filter.tendsto_pure_pure, Eq.rec, Filter.OrderTop.atTop_eq, Eq.symm
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
m : α → β
f : Filter α
⊢ Tendsto m f atTop ↔ ∀ (b : β), ∀ᶠ (a : α) in f, b ≤ m a

Tactic:
simp only [atTop, tendsto_iInf, tendsto_principal, mem_Ici]

Premises used: Filter.tendsto_principal, Filter.atTop, Set.mem_Ici, Filter.tendsto_iInf
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
f₁ f₂ : α → β
h : f₁ ≤ᶠ[l] f₂
h₁ : Tendsto f₁ l atTop
b : β
x : α
⊢ b ≤ f₁ x → f₁ x ≤ f₂ x → b ≤ f₂ x

Tactic:
le_trans

Premises used: le_trans
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
f₁ f₂ : α → β
h : f₁ ≤ᶠ[l] f₂
h₁ : Tendsto f₁ l atTop
b : β
h₂ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ b ≤ f₁ a) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f₁ x ≤ f₂ x) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ b ≤ f₂ a) x} x}
            x}
      a
h₃ h₄ : ∀ (x : α), b ≤ f₁ x → f₁ x ≤ f₂ x → b ≤ f₂ x
⊢ ∀ᶠ (a : α) in l, b ≤ f₂ a

Tactic:
filter_upwards [tendsto_atTop.1 h₁ b, h] with x using le_trans

Premises used: Filter.tendsto_atTop, Iff.mp, le_trans
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
inst : Preorder β
l : Filter α
f g : α → β
h : ∀ (n : α), f n ≤ g n
⊢ Tendsto f l atTop → Tendsto g l atTop

Tactic:
tendsto_atTop_mono' l <| Eventually.of_forall h

Premises used: Filter.Eventually.of_forall, Filter.tendsto_atTop_mono'
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
φ : ℕ → ℕ
h : StrictMono φ
⊢ Tendsto φ atTop atTop

Tactic:
tendsto_atTop_mono h.id_le tendsto_id

Premises used: Filter.tendsto_id, Filter.tendsto_atTop_mono, StrictMono.id_le
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : Preorder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
⊢ upperBounds (range (f ∘ g)) = upperBounds (range f)

Tactic:
Subset.antisymm ?_ (upperBounds_mono_set <| range_comp_subset_range _ _)

Premises used: Set.Subset.antisymm, Set.range_comp_subset_range, upperBounds_mono_set
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : Preorder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
refine : upperBounds (range (f ∘ g)) ⊆ upperBounds (range f)
⊢ upperBounds (range (f ∘ g)) = upperBounds (range f)

Tactic:
refine Subset.antisymm ?_ (upperBounds_mono_set <| range_comp_subset_range _ _)

Premises used: Set.Subset.antisymm, Set.range_comp_subset_range, upperBounds_mono_set
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : Preorder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
c : γ
hc : c ∈ upperBounds (range (f ∘ g))
b : β
⊢ ∃ (a : α), b ≤ g a

Tactic:
(hg.eventually_ge_atTop b).exists

Premises used: Filter.Eventually.exists, Filter.Tendsto.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : Preorder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
c : γ
hc : c ∈ upperBounds (range (f ∘ g))
b : β
obtain : ∀ (a : α) (ha : b ≤ g a), f b ≤ c
⊢ f b ≤ c

Tactic:
obtain ⟨a, ha⟩ : ∃ a, b ≤ g a := (hg.eventually_ge_atTop b).exists

Premises used: Filter.Eventually.exists, Filter.Tendsto.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : Preorder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
c : γ
hc : c ∈ upperBounds (range (f ∘ g))
b : β
a : α
ha : b ≤ g a
⊢ f b ≤ c

Tactic:
(hf ha).trans <| hc <| mem_range_self _

Premises used: Set.mem_range_self, LE.le.trans
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : Preorder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
c : γ
hc : c ∈ upperBounds (range (f ∘ g))
b : β
a : α
ha : b ≤ g a
⊢ f b ≤ c

Tactic:
exact (hf ha).trans <| hc <| mem_range_self _

Premises used: Set.mem_range_self, LE.le.trans
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : Preorder γ
l : Filter α
inst_2 : l.NeBot
f : β → γ
hf : Antitone f
g : α → β
hg : Tendsto g l atTop
⊢ lowerBounds (range (f ∘ g)) = lowerBounds (range f)

Tactic:
hf.dual_left.lowerBounds_range_comp_tendsto_atBot hg

Premises used: Monotone.lowerBounds_range_comp_tendsto_atBot, Antitone.dual_left, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Monotone f
h : ∀ (b : β), ∃ (a : α), b ≤ f a
⊢ Tendsto f atTop atTop

Tactic:
tendsto_iInf.2 fun b =>
    tendsto_principal.2 <|
      let ⟨a, ha⟩ := h b
      mem_of_superset (mem_atTop a) fun _a' ha' => le_trans ha (hf ha')

Premises used: Iff.mpr, Set.Ici, Filter.mem_atTop, Filter.Eventually, Membership.mem, Filter.tendsto_principal, Filter.atTop, _private.0.Filter.tendsto_atTop_atTop_of_monotone.match_1, Filter.tendsto_iInf, le_trans, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : Antitone f
h : ∀ (b : β), ∃ (a : α), f a ≤ b
⊢ Tendsto f atTop atBot

Tactic:
@tendsto_atTop_atTop_of_monotone _ βᵒᵈ _ _ _ hf h

Premises used: setOf, Filter.tendsto_atTop_atTop_of_monotone, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : Preorder γ
e : β → γ
hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂
hu : ∀ (c : γ), ∃ (b : β), c ≤ e b
⊢ comap e atTop = atTop

Tactic:
le_antisymm
    (le_iInf fun b =>
      le_principal_iff.2 <| mem_comap.2 ⟨Ici (e b), mem_atTop _, fun _ => (hm _ _).1⟩)
    (tendsto_atTop_atTop_of_monotone (fun _ _ => (hm _ _).2) hu).le_comap

Premises used: Iff.mpr, Filter.Tendsto.le_comap, Set.Ici, Filter.le_principal_iff, Filter.mem_atTop, le_iInf, Filter.tendsto_atTop_atTop_of_monotone, Filter.mem_comap, le_antisymm, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Preorder β
inst_1 : Preorder γ
f : α → β
e : β → γ
l : Filter α
hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂
hu : ∀ (c : γ), ∃ (b : β), c ≤ e b
rw : Tendsto (e ∘ f) l atTop ↔ Tendsto f l (comap e atTop)
rw₁ rw₂ : Tendsto (e ∘ f) l atTop ↔ Tendsto (e ∘ f) l atTop
⊢ Tendsto (e ∘ f) l atTop ↔ Tendsto f l atTop

Tactic:
rw [← comap_embedding_atTop hm hu, tendsto_comap_iff]

Premises used: Filter.tendsto_comap_iff, Filter.comap_embedding_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder ι
inst_1 : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
apply : ∀ (b : α), ∃ (a : ι), b ≤ u a
⊢ Tendsto u atTop atTop

Tactic:
apply h.tendsto_atTop_atTop

Premises used: Monotone.tendsto_atTop_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder ι
inst_1 : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
b : α
rcases : ∀ (N : ι) (hN : b < u N), ∃ (a : ι), b ≤ u a
⊢ ∃ (a : ι), b ≤ u a

Tactic:
rcases not_bddAbove_iff.1 H b with ⟨_, ⟨N, rfl⟩, hN⟩

Premises used: Iff.mp, not_bddAbove_iff, rfl
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder ι
inst_1 : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
b : α
N : ι
hN : b < u N
⊢ ∃ (a : ι), b ≤ u a

Tactic:
⟨N, le_of_lt hN⟩

Premises used: le_of_lt, Exists.intro
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder ι
inst_1 : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
b : α
N : ι
hN : b < u N
⊢ ∃ (a : ι), b ≤ u a

Tactic:
exact ⟨N, le_of_lt hN⟩
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
ι : Type u_1
α : Type u_3
inst : Preorder ι
inst_1 : Preorder α
l : Filter ι
u : ι → α
h : Monotone u
inst_2 : l.NeBot
hu : Tendsto u l atTop
⊢ Tendsto u atTop atTop

Tactic:
h.tendsto_atTop_atTop fun b => (hu.eventually (mem_atTop b)).exists

Premises used: Filter.mem_atTop, Filter.Eventually.exists, Filter.Tendsto.eventually, Monotone.tendsto_atTop_atTop
-- Module: Mathlib.Order.Filter.AtTopBot.Tendsto
Goal:
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst : Preorder ι
inst_1 : Preorder α
u : ι → α
φ : ι' → ι
h : Monotone u
l : Filter ι'
inst_2 : l.NeBot
H : Tendsto (u ∘ φ) l atTop
⊢ Tendsto u atTop atTop

Tactic:
tendsto_atTop_of_monotone_of_filter h (tendsto_map' H)

Premises used: Filter.tendsto_map', Filter.tendsto_atTop_of_monotone_of_filter
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
B : FilterBasis α
⊢ Nonempty.{u_1 + 1} (↑B.sets : Type u_1)

Tactic:
B.nonempty.to_subtype

Premises used: Set.Nonempty.to_subtype, FilterBasis.nonempty
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
s : Set α
B : FilterBasis α
⊢ s ∈ B.sets ↔ s ∈ B

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
n m : ℕ
⊢ ∃ (z : Set ℕ), Membership.mem (γ := Set (Set ℕ)) (range Ici) z ∧ z ⊆ Ici n ∩ Ici m

Tactic:
⟨Ici (max n m), mem_range_self _, Ici_inter_Ici.symm.subset⟩

Premises used: Set.mem_range_self, Set.Ici, Eq.subset, Max.max, And.intro, Exists.intro, Set.Ici_inter_Ici, Eq.symm
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
n m : ℕ
⊢ ∃ (z : Set ℕ), Membership.mem (γ := Set (Set ℕ)) (range Ici) z ∧ z ⊆ Ici n ∩ Ici m

Tactic:
exact ⟨Ici (max n m), mem_range_self _, Ici_inter_Ici.symm.subset⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
p : ι → Prop
s : ι → Set α
h : IsBasis p s
i : ι
hi : p i
j : ι
hj : p j
rcases :
  ∀ (k : ι) (hk : p k) (hk' : s k ⊆ s i ∩ s j),
    ∃ (z : Set α), Membership.mem (γ := Set (Set α)) {t : Set α | ∃ (i : ι), p i ∧ s i = t} z ∧ z ⊆ s i ∩ s j
⊢ ∃ (z : Set α), Membership.mem (γ := Set (Set α)) {t : Set α | ∃ (i : ι), p i ∧ s i = t} z ∧ z ⊆ s i ∩ s j

Tactic:
rcases h.inter hi hj with ⟨k, hk, hk'⟩

Premises used: Filter.IsBasis.inter
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
p : ι → Prop
s : ι → Set α
h : IsBasis p s
i : ι
hi : p i
j : ι
hj : p j
k : ι
hk : p k
hk' : s k ⊆ s i ∩ s j
⊢ ∃ (z : Set α), Membership.mem (γ := Set (Set α)) {t : Set α | ∃ (i : ι), p i ∧ s i = t} z ∧ z ⊆ s i ∩ s j

Tactic:
⟨_, ⟨k, hk, rfl⟩, hk'⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
p : ι → Prop
s : ι → Set α
h : IsBasis p s
i : ι
hi : p i
j : ι
hj : p j
k : ι
hk : p k
hk' : s k ⊆ s i ∩ s j
⊢ ∃ (z : Set α), Membership.mem (γ := Set (Set α)) {t : Set α | ∃ (i : ι), p i ∧ s i = t} z ∧ z ⊆ s i ∩ s j

Tactic:
exact ⟨_, ⟨k, hk, rfl⟩, hk'⟩
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
U : Set α
⊢ U ∈ h.filterBasis (p := p) (s := s) ↔ ∃ (i : ι), p i ∧ s i = U

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
U : Set α
⊢ U ∈ B.filter ↔ ∃ s ∈ B, s ⊆ U

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Filter.Bases.Basic
Goal:
α : Type u_1
B : FilterBasis α
U : Set α
⊢ U ∈ B → U ∈ B.filter

Tactic:
fun U_in =>
  ⟨U, U_in, Subset.refl _⟩

Premises used: Set.Subset.refl, Set.Mem, setOf, And.intro, Exists.intro