case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : ContinuousAt f x
⊢ leftLim f x = rightLim f x

case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
⊢ ContinuousAt f x
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
⊢ ContinuousAt f x ↔ leftLim f x = rightLim f x
refine' ⟨fun h => _, fun h => _⟩
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : ContinuousAt f x
A : leftLim f x = f x
⊢ leftLim f x = rightLim f x
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : ContinuousAt f x
⊢ leftLim f x = rightLim f x
have A : leftLim f x = f x :=
  hf.continuousWithinAt_Iio_iff_leftLim_eq.1 h.continuousWithinAt
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : ContinuousAt f x
A : leftLim f x = f x
B : rightLim f x = f x
⊢ leftLim f x = rightLim f x
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : ContinuousAt f x
A : leftLim f x = f x
⊢ leftLim f x = rightLim f x
have B : rightLim f x = f x :=
  hf.continuousWithinAt_Ioi_iff_rightLim_eq.1 h.continuousWithinAt
no goals
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : ContinuousAt f x
A : leftLim f x = f x
B : rightLim f x = f x
⊢ leftLim f x = rightLim f x
exact A.trans B.symm
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ ContinuousAt f x
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
⊢ ContinuousAt f x
have h' : leftLim f x = f x := by
  apply le_antisymm (leftLim_le hf (le_refl _))
  rw [h]
  exact le_rightLim hf (le_refl _)
case refine'_2.refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x

case refine'_2.refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ ContinuousWithinAt f (Ioi x) x
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ ContinuousAt f x
refine' continuousAt_iff_continuous_left'_right'.2 ⟨_, _⟩
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
⊢ f x ≤ leftLim f x
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
⊢ leftLim f x = f x
apply le_antisymm (leftLim_le hf (le_refl _))
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
⊢ f x ≤ rightLim f x
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
⊢ f x ≤ leftLim f x
rw [h]
no goals
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
⊢ f x ≤ rightLim f x
exact le_rightLim hf (le_refl _)
no goals
case refine'_2.refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x
exact hf.continuousWithinAt_Iio_iff_leftLim_eq.2 h'
case refine'_2.refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
h' : rightLim f x = f x
⊢ ContinuousWithinAt f (Ioi x) x
case refine'_2.refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ ContinuousWithinAt f (Ioi x) x
rw [h] at h'
no goals
case refine'_2.refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
h' : rightLim f x = f x
⊢ ContinuousWithinAt f (Ioi x) x
exact hf.continuousWithinAt_Ioi_iff_rightLim_eq.2 h'