-- Mathlib/Topology/Order/Monotone.lean
lemma MonotoneOn.tendsto_nhdsWithin_Ioo_left {α β : Type*} [LinearOrder α] [TopologicalSpace α]
    [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [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)))

Proof state:
case refine_2.intro.intro
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : 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
⊢ ∀ᶠ (b : α) in 𝓝[<] x, f b < m

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

Result:
case h
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : 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
w : α
hw : w ∈ Ioo y x
⊢ f w < m

Proof state:
case refine_2
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : 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)
⊢ ∀ᶠ (b : α) in 𝓝[<] x, f b < m

Tactic:
rcases h_nonempty with ⟨_, hy, hx⟩

Result:
case refine_2.intro.intro
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : 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
⊢ ∀ᶠ (b : α) in 𝓝[<] x, f b < m

Proof state:
case refine_1.intro.intro.intro
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : 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
⊢ ∀ᶠ (b : α) in 𝓝[<] x, l < f b

Tactic:
filter_upwards [Ioo_mem_nhdsLT zx] with w hw

Result:
case h
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : 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

Proof state:
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : 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:
refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩

Result:
case refine_1
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : 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)
⊢ ∀ᶠ (b : α) in 𝓝[<] x, l < f b

case refine_2
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : 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)
⊢ ∀ᶠ (b : α) in 𝓝[<] x, f b < m

Proof state:
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : 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

Result:
no goals

Proof state:
case refine_1
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : 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)
⊢ ∀ᶠ (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

Result:
case refine_1.intro.intro.intro
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : 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
⊢ ∀ᶠ (b : α) in 𝓝[<] x, l < f b

Proof state:
case h
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : 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

Result:
no goals

Proof state:
case h
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : 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
w : α
hw : w ∈ Ioo y x
⊢ f w < m

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

Result:
no goals