-- Mathlib/Topology/Order/LeftRightLim.lean
theorem countable_not_continuousWithinAt_Ioi [SecondCountableTopology β] :
    Set.Countable { x | ¬ContinuousWithinAt f (Ioi x) x }

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
⊢ {x | ¬ContinuousWithinAt f (Ioi x) x}.Countable

Tactic:
apply (countable_image_lt_image_Ioi f).mono

Result:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
⊢ {x | ¬ContinuousWithinAt f (Ioi x) x} ⊆ {x | ∃ z, f x < z ∧ ∀ (y : α), x < y → z ≤ f y}

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
u : β
hu : u > f x
v : α
xv : x < v
fvu : f v < u
this : Ioo x v ∈ 𝓝[>] x
y : α
hy : y ∈ Ioo x v
⊢ f y < u

Tactic:
apply (hf hy.2.le).trans_lt fvu

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
u : β
hu : u > f x
v : α
xv : x < v
fvu : f v < u
this : Ioo x v ∈ 𝓝[>] x
⊢ ∀ᶠ (b : α) in 𝓝[>] x, f b < u

Tactic:
filter_upwards [this] with y hy

Result:
case h
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
u : β
hu : u > f x
v : α
xv : x < v
fvu : f v < u
this : Ioo x v ∈ 𝓝[>] x
y : α
hy : y ∈ Ioo x v
⊢ f y < u

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ¬ContinuousWithinAt f (Ioi x) x
⊢ x ∈ {x | ∃ z, f x < z ∧ ∀ (y : α), x < y → z ≤ f y}

Tactic:
dsimp

Result:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ¬ContinuousWithinAt f (Ioi x) x
⊢ ∃ z, f x < z ∧ ∀ (y : α), x < y → z ≤ f y

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
⊢ {x | ¬ContinuousWithinAt f (Ioi x) x} ⊆ {x | ∃ z, f x < z ∧ ∀ (y : α), x < y → z ≤ f y}

Tactic:
rintro x (hx : ¬ContinuousWithinAt f (Ioi x) x)

Result:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ¬ContinuousWithinAt f (Ioi x) x
⊢ x ∈ {x | ∃ z, f x < z ∧ ∀ (y : α), x < y → z ≤ f y}

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
u : β
hu : u > f x
⊢ ∀ᶠ (b : α) in 𝓝[>] x, f b < u

Tactic:
rcases hx u hu with ⟨v, xv, fvu⟩

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
u : β
hu : u > f x
v : α
xv : x < v
fvu : f v < u
⊢ ∀ᶠ (b : α) in 𝓝[>] x, f b < u

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
m : β
hm : m < f x
⊢ ∀ᶠ (b : α) in 𝓝[>] x, m < f b

Tactic:
filter_upwards [@self_mem_nhdsWithin _ _ x (Ioi x)] with y hy using hm.trans_le
  (hf (le_of_lt hy))

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ¬ContinuousWithinAt f (Ioi x) x
⊢ ∃ z, f x < z ∧ ∀ (y : α), x < y → z ≤ f y

Tactic:
contrapose! hx

Result:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
⊢ ContinuousWithinAt f (Ioi x) x

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
⊢ ContinuousWithinAt f (Ioi x) x

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

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
m : β
hm : m < f x
⊢ ∀ᶠ (b : α) in 𝓝[>] x, m < f b

case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology β
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
u : β
hu : u > f x
⊢ ∀ᶠ (b : α) in 𝓝[>] x, f b < u