-- Mathlib/Topology/Order/LeftRightLim.lean
theorem continuousWithinAt_Iio_iff_leftLim_eq :
    ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

Tactic:
haveI : (𝓝[Iio x] x).NeBot := neBot_iff.2 h'

Result:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
this : (𝓝[<] x).NeBot
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
this : (𝓝[<] x).NeBot
h : leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x

Tactic:
have := hf.tendsto_leftLim x

Result:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
this✝ : (𝓝[<] x).NeBot
h : leftLim f x = f x
this : Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))
⊢ ContinuousWithinAt f (Iio x) x

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[<] x = ⊥
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

Tactic:
simp [leftLim_eq_of_eq_bot f h', ContinuousWithinAt, h']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

Tactic:
rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')

Result:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[<] x = ⊥
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
this✝ : (𝓝[<] x).NeBot
h : leftLim f x = f x
this : Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))
⊢ ContinuousWithinAt f (Iio x) x

Tactic:
rwa [h] at this

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
this : (𝓝[<] x).NeBot
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

Tactic:
refine ⟨fun h => tendsto_nhds_unique (hf.tendsto_leftLim x) h.tendsto, fun h => ?_⟩

Result:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
this : (𝓝[<] x).NeBot
h : leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x