α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this : TopologicalSpace α := Preorder.topology α
⊢ rightLim f x ≤ leftLim f y
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
⊢ rightLim f x ≤ leftLim f y
letI : TopologicalSpace α := Preorder.topology α
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ rightLim f x ≤ leftLim f y
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this : TopologicalSpace α := Preorder.topology α
⊢ rightLim f x ≤ leftLim f y
haveI : OrderTopology α := ⟨rfl⟩
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y = ⊥
⊢ rightLim f x ≤ leftLim f y

case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y ≠ ⊥
⊢ rightLim f x ≤ leftLim f y
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ rightLim f x ≤ leftLim f y
rcases eq_or_ne (𝓝[<] y) ⊥ with (h' | h')
case inr.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y ≠ ⊥
a : α
xa : x < a
ay : a < y
⊢ rightLim f x ≤ leftLim f y
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y ≠ ⊥
⊢ rightLim f x ≤ leftLim f y
obtain ⟨a, ⟨xa, ay⟩⟩ : (Ioo x y).Nonempty :=
  forall_mem_nonempty_iff_neBot.2 (neBot_iff.2 h') (Ioo x y)
    (Ioo_mem_nhdsWithin_Iio ⟨h, le_refl _⟩)
no goals
case inr.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y ≠ ⊥
a : α
xa : x < a
ay : a < y
⊢ rightLim f x ≤ leftLim f y
calc
  rightLim f x ≤ f a := hf.rightLim_le xa
  _ ≤ leftLim f y := hf.le_leftLim ay
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y = ⊥
⊢ rightLim f x ≤ f y
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y = ⊥
⊢ rightLim f x ≤ leftLim f y
simp [leftLim, h']
no goals
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y = ⊥
⊢ rightLim f x ≤ f y
exact rightLim_le hf h