awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
a : α
⊢ TendstoIxxClass Ico (𝓟 (Ioi a)) (𝓟 (Ioi a))

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self

Premises used: Set.Ico_subset_Icc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
a : α
⊢ TendstoIxxClass Ico (𝓟 (Iic a)) (𝓟 (Iio a))

Tactic:
tendstoIxxClass_principal.2 fun _ _ _ h₁ _ h₂ => lt_of_lt_of_le h₂.2 h₁

Premises used: Iff.mpr, Filter.tendstoIxxClass_principal, And.right, lt_of_lt_of_le
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
a : α
⊢ TendstoIxxClass Ico (𝓟 (Iio a)) (𝓟 (Iio a))

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self

Premises used: Set.Ico_subset_Icc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
a : α
⊢ TendstoIxxClass Ioc (𝓟 (Ici a)) (𝓟 (Ioi a))

Tactic:
tendstoIxxClass_principal.2 fun _ h₁ _ _ _ h₂ => lt_of_le_of_lt h₁ h₂.1

Premises used: Iff.mpr, lt_of_le_of_lt, Filter.tendstoIxxClass_principal, And.left
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
a : α
⊢ TendstoIxxClass Ioc (𝓟 (Iic a)) (𝓟 (Iic a))

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
a : α
⊢ TendstoIxxClass Ioc (𝓟 (Iio a)) (𝓟 (Iio a))

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
a : α
⊢ TendstoIxxClass Ioc (𝓟 (Ioi a)) (𝓟 (Ioi a))

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
a : α
⊢ TendstoIxxClass Ioo (𝓟 (Ici a)) (𝓟 (Ioi a))

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Ioc_self

Premises used: Set.Ioo_subset_Ioc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
a : α
⊢ TendstoIxxClass Ioo (𝓟 (Iic a)) (𝓟 (Iio a))

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Ico_self

Premises used: Set.Ioo_subset_Ico_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
a : α
⊢ TendstoIxxClass Ioo (𝓟 (Ioi a)) (𝓟 (Ioi a))

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Ioc_self

Premises used: Set.Ioo_subset_Ioc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
a : α
⊢ TendstoIxxClass Ioo (𝓟 (Iio a)) (𝓟 (Iio a))

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Ioc_self

Premises used: Set.Ioo_subset_Ioc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
a b : α
⊢ TendstoIxxClass Icc (𝓟 (Icc a b)) (𝓟 (Icc a b))

Tactic:
tendstoIxxClass_principal.mpr fun _x hx _y hy => Icc_subset_Icc hx.1 hy.2

Premises used: Iff.mpr, Filter.tendstoIxxClass_principal, And.right, And.left, Set.Icc_subset_Icc
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
a b : α
⊢ TendstoIxxClass Ioc (𝓟 (Icc a b)) (𝓟 (Icc a b))

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
a : α
rw : TendstoIxxClass (α := α) Icc (𝓟 {a}) (𝓟 {a})
⊢ TendstoIxxClass Icc (pure a) (pure a)

Tactic:
rw [← principal_singleton]

Premises used: Filter.principal_singleton
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
a : α
⊢ TendstoIxxClass (α := α) Icc (𝓟 {a}) (𝓟 {a})

Tactic:
tendstoIxxClass_principal.2 ordConnected_singleton.out

Premises used: Iff.mpr, Set.OrdConnected.out, Filter.tendstoIxxClass_principal, Set.ordConnected_singleton
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
a : α
⊢ TendstoIxxClass (α := α) Icc (𝓟 {a}) (𝓟 {a})

Tactic:
exact tendstoIxxClass_principal.2 ordConnected_singleton.out

Premises used: Iff.mpr, Set.OrdConnected.out, Filter.tendstoIxxClass_principal, Set.ordConnected_singleton
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
a : α
⊢ Tendsto (β := Set α) (fun (p : α × α) ↦ Ico p.1 p.2) (SProd.sprod (α := Filter α) (β := Filter α) (pure a) (pure a))
    (smallSets ⊥)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
a : α
⊢ Tendsto (β := Set α) (fun (p : α × α) ↦ Ioc p.1 p.2) (SProd.sprod (α := Filter α) (β := Filter α) (pure a) (pure a))
    (smallSets ⊥)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
a : α
⊢ Tendsto (β := Set α) (fun (p : α × α) ↦ Ioo p.1 p.2) (SProd.sprod (α := Filter α) (β := Filter α) (pure a) (pure a))
    (smallSets ⊥)

Tactic:
simp
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
⊢ TendstoIxxClass Icc (𝓟 [[a, b]]) (𝓟 [[a, b]])

Tactic:
Filter.tendsto_Icc_Icc_Icc

Premises used: Filter.tendsto_Icc_Icc_Icc, Set.uIcc
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
⊢ TendstoIxxClass Ioc (𝓟 [[a, b]]) (𝓟 [[a, b]])

Tactic:
Filter.tendsto_Ioc_Icc_Icc

Premises used: Filter.tendsto_Ioc_Icc_Icc, Set.uIcc
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
⊢ TendstoIxxClass uIcc l l

Tactic:
⟨fun s hs => mem_map.2 <| mem_prod_self_iff.2 ?_⟩

Premises used: Iff.mpr, Filter.mem_prod_self_iff, Filter.TendstoIxxClass.mk, Filter.mem_map
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
refine : ∀ (s : Set (Set α)) (hs : s ∈ l.smallSets), ∃ t ∈ l, t ×ˢ t ⊆ (fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s
⊢ TendstoIxxClass uIcc l l

Tactic:
refine ⟨fun s hs => mem_map.2 <| mem_prod_self_iff.2 ?_⟩
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
⊢ ∃ t ∈ l, ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s

Tactic:
mem_prod_self_iff.1 (mem_map.1 (tendsto_fst.Icc tendsto_snd hs))

Premises used: Filter.mem_prod_self_iff, Filter.Tendsto.Icc, Set.Mem, Set.Subset, Iff.mp, Filter.tendsto_snd, Filter.mem_map, Filter.tendsto_fst
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
obtain :
  ∀ (t : Set α) (htl : t ∈ l) (hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s),
    ∃ t ∈ l, t ×ˢ t ⊆ (fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s
⊢ ∃ t ∈ l, t ×ˢ t ⊆ (fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s

Tactic:
obtain ⟨t, htl, hts⟩ : ∃ t ∈ l, ∀ p ∈ (t : Set α) ×ˢ t, Icc (p : α × α).1 p.2 ∈ s :=
    mem_prod_self_iff.1 (mem_map.1 (tendsto_fst.Icc tendsto_snd hs))

Premises used: Filter.mem_prod_self_iff, Filter.Tendsto.Icc, Iff.mp, Filter.tendsto_snd, Filter.mem_map, Filter.tendsto_fst
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
⊢ ∃ t ∈ l, t ×ˢ t ⊆ (fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s

Tactic:
⟨t, htl, fun p hp => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
refine : ∀ (p : α × α) (hp : p ∈ t ×ˢ t), Membership.mem (γ := Set (α × α)) ((fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s) p
⊢ ∃ t ∈ l, t ×ˢ t ⊆ (fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s

Tactic:
refine ⟨t, htl, fun p hp => ?_⟩
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
inl : ∀ (h : p.1 ≤ p.2), Membership.mem (γ := Set (α × α)) ((fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s) p
inr : ∀ (h : p.2 ≤ p.1), Membership.mem (γ := Set (α × α)) ((fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s) p
⊢ Membership.mem (γ := Set (α × α)) ((fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s) p

Tactic:
rcases le_total p.1 p.2 with h | h

Premises used: le_total, Prod.fst, Prod.snd
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.1 ≤ p.2
inl : Icc p.1 p.2 ∈ s
⊢ Membership.mem (γ := Set (α × α)) ((fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s) p

Tactic:
rw [mem_preimage, uIcc_of_le h]

Premises used: Set.uIcc_of_le, Set.mem_preimage
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.1 ≤ p.2
⊢ Icc p.1 p.2 ∈ s

Tactic:
hts p hp
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.1 ≤ p.2
⊢ Icc p.1 p.2 ∈ s

Tactic:
exact hts p hp
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.2 ≤ p.1
inr : Icc p.2 p.1 ∈ s
⊢ Membership.mem (γ := Set (α × α)) ((fun (p : α × α) ↦ [[p.1, p.2]]) ⁻¹' s) p

Tactic:
rw [mem_preimage, uIcc_of_ge h]

Premises used: Set.uIcc_of_ge, Set.mem_preimage
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.2 ≤ p.1
⊢ Icc p.2 p.1 ∈ s

Tactic:
hts ⟨p.2, p.1⟩ ⟨hp.2, hp.1⟩

Premises used: Set.Mem, Prod.mk, Prod.fst, And.right, And.left, And.intro, Prod.snd
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.2 ≤ p.1
⊢ Icc p.2 p.1 ∈ s

Tactic:
exact hts ⟨p.2, p.1⟩ ⟨hp.2, hp.1⟩

Premises used: Prod.mk, Prod.fst, And.right, And.left, And.intro, Prod.snd
-- Module: Mathlib.Order.Filter.Interval
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
l : Filter α
inst_1 : TendstoIxxClass Icc l l
f g : β → α
lb : Filter β
hf : Tendsto f lb l
hg : Tendsto g lb l
⊢ Tendsto (fun (x : β) ↦ [[f x, g x]]) lb l.smallSets

Tactic:
(@TendstoIxxClass.tendsto_Ixx α Set.uIcc _ _ _).comp <| hf.prodMk hg

Premises used: Filter.TendstoIxxClass.tendsto_Ixx, setOf, Set.Icc, Filter.Tendsto.prodMk, Filter.Tendsto.comp, Set.uIcc
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
r : α → α → Prop
f : Filter α
⊢ IsBounded r f ↔ ∃ s ∈ f.sets, ∃ (b : α), s ⊆ {x : α | r x b}

Tactic:
Iff.intro (fun ⟨b, hb⟩ => ⟨{ a | r a b }, hb, b, Subset.refl _⟩) fun ⟨_, hs, b, hb⟩ =>
    ⟨b, mem_of_superset hs hb⟩

Premises used: Set.Subset.refl, setOf, Membership.mem, Exists, Filter.sets, HasSubset.Subset, Filter.IsBounded, And, And.intro, Iff.intro, Exists.intro, _private.0.Filter.isBounded_iff.match_2, _private.0.Filter.isBounded_iff.match_1, Filter.mem_of_superset
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
r : α → α → Prop
⊢ IsBounded r ⊥ ↔ Nonempty α

Tactic:
simp [IsBounded, exists_true_iff_nonempty]

Premises used: exists_true_iff_nonempty, Filter.IsBounded
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
r : α → α → Prop
⊢ IsBounded r ⊤ ↔ ∃ (t : α), ∀ (x : α), r x t

Tactic:
simp [IsBounded]

Premises used: Filter.IsBounded
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
⊢ IsBounded r (𝓟 s) ↔ ∃ (t : α), ∀ x ∈ s, r x t

Tactic:
simp [IsBounded]

Premises used: Filter.IsBounded
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
f g : Filter β
u : β → α
h : f ≤ g
⊢ IsBoundedUnder r g u → IsBoundedUnder r f u

Tactic:
fun hg => IsBounded.mono (map_mono h) hg

Premises used: Filter.map_mono, Filter.IsBounded.mono, Filter.IsBoundedUnder
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l u
hv : v ≤ᶠ[l] u
apply :
  ∀ (a : β),
    (∀ᶠ (x : β) in map u l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → ∀ᶠ (x : β) in map v l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l v

Tactic:
apply hu.imp

Premises used: Exists.imp
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l u
hv : v ≤ᶠ[l] u
⊢ ∀ (a : β),
    (∀ᶠ (x : β) in map u l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → ∀ᶠ (x : β) in map v l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a

Tactic:
fun b hb => (eventually_map.1 hb).mp <| hv.mono fun x => le_trans

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.eventually_map, Filter.Eventually.mono, Filter.Eventually.mp, Set.preimage, Iff.mp, le_trans
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l u
hv : v ≤ᶠ[l] u
⊢ ∀ (a : β),
    (∀ᶠ (x : β) in map u l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → ∀ᶠ (x : β) in map v l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a

Tactic:
exact fun b hb => (eventually_map.1 hb).mp <| hv.mono fun x => le_trans

Premises used: Filter.eventually_map, Filter.Eventually.mono, Filter.Eventually.mp, Iff.mp, le_trans
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) l u
hv : u ≤ᶠ[l] v
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) l v

Tactic:
IsBoundedUnder.mono_le (β := βᵒᵈ) hu hv

Premises used: Filter.IsBoundedUnder.mono_le, OrderDual
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
inst : Std.Refl r
l : Filter β
a : α
⊢ IsBoundedUnder r l fun (x : β) ↦ a

Tactic:
⟨a, eventually_map.2 <| Eventually.of_forall fun _ => refl _⟩

Premises used: Iff.mpr, Filter.Eventually.of_forall, Filter.IsBounded, Filter.eventually_map, Exists.intro, refl, Filter.IsBoundedUnder
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
ι : Type u_5
κ : Type u_6
X : Type u_7
r : X → X → Prop
f : ι → X
φ : κ → ι
𝓕 : Filter κ
⊢ IsBoundedUnder r (map φ 𝓕) f ↔ IsBoundedUnder r 𝓕 (f ∘ φ)

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.map, Iff.rfl, setOf, Set.preimage, Filter.IsBoundedUnder
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
ι : Type u_5
κ : Type u_6
X : Type u_7
r : X → X → Prop
f : ι → X
φ : κ → ι
𝓕 : Filter ι
𝓖 : Filter κ
φ_tendsto : Tendsto φ 𝓖 𝓕
𝓕_bounded : IsBoundedUnder r 𝓕 f
⊢ IsBoundedUnder r 𝓖 (f ∘ φ)

Tactic:
isBoundedUnder_map_iff.mp (𝓕_bounded.mono φ_tendsto)

Premises used: Filter.isBoundedUnder_map_iff, Filter.IsBoundedUnder.mono, Iff.mp
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
⊢ ∃ (a : α), ∀ᶠ (x : β) in f, u x ≤ a

Tactic:
tauto
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
⊢ ∃ (a : α), ∀ᶠ (x : β) in f, a ≤ u x

Tactic:
IsBoundedUnder.eventually_le (α := αᵒᵈ) h

Premises used: Filter.IsBoundedUnder.eventually_le, OrderDual
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
a : α
h : ∀ᶠ (x : β) in f, u x ≤ a
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u

Tactic:
⟨a, h⟩

Premises used: Filter.IsBounded, Exists.intro, Filter.IsBoundedUnder
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
a : α
h : ∀ᶠ (x : β) in f, a ≤ u x
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u

Tactic:
⟨a, h⟩

Premises used: Filter.IsBounded, Exists.intro, Filter.IsBoundedUnder
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
mp : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u → ∃ (s : Set β), BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s
mpr : (∃ (s : Set β), BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s) → IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u ↔ ∃ (s : Set β), BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s

Tactic:
constructor
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
b : α
hb : ∀ᶠ (x : α) in map u f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x b
a : β
ha : Membership.mem (γ := Set β) {a : β | u a ≤ b} a
⊢ u a ≤ b

Tactic:
ha

Premises used: Set.Mem, setOf
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
b : α
hb : ∀ᶠ (x : α) in map u f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x b
a : β
ha : Membership.mem (γ := Set β) {a : β | u a ≤ b} a
⊢ u a ≤ b

Tactic:
exact ha
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
b : α
hb : ∀ᶠ (x : α) in map u f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x b
⊢ ∃ (s : Set β), BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s

Tactic:
exact ⟨{a | u a ≤ b}, ⟨b, by rintro _ ⟨a, ha, rfl⟩; exact ha⟩, hb⟩
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
s : Set β
hs : ∀ᶠ (x : β) in f, x ∈ s
b : α
hb : b ∈ upperBounds (u '' s)
⊢ ∀ x ∈ s, Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ((fun (x1 x2 : α) ↦ x1 ≤ x2) x b : Prop)) x} (u x)

Tactic:
simpa [upperBounds] using hb

Premises used: upperBounds
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
s : Set β
hs : ∀ᶠ (x : β) in f, x ∈ s
b : α
hb : b ∈ upperBounds (u '' s)
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u

Tactic:
exact ⟨b, hs.mono <| by simpa [upperBounds] using hb⟩
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u ↔ ∃ (s : Set β), BddBelow (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s

Tactic:
isBoundedUnder_iff_eventually_bddAbove (α := αᵒᵈ)

Premises used: lowerBounds, Set.Mem, setOf, Filter.isBoundedUnder_iff_eventually_bddAbove, BddBelow, OrderDual
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
s : Set β
hs : s ∈ f
hu : BddAbove (u '' s)
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u

Tactic:
isBoundedUnder_iff_eventually_bddAbove.2 ⟨_, hu, hs⟩

Premises used: Iff.mpr, Filter.isBoundedUnder_iff_eventually_bddAbove, And.intro, Exists.intro
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
hu : BddAbove (range u)
⊢ BddAbove (u '' univ)

Tactic:
simpa
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
s : Set β
hs : s ∈ f
hu : BddBelow (u '' s)
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u

Tactic:
isBoundedUnder_iff_eventually_bddBelow.2 ⟨_, hu, hs⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Filter.isBoundedUnder_iff_eventually_bddBelow
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
f : Filter β
u : β → α
hu : BddBelow (range u)
⊢ BddBelow (u '' univ)

Tactic:
simpa
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
inst_3 : Finite β
f : Filter β
u : β → α
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u

Tactic:
(Set.toFinite _).bddAbove.isBoundedUnder_of_range

Premises used: Set.toFinite, BddAbove.isBoundedUnder_of_range, Set.Finite.bddAbove
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsCodirectedOrder α
inst_3 : Finite β
f : Filter β
u : β → α
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u

Tactic:
(Set.toFinite _).bddBelow.isBoundedUnder_of_range

Premises used: BddBelow.isBoundedUnder_of_range, Set.Finite.bddBelow, Set.toFinite
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
l : Filter γ
u : γ → α
v : α → β
hv : Monotone v
hl : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) l u
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l (v ∘ u)

Tactic:
hl.comp hv

Premises used: Filter.IsBoundedUnder.comp
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
l : Filter γ
u : γ → α
v : α → β
hv : Monotone v
hl : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) l u
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) l (v ∘ u)

Tactic:
hl.comp (swap hv)

Premises used: Function.swap, Filter.IsBoundedUnder.comp
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
l : Filter γ
u : γ → α
v : α → β
hv : Antitone v
hl : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) l u
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l (v ∘ u)

Tactic:
hl.comp (swap hv)

Premises used: Function.swap, Filter.IsBoundedUnder.comp
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
l : Filter γ
u : γ → α
v : α → β
hv : Antitone v
hl : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) l u
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) l (v ∘ u)

Tactic:
hl.comp hv

Premises used: Filter.IsBoundedUnder.comp
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : NoMaxOrder β
f : α → β
l : Filter α
inst_2 : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (x : β) in map f l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b
⊢ ∀ᶠ (a : α) in l, (fun (x1 x2 : β) ↦ x1 ≤ x2) (f a) b

Tactic:
rw [eventually_map] at hb

Premises used: Filter.eventually_map
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : NoMaxOrder β
f : α → β
l : Filter α
inst_2 : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun (x1 x2 : β) ↦ x1 ≤ x2) (f a) b
obtain : ∀ (b' : β) (h : b < b'), False
⊢ False

Tactic:
obtain ⟨b', h⟩ := exists_gt b

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : NoMaxOrder β
f : α → β
l : Filter α
inst_2 : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun (x1 x2 : β) ↦ x1 ≤ x2) (f a) b
b' : β
h : b < b'
⊢ ∀ᶠ (a : α) in l, b' ≤ f a

Tactic:
have hb' := (tendsto_atTop.mp hf) b'