awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
h : s.Nonempty
⊢ f (sSup s) = sSup (f '' s)

Tactic:
exact Mf.map_csSup_of_continuousWithinAt Cf h

Premises used: MonotoneOn.map_csSup_of_continuousWithinAt
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousAt f (sSup s)
Mf : Monotone f
fbot : f ⊥ = ⊥
⊢ f (sSup s) = sSup (f '' s)

Tactic:
MonotoneOn.map_sSup_of_continuousWithinAt Cf.continuousWithinAt (Mf.monotoneOn _) fbot

Premises used: ContinuousAt.continuousWithinAt, Monotone.monotoneOn, MonotoneOn.map_sSup_of_continuousWithinAt
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
fbot : f ⊥ = ⊥
rw : f (sSup (range fun (i : ι) ↦ g i)) = ⨆ (i : ι), f (g i)
rw₁ : sSup (f '' range g) = ⨆ (i : ι), f (g i)
rw₂ : sSup (range (f ∘ g)) = ⨆ (i : ι), f (g i)
rw₃ : sSup (range (f ∘ g)) = sSup (range fun (i : ι) ↦ f (g i))
rw₄ rw₅ : Eq.{u_2 + 1} (α := β) (sSup (range fun (x : ι) ↦ f (g x))) (sSup (range fun (i : ι) ↦ f (g i)))
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

Tactic:
rw [iSup, Mf.map_sSup_of_continuousAt Cf fbot, ← range_comp, iSup, comp_def]

Premises used: Set.range_comp, iSup, Function.comp_def, Monotone.map_sSup_of_continuousAt
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sInf s)
Mf : MonotoneOn f s
ftop : f ⊤ = ⊤
⊢ f (sInf s) = sInf (f '' s)

Tactic:
MonotoneOn.map_sSup_of_continuousWithinAt (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual ftop

Premises used: MonotoneOn.dual, OrderDual, MonotoneOn.map_sSup_of_continuousWithinAt
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousAt f (sInf s)
Mf : Monotone f
ftop : f ⊤ = ⊤
⊢ f (sInf s) = sInf (f '' s)

Tactic:
Monotone.map_sSup_of_continuousAt (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual ftop

Premises used: Monotone.dual, OrderDual, Monotone.map_sSup_of_continuousAt
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Mf : Monotone f
ftop : f ⊤ = ⊤
⊢ f (iInf g) = iInf (f ∘ g)

Tactic:
Monotone.map_iSup_of_continuousAt (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual ftop

Premises used: iInf, Monotone.dual, Monotone.map_iSup_of_continuousAt, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Af : AntitoneOn f s
fbot : f ⊥ = ⊤
⊢ f (sSup s) = sInf (f '' s)

Tactic:
MonotoneOn.map_sSup_of_continuousWithinAt
    (show ContinuousWithinAt (OrderDual.toDual ∘ f) s (sSup s) from Cf) Af fbot

Premises used: OrderDual, MonotoneOn.map_sSup_of_continuousWithinAt
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousAt f (sSup s)
Af : Antitone f
fbot : f ⊥ = ⊤
⊢ f (sSup s) = sInf (f '' s)

Tactic:
Monotone.map_sSup_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (sSup s) from Cf) Af
    fbot

Premises used: OrderDual, Monotone.map_sSup_of_continuousAt
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Af : Antitone f
fbot : f ⊥ = ⊤
⊢ f (⨆ (i : ι), g i) = ⨅ (i : ι), f (g i)

Tactic:
Monotone.map_iSup_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (iSup g) from Cf) Af
    fbot

Premises used: iInf, Monotone.map_iSup_of_continuousAt, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sInf s)
Af : AntitoneOn f s
ftop : f ⊤ = ⊥
⊢ f (sInf s) = sSup (f '' s)

Tactic:
MonotoneOn.map_sInf_of_continuousWithinAt
    (show ContinuousWithinAt (OrderDual.toDual ∘ f) s (sInf s) from Cf) Af ftop

Premises used: MonotoneOn.map_sInf_of_continuousWithinAt, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousAt f (sInf s)
Af : Antitone f
ftop : f ⊤ = ⊥
⊢ f (sInf s) = sSup (f '' s)

Tactic:
Monotone.map_sInf_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (sInf s) from Cf) Af
    ftop

Premises used: OrderDual, Monotone.map_sInf_of_continuousAt
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : CompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderClosedTopology β
ι : Sort u_3
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Af : Antitone f
ftop : f ⊤ = ⊥
⊢ f (iInf g) = iSup (f ∘ g)

Tactic:
Monotone.map_iInf_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (iInf g) from Cf) Af
    ftop

Premises used: iSup, Monotone.map_iInf_of_continuousAt, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : s.Nonempty
B : BddAbove s
⊢ sSup s ∈ closure[inst_1] s

Tactic:
(isLUB_csSup hs B).mem_closure hs

Premises used: Set.Mem, IsLUB.mem_closure, isLUB_csSup
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : s.Nonempty
B : BddBelow s
⊢ sInf s ∈ closure[inst_1] s

Tactic:
(isGLB_csInf hs B).mem_closure hs

Premises used: Set.Mem, IsGLB.mem_closure, isGLB_csInf
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hc : IsClosed[inst_1] s
hs : s.Nonempty
B : BddAbove s
⊢ sSup s ∈ s

Tactic:
(isLUB_csSup hs B).mem_of_isClosed hs hc

Premises used: Set.Mem, isLUB_csSup, IsLUB.mem_of_isClosed
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hc : IsClosed[inst_1] s
hs : s.Nonempty
B : BddBelow s
⊢ sInf s ∈ s

Tactic:
(isGLB_csInf hs B).mem_of_isClosed hs hc

Premises used: IsGLB.mem_of_isClosed, Set.Mem, isGLB_csInf
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hc : IsClosed[inst_1] s
hs : s.Nonempty
B : BddBelow s
⊢ IsLeast s (sInf s)

Tactic:
⟨hc.csInf_mem hs B, (isGLB_csInf hs B).1⟩

Premises used: IsLeast, isGLB_csInf, And.left, And.intro, IsClosed.csInf_mem
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hc : IsClosed[inst_1] s
hs : s.Nonempty
B : BddAbove s
⊢ IsGreatest s (sSup s)

Tactic:
IsClosed.isLeast_csInf (α := αᵒᵈ) hc hs B

Premises used: Set.Mem, setOf, upperBounds, IsGreatest, OrderDual, IsClosed.isLeast_csInf
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Ioo y x)))

Tactic:
tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
refine_1 : ∀ (l : β) (hl : l < sSup (f '' Ioo y x)), ∀ᶠ (b : α) in 𝓝[<] x, l < f b
refine_2 : ∀ (m : β) (hm : m > sSup (f '' Ioo y x)), ∀ᶠ (b : α) in 𝓝[<] x, f b < m
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Ioo y x)))

Tactic:
refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
l : β
hl : l < sSup (f '' Ioo y x)
⊢ ∃ a ∈ Ioo y x, l < f a

Tactic:
simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_lt_csSup (h_nonempty.image _) hl

Premises used: Set.mem_image, exists_prop, exists_lt_of_lt_csSup, exists_exists_and_eq_and, Set.Nonempty.image
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
l : β
hl : l < sSup (f '' Ioo y x)
refine_1 : ∀ (z : α) (lz : l < f z) (yz : y < z) (zx : z < x), ∀ᶠ (b : α) in 𝓝[<] x, l < f b
⊢ ∀ᶠ (b : α) in 𝓝[<] x, l < f b

Tactic:
obtain ⟨z, ⟨yz, zx⟩, lz⟩ : ∃ a : α, a ∈ Ioo y x ∧ l < f a := by
      simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_lt_csSup (h_nonempty.image _) hl

Premises used: Set.Ioo
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
l : β
hl : l < sSup (f '' Ioo y x)
z : α
lz : l < f z
yz : y < z
zx : z < x
h : ∀ (w : α) (hw : w ∈ Ioo z x), l < f w
⊢ ∀ᶠ (b : α) in 𝓝[<] x, l < f b

Tactic:
filter_upwards [Ioo_mem_nhdsLT zx] with w hw

Premises used: Ioo_mem_nhdsLT
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
l : β
hl : l < sSup (f '' Ioo y x)
z : α
lz : l < f z
yz : y < z
zx : z < x
w : α
hw : w ∈ Ioo z x
⊢ l < f w

Tactic:
lz.trans_le <| Mf ⟨yz, zx⟩ ⟨yz.trans_le hw.1.le, hw.2⟩ hw.1.le

Premises used: LT.lt.le, And.right, And.left, LT.lt.trans_le, And.intro
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
l : β
hl : l < sSup (f '' Ioo y x)
z : α
lz : l < f z
yz : y < z
zx : z < x
w : α
hw : w ∈ Ioo z x
⊢ l < f w

Tactic:
exact lz.trans_le <| Mf ⟨yz, zx⟩ ⟨yz.trans_le hw.1.le, hw.2⟩ hw.1.le

Premises used: LT.lt.le, And.right, And.left, LT.lt.trans_le, And.intro
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
m : β
hm : m > sSup (f '' Ioo y x)
refine_2 : ∀ (w : α) (hy : y < w) (hx : w < x), ∀ᶠ (b : α) in 𝓝[<] x, f b < m
⊢ ∀ᶠ (b : α) in 𝓝[<] x, f b < m

Tactic:
rcases h_nonempty with ⟨_, hy, hx⟩
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
m : β
hm : m > sSup (f '' Ioo y x)
w : α
hy : y < w
hx : w < x
h : ∀ (w : α) (hw : w ∈ Ioo y x), f w < m
⊢ ∀ᶠ (b : α) in 𝓝[<] x, f b < m

Tactic:
filter_upwards [Ioo_mem_nhdsLT (hy.trans hx)] with w hw

Premises used: Ioo_mem_nhdsLT, LT.lt.trans
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
m : β
hm : m > sSup (f '' Ioo y x)
w_1 : α
hy : y < w_1
hx : w_1 < x
w : α
hw : w ∈ Ioo y x
⊢ f w < m

Tactic:
(le_csSup h_bdd (mem_image_of_mem _ hw)).trans_lt hm

Premises used: Set.mem_image_of_mem, le_csSup, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
Mf : MonotoneOn f (Ioo y x)
h_bdd : BddAbove (f '' Ioo y x)
m : β
hm : m > sSup (f '' Ioo y x)
w_1 : α
hy : y < w_1
hx : w_1 < x
w : α
hw : w ∈ Ioo y x
⊢ f w < m

Tactic:
exact (le_csSup h_bdd (mem_image_of_mem _ hw)).trans_lt hm

Premises used: Set.mem_image_of_mem, le_csSup, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
⊢ Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioo x y)))

Tactic:
tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
refine_1 : ∀ (l : β) (hl : l < sInf (f '' Ioo x y)), ∀ᶠ (b : α) in 𝓝[>] x, l < f b
refine_2 : ∀ (m : β) (hm : m > sInf (f '' Ioo x y)), ∀ᶠ (b : α) in 𝓝[>] x, f b < m
⊢ Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioo x y)))

Tactic:
refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
l : β
hl : l < sInf (f '' Ioo x y)
refine_1 : ∀ (p : α) (hy : x < p) (hx : p < y), ∀ᶠ (b : α) in 𝓝[>] x, l < f b
⊢ ∀ᶠ (b : α) in 𝓝[>] x, l < f b

Tactic:
rcases h_nonempty with ⟨p, hy, hx⟩
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
l : β
hl : l < sInf (f '' Ioo x y)
p : α
hy : x < p
hx : p < y
h : ∀ (w : α) (hw : w ∈ Ioo x y), l < f w
⊢ ∀ᶠ (b : α) in 𝓝[>] x, l < f b

Tactic:
filter_upwards [Ioo_mem_nhdsGT (hy.trans hx)] with w hw

Premises used: LT.lt.trans, Ioo_mem_nhdsGT
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
l : β
hl : l < sInf (f '' Ioo x y)
p : α
hy : x < p
hx : p < y
w : α
hw : w ∈ Ioo x y
⊢ l < f w

Tactic:
hl.trans_le <| csInf_le h_bdd (mem_image_of_mem _ hw)

Premises used: Set.mem_image_of_mem, LT.lt.trans_le, csInf_le
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
l : β
hl : l < sInf (f '' Ioo x y)
p : α
hy : x < p
hx : p < y
w : α
hw : w ∈ Ioo x y
⊢ l < f w

Tactic:
exact hl.trans_le <| csInf_le h_bdd (mem_image_of_mem _ hw)

Premises used: Set.mem_image_of_mem, LT.lt.trans_le, csInf_le
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
m : β
hm : m > sInf (f '' Ioo x y)
⊢ ∃ a ∈ Ioo x y, f a < m

Tactic:
simpa [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_csInf_lt (h_nonempty.image _) hm

Premises used: Set.mem_image, exists_prop, exists_exists_and_eq_and, Set.Nonempty.image, exists_lt_of_csInf_lt
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
m : β
hm : m > sInf (f '' Ioo x y)
refine_2 : ∀ (z : α) (zm : f z < m) (xz : x < z) (zy : z < y), ∀ᶠ (b : α) in 𝓝[>] x, f b < m
⊢ ∀ᶠ (b : α) in 𝓝[>] x, f b < m

Tactic:
obtain ⟨z, ⟨xz, zy⟩, zm⟩ : ∃ a : α, a ∈ Ioo x y ∧ f a < m := by
      simpa [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_csInf_lt (h_nonempty.image _) hm

Premises used: Set.Ioo
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
m : β
hm : m > sInf (f '' Ioo x y)
z : α
zm : f z < m
xz : x < z
zy : z < y
h : ∀ (w : α) (hw : w ∈ Ioo x z), f w < m
⊢ ∀ᶠ (b : α) in 𝓝[>] x, f b < m

Tactic:
filter_upwards [Ioo_mem_nhdsGT xz] with w hw

Premises used: Ioo_mem_nhdsGT
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
m : β
hm : m > sInf (f '' Ioo x y)
z : α
zm : f z < m
xz : x < z
zy : z < y
w : α
hw : w ∈ Ioo x z
⊢ f w < m

Tactic:
(Mf ⟨hw.1, hw.2.trans zy⟩ ⟨xz, zy⟩ hw.2.le).trans_lt zm

Premises used: LT.lt.le, And.right, And.left, And.intro, LT.lt.trans, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
m : β
hm : m > sInf (f '' Ioo x y)
z : α
zm : f z < m
xz : x < z
zy : z < y
w : α
hw : w ∈ Ioo x z
⊢ f w < m

Tactic:
exact (Mf ⟨hw.1, hw.2.trans zy⟩ ⟨xz, zy⟩ hw.2.le).trans_lt zm

Premises used: LT.lt.le, And.right, And.left, And.intro, LT.lt.trans, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
inl : ∀ (h : Iio x = ∅), Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))
inr : ∀ (h : (Iio x).Nonempty), Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))

Tactic:
rcases eq_empty_or_nonempty (Iio x) with (h | h)

Premises used: Set.eq_empty_or_nonempty, Set.Iio
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : Iio x = ∅
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))

Tactic:
simp [h]
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))

Tactic:
tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
inr : ∀ (l : β) (hl : l < sSup (f '' Iio x)), ∀ᶠ (b : α) in 𝓝[<] x, l < f b
inr₁ : ∀ (m : β) (hm : m > sSup (f '' Iio x)), ∀ᶠ (b : α) in 𝓝[<] x, f b < m
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))

Tactic:
refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro