[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
f : α → β
a : α
⊢ β
[PROOFSTEP]
classical
haveI : Nonempty β := ⟨f a⟩
letI : TopologicalSpace α := Preorder.topology α
exact if 𝓝[<] a = ⊥ ∨ ¬∃ y, Tendsto f (𝓝[<] a) (𝓝 y) then f a else limUnder (𝓝[<] a) f
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
f : α → β
a : α
⊢ β
[PROOFSTEP]
haveI : Nonempty β := ⟨f a⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
f : α → β
a : α
this : Nonempty β
⊢ β
[PROOFSTEP]
letI : TopologicalSpace α := Preorder.topology α
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
f : α → β
a : α
this✝ : Nonempty β
this : TopologicalSpace α := Preorder.topology α
⊢ β
[PROOFSTEP]
exact if 𝓝[<] a = ⊥ ∨ ¬∃ y, Tendsto f (𝓝[<] a) (𝓝 y) then f a else limUnder (𝓝[<] a) f
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
⊢ leftLim f a = y
[PROOFSTEP]
have h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y) := ⟨y, h'⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
⊢ leftLim f a = y
[PROOFSTEP]
rw [h'α.topology_eq_generate_intervals] at h h' h'' 
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
⊢ leftLim f a = y
[PROOFSTEP]
simp only [leftLim, h, h'', not_true, or_self_iff, if_false]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
⊢ limUnder (𝓝[Iio a] a) f = y
[PROOFSTEP]
haveI := neBot_iff.2 h
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
this : NeBot (𝓝[Iio a] a)
⊢ limUnder (𝓝[Iio a] a) f = y
[PROOFSTEP]
exact lim_eq h'
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : 𝓝[Iio a] a = ⊥
⊢ leftLim f a = f a
[PROOFSTEP]
rw [h'α.topology_eq_generate_intervals] at h 
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : 𝓝[Iio a] a = ⊥
⊢ leftLim f a = f a
[PROOFSTEP]
simp [leftLim, ite_eq_left_iff, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
⊢ leftLim f x ≤ f y
[PROOFSTEP]
letI : TopologicalSpace α := Preorder.topology α
[GOAL]
α : 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 α
⊢ leftLim f x ≤ f y
[PROOFSTEP]
haveI : OrderTopology α := ⟨rfl⟩
[GOAL]
α : 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 α
⊢ leftLim f x ≤ f y
[PROOFSTEP]
rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')
[GOAL]
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 x] x = ⊥
⊢ leftLim f x ≤ f y
[PROOFSTEP]
simpa [leftLim, h'] using hf h
[GOAL]
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 x] x ≠ ⊥
⊢ leftLim f x ≤ f y
[PROOFSTEP]
haveI A : NeBot (𝓝[<] x) := neBot_iff.2 h'
[GOAL]
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 x] x ≠ ⊥
A : NeBot (𝓝[Iio x] x)
⊢ leftLim f x ≤ f y
[PROOFSTEP]
rw [leftLim_eq_sSup hf h']
[GOAL]
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 x] x ≠ ⊥
A : NeBot (𝓝[Iio x] x)
⊢ sSup (f '' Iio x) ≤ f y
[PROOFSTEP]
refine' csSup_le _ _
[GOAL]
case inr.refine'_1
α : 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 x] x ≠ ⊥
A : NeBot (𝓝[Iio x] x)
⊢ Set.Nonempty (f '' Iio x)
[PROOFSTEP]
simp only [nonempty_image_iff]
[GOAL]
case inr.refine'_1
α : 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 x] x ≠ ⊥
A : NeBot (𝓝[Iio x] x)
⊢ Set.Nonempty (Iio x)
[PROOFSTEP]
exact (forall_mem_nonempty_iff_neBot.2 A) _ self_mem_nhdsWithin
[GOAL]
case inr.refine'_2
α : 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 x] x ≠ ⊥
A : NeBot (𝓝[Iio x] x)
⊢ ∀ (b : β), b ∈ f '' Iio x → b ≤ f y
[PROOFSTEP]
simp only [mem_image, mem_Iio, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
[GOAL]
case inr.refine'_2
α : 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 x] x ≠ ⊥
A : NeBot (𝓝[Iio x] x)
⊢ ∀ (a : α), a < x → f a ≤ f y
[PROOFSTEP]
intro z hz
[GOAL]
case inr.refine'_2
α : 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 x] x ≠ ⊥
A : NeBot (𝓝[Iio x] x)
z : α
hz : z < x
⊢ f z ≤ f y
[PROOFSTEP]
exact hf (hz.le.trans h)
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
⊢ f x ≤ leftLim f y
[PROOFSTEP]
letI : TopologicalSpace α := Preorder.topology α
[GOAL]
α : 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 α
⊢ f x ≤ leftLim f y
[PROOFSTEP]
haveI : OrderTopology α := ⟨rfl⟩
[GOAL]
α : 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 α
⊢ f x ≤ leftLim f y
[PROOFSTEP]
rcases eq_or_ne (𝓝[<] y) ⊥ with (h' | h')
[GOAL]
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 = ⊥
⊢ f x ≤ leftLim f y
[PROOFSTEP]
rw [leftLim_eq_of_eq_bot _ h']
[GOAL]
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 = ⊥
⊢ f x ≤ f y
[PROOFSTEP]
exact hf h.le
[GOAL]
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 ≠ ⊥
⊢ f x ≤ leftLim f y
[PROOFSTEP]
rw [leftLim_eq_sSup hf h']
[GOAL]
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 ≠ ⊥
⊢ f x ≤ sSup (f '' Iio y)
[PROOFSTEP]
refine' le_csSup ⟨f y, _⟩ (mem_image_of_mem _ h)
[GOAL]
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 ≠ ⊥
⊢ f y ∈ upperBounds (f '' Iio y)
[PROOFSTEP]
simp only [upperBounds, mem_image, mem_Iio, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq]
[GOAL]
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 ≠ ⊥
⊢ ∀ (a : α), a < y → f a ≤ f y
[PROOFSTEP]
intro z hz
[GOAL]
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 ≠ ⊥
z : α
hz : z < y
⊢ f z ≤ f y
[PROOFSTEP]
exact hf hz.le
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
⊢ Monotone (leftLim f)
[PROOFSTEP]
intro x y h
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y✝ x y : α
h : x ≤ y
⊢ leftLim f x ≤ leftLim f y
[PROOFSTEP]
rcases eq_or_lt_of_le h with (rfl | hxy)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y x : α
h : x ≤ x
⊢ leftLim f x ≤ leftLim f x
[PROOFSTEP]
exact le_rfl
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y✝ x y : α
h : x ≤ y
hxy : x < y
⊢ leftLim f x ≤ leftLim f y
[PROOFSTEP]
exact (hf.leftLim_le le_rfl).trans (hf.le_leftLim hxy)
[GOAL]
α : 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
[PROOFSTEP]
letI : TopologicalSpace α := Preorder.topology α
[GOAL]
α : 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
[PROOFSTEP]
haveI : OrderTopology α := ⟨rfl⟩
[GOAL]
α : 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
[PROOFSTEP]
rcases eq_or_ne (𝓝[<] y) ⊥ with (h' | h')
[GOAL]
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
[PROOFSTEP]
simp [leftLim, h']
[GOAL]
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
[PROOFSTEP]
exact rightLim_le hf h
[GOAL]
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
[PROOFSTEP]
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 _⟩)
[GOAL]
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
[PROOFSTEP]
calc
  rightLim f x ≤ f a := hf.rightLim_le xa
  _ ≤ leftLim f y := hf.le_leftLim ay
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
⊢ Tendsto f (𝓝[Iio x] x) (𝓝 (leftLim f x))
[PROOFSTEP]
rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[Iio x] x = ⊥
⊢ Tendsto f (𝓝[Iio x] x) (𝓝 (leftLim f x))
[PROOFSTEP]
simp [h']
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[Iio x] x ≠ ⊥
⊢ Tendsto f (𝓝[Iio x] x) (𝓝 (leftLim f x))
[PROOFSTEP]
rw [leftLim_eq_sSup hf h']
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[Iio x] x ≠ ⊥
⊢ Tendsto f (𝓝[Iio x] x) (𝓝 (sSup (f '' Iio x)))
[PROOFSTEP]
exact hf.tendsto_nhdsWithin_Iio x
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
⊢ Tendsto f (𝓝[Iio x] x) (𝓝[Iic (leftLim f x)] leftLim f x)
[PROOFSTEP]
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within f (hf.tendsto_leftLim x)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
⊢ ∀ᶠ (x_1 : α) in 𝓝[Iio x] x, f x_1 ∈ Iic (leftLim f x)
[PROOFSTEP]
filter_upwards [@self_mem_nhdsWithin _ _ x (Iio x)] with y hy using hf.le_leftLim hy
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
[PROOFSTEP]
rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')
[GOAL]
case inl
α : 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' : 𝓝[Iio x] x = ⊥
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
[PROOFSTEP]
simp [leftLim_eq_of_eq_bot f h', ContinuousWithinAt, h']
[GOAL]
case inr
α : 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' : 𝓝[Iio x] x ≠ ⊥
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
[PROOFSTEP]
haveI : (𝓝[Iio x] x).NeBot := neBot_iff.2 h'
[GOAL]
case inr
α : 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' : 𝓝[Iio x] x ≠ ⊥
this : NeBot (𝓝[Iio x] x)
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
[PROOFSTEP]
refine' ⟨fun h => tendsto_nhds_unique (hf.tendsto_leftLim x) h.tendsto, fun h => _⟩
[GOAL]
case inr
α : 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' : 𝓝[Iio x] x ≠ ⊥
this : NeBot (𝓝[Iio x] x)
h : leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x
[PROOFSTEP]
have := hf.tendsto_leftLim x
[GOAL]
case inr
α : 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' : 𝓝[Iio x] x ≠ ⊥
this✝ : NeBot (𝓝[Iio x] x)
h : leftLim f x = f x
this : Tendsto f (𝓝[Iio x] x) (𝓝 (leftLim f x))
⊢ ContinuousWithinAt f (Iio x) x
[PROOFSTEP]
rwa [h] at this 
[GOAL]
α : 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
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
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
[PROOFSTEP]
have A : leftLim f x = f x := hf.continuousWithinAt_Iio_iff_leftLim_eq.1 h.continuousWithinAt
[GOAL]
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
[PROOFSTEP]
have B : rightLim f x = f x := hf.continuousWithinAt_Ioi_iff_rightLim_eq.1 h.continuousWithinAt
[GOAL]
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
[PROOFSTEP]
exact A.trans B.symm
[GOAL]
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
[PROOFSTEP]
have h' : leftLim f x = f x := by
  apply le_antisymm (leftLim_le hf (le_refl _))
  rw [h]
  exact le_rightLim hf (le_refl _)
[GOAL]
α : 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
[PROOFSTEP]
apply le_antisymm (leftLim_le hf (le_refl _))
[GOAL]
α : 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
[PROOFSTEP]
rw [h]
[GOAL]
α : 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
[PROOFSTEP]
exact le_rightLim hf (le_refl _)
[GOAL]
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
[PROOFSTEP]
refine' continuousAt_iff_continuous_left'_right'.2 ⟨_, _⟩
[GOAL]
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
[PROOFSTEP]
exact hf.continuousWithinAt_Iio_iff_leftLim_eq.2 h'
[GOAL]
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
[PROOFSTEP]
rw [h] at h' 
[GOAL]
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
[PROOFSTEP]
exact hf.continuousWithinAt_Ioi_iff_rightLim_eq.2 h'
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
⊢ Set.Countable {x | ¬ContinuousWithinAt f (Ioi x) x}
[PROOFSTEP]
nontriviality α
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
⊢ Set.Countable {x | ¬ContinuousWithinAt f (Ioi x) x}
[PROOFSTEP]
let s := {x | ¬ContinuousWithinAt f (Ioi x) x}
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
⊢ Set.Countable {x | ¬ContinuousWithinAt f (Ioi x) x}
[PROOFSTEP]
have : ∀ x, x ∈ s → ∃ z, f x < z ∧ ∀ y, x < y → z ≤ f y :=
  by
  rintro x (hx : ¬ContinuousWithinAt f (Ioi x) x)
  contrapose! hx
  refine' tendsto_order.2 ⟨fun m hm => _, fun u hu => _⟩
  · filter_upwards [@self_mem_nhdsWithin _ _ x (Ioi x)] with y hy using hm.trans_le (hf (le_of_lt hy))
  rcases hx u hu with ⟨v, xv, fvu⟩
  have : Ioo x v ∈ 𝓝[>] x := Ioo_mem_nhdsWithin_Ioi ⟨le_refl _, xv⟩
  filter_upwards [this] with y hy
  apply (hf hy.2.le).trans_lt fvu
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
⊢ ∀ (x : α), x ∈ s → ∃ z, f x < z ∧ ∀ (y : α), x < y → z ≤ f y
[PROOFSTEP]
rintro x (hx : ¬ContinuousWithinAt f (Ioi x) x)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
x : α
hx : ¬ContinuousWithinAt f (Ioi x) x
⊢ ∃ z, f x < z ∧ ∀ (y : α), x < y → z ≤ f y
[PROOFSTEP]
contrapose! hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
⊢ ContinuousWithinAt f (Ioi x) x
[PROOFSTEP]
refine' tendsto_order.2 ⟨fun m hm => _, fun u hu => _⟩
[GOAL]
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 α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
m : β
hm : m < f x
⊢ ∀ᶠ (b : α) in 𝓝[Ioi x] x, m < f b
[PROOFSTEP]
filter_upwards [@self_mem_nhdsWithin _ _ x (Ioi x)] with y hy using hm.trans_le (hf (le_of_lt hy))
[GOAL]
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 α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
u : β
hu : u > f x
⊢ ∀ᶠ (b : α) in 𝓝[Ioi x] x, f b < u
[PROOFSTEP]
rcases hx u hu with ⟨v, xv, fvu⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
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 𝓝[Ioi x] x, f b < u
[PROOFSTEP]
have : Ioo x v ∈ 𝓝[>] x := Ioo_mem_nhdsWithin_Ioi ⟨le_refl _, xv⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
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 ∈ 𝓝[Ioi x] x
⊢ ∀ᶠ (b : α) in 𝓝[Ioi x] x, f b < u
[PROOFSTEP]
filter_upwards [this] with y hy
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y✝ : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
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 ∈ 𝓝[Ioi x] x
y : α
hy : y ∈ Ioo x v
⊢ f y < u
[PROOFSTEP]
apply (hf hy.2.le).trans_lt fvu
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
this : ∀ (x : α), x ∈ s → ∃ z, f x < z ∧ ∀ (y : α), x < y → z ≤ f y
⊢ Set.Countable {x | ¬ContinuousWithinAt f (Ioi x) x}
[PROOFSTEP]
choose! z hz using this
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
⊢ Set.Countable {x | ¬ContinuousWithinAt f (Ioi x) x}
[PROOFSTEP]
have I : InjOn f s := by
  apply StrictMonoOn.injOn
  intro x hx y _ hxy
  calc
    f x < z x := (hz x hx).1
    _ ≤ f y := (hz x hx).2 y hxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
⊢ InjOn f s
[PROOFSTEP]
apply StrictMonoOn.injOn
[GOAL]
case H
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
⊢ StrictMonoOn f s
[PROOFSTEP]
intro x hx y _ hxy
[GOAL]
case H
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝¹ y✝ : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
x : α
hx : x ∈ s
y : α
x✝ : y ∈ s
hxy : x < y
⊢ f x < f y
[PROOFSTEP]
calc
  f x < z x := (hz x hx).1
  _ ≤ f y := (hz x hx).2 y hxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
⊢ Set.Countable {x | ¬ContinuousWithinAt f (Ioi x) x}
[PROOFSTEP]
have fs_count : (f '' s).Countable :=
  by
  have A : (f '' s).PairwiseDisjoint fun x => Ioo x (z (invFunOn f s x)) :=
    by
    rintro _ ⟨u, us, rfl⟩ _ ⟨v, vs, rfl⟩ huv
    wlog hle : u ≤ v generalizing u v
    · exact (this v vs u us huv.symm (le_of_not_le hle)).symm
    have hlt : u < v := hle.lt_of_ne (ne_of_apply_ne _ huv)
    apply disjoint_iff_forall_ne.2
    rintro a ha b hb rfl
    simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb 
    exact lt_irrefl _ ((ha.2.trans_le ((hz u us).2 v hlt)).trans hb.1)
  apply Set.PairwiseDisjoint.countable_of_Ioo A
  rintro _ ⟨y, ys, rfl⟩
  simpa only [I.leftInvOn_invFunOn ys] using (hz y ys).1
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
⊢ Set.Countable (f '' s)
[PROOFSTEP]
have A : (f '' s).PairwiseDisjoint fun x => Ioo x (z (invFunOn f s x)) :=
  by
  rintro _ ⟨u, us, rfl⟩ _ ⟨v, vs, rfl⟩ huv
  wlog hle : u ≤ v generalizing u v
  · exact (this v vs u us huv.symm (le_of_not_le hle)).symm
  have hlt : u < v := hle.lt_of_ne (ne_of_apply_ne _ huv)
  apply disjoint_iff_forall_ne.2
  rintro a ha b hb rfl
  simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb 
  exact lt_irrefl _ ((ha.2.trans_le ((hz u us).2 v hlt)).trans hb.1)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
⊢ PairwiseDisjoint (f '' s) fun x => Ioo x (z (invFunOn f s x))
[PROOFSTEP]
rintro _ ⟨u, us, rfl⟩ _ ⟨v, vs, rfl⟩ huv
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
u : α
us : u ∈ s
v : α
vs : v ∈ s
huv : f u ≠ f v
⊢ (Disjoint on fun x => Ioo x (z (invFunOn f s x))) (f u) (f v)
[PROOFSTEP]
wlog hle : u ≤ v generalizing u v
[GOAL]
case intro.intro.intro.intro.inr
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
u : α
us : u ∈ s
v : α
vs : v ∈ s
huv : f u ≠ f v
this :
  ∀ (u : α),
    u ∈ s → ∀ (v : α), v ∈ s → f u ≠ f v → u ≤ v → (Disjoint on fun x => Ioo x (z (invFunOn f s x))) (f u) (f v)
hle : ¬u ≤ v
⊢ (Disjoint on fun x => Ioo x (z (invFunOn f s x))) (f u) (f v)
[PROOFSTEP]
exact (this v vs u us huv.symm (le_of_not_le hle)).symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
u : α
us : u ∈ s
v : α
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
⊢ (Disjoint on fun x => Ioo x (z (invFunOn f s x))) (f u) (f v)
[PROOFSTEP]
have hlt : u < v := hle.lt_of_ne (ne_of_apply_ne _ huv)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
u : α
us : u ∈ s
v : α
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
⊢ (Disjoint on fun x => Ioo x (z (invFunOn f s x))) (f u) (f v)
[PROOFSTEP]
apply disjoint_iff_forall_ne.2
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
u : α
us : u ∈ s
v : α
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
⊢ ∀ ⦃a : β⦄,
    a ∈ (fun x => Ioo x (z (invFunOn f s x))) (f u) → ∀ ⦃b : β⦄, b ∈ (fun x => Ioo x (z (invFunOn f s x))) (f v) → a ≠ b
[PROOFSTEP]
rintro a ha b hb rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
u : α
us : u ∈ s
v : α
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
a : β
ha : a ∈ (fun x => Ioo x (z (invFunOn f s x))) (f u)
hb : a ∈ (fun x => Ioo x (z (invFunOn f s x))) (f v)
⊢ False
[PROOFSTEP]
simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb 
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
u : α
us : u ∈ s
v : α
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
a : β
ha : a ∈ Ioo (f u) (z u)
hb : a ∈ Ioo (f v) (z v)
⊢ False
[PROOFSTEP]
exact lt_irrefl _ ((ha.2.trans_le ((hz u us).2 v hlt)).trans hb.1)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
A : PairwiseDisjoint (f '' s) fun x => Ioo x (z (invFunOn f s x))
⊢ Set.Countable (f '' s)
[PROOFSTEP]
apply Set.PairwiseDisjoint.countable_of_Ioo A
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
A : PairwiseDisjoint (f '' s) fun x => Ioo x (z (invFunOn f s x))
⊢ ∀ (x : β), x ∈ f '' s → x < z (invFunOn f s x)
[PROOFSTEP]
rintro _ ⟨y, ys, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y✝ : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
A : PairwiseDisjoint (f '' s) fun x => Ioo x (z (invFunOn f s x))
y : α
ys : y ∈ s
⊢ f y < z (invFunOn f s (f y))
[PROOFSTEP]
simpa only [I.leftInvOn_invFunOn ys] using (hz y ys).1
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
fs_count : Set.Countable (f '' s)
⊢ Set.Countable {x | ¬ContinuousWithinAt f (Ioi x) x}
[PROOFSTEP]
exact MapsTo.countable_of_injOn (mapsTo_image f s) I fs_count
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
⊢ Set.Countable {x | ¬ContinuousAt f x}
[PROOFSTEP]
apply (hf.countable_not_continuousWithinAt_Ioi.union hf.countable_not_continuousWithinAt_Iio).mono _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
⊢ {x | ¬ContinuousAt f x} ⊆ {x | ¬ContinuousWithinAt f (Ioi x) x} ∪ {x | ¬ContinuousWithinAt f (Iio x) x}
[PROOFSTEP]
refine' compl_subset_compl.1 _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
⊢ ({x | ¬ContinuousWithinAt f (Ioi x) x} ∪ {x | ¬ContinuousWithinAt f (Iio x) x})ᶜ ⊆ {x | ¬ContinuousAt f x}ᶜ
[PROOFSTEP]
simp only [compl_union]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
⊢ {x | ¬ContinuousWithinAt f (Ioi x) x}ᶜ ∩ {x | ¬ContinuousWithinAt f (Iio x) x}ᶜ ⊆ {x | ¬ContinuousAt f x}ᶜ
[PROOFSTEP]
rintro x ⟨hx, h'x⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
x : α
hx : x ∈ {x | ¬ContinuousWithinAt f (Ioi x) x}ᶜ
h'x : x ∈ {x | ¬ContinuousWithinAt f (Iio x) x}ᶜ
⊢ x ∈ {x | ¬ContinuousAt f x}ᶜ
[PROOFSTEP]
simp only [mem_setOf_eq, Classical.not_not, mem_compl_iff] at hx h'x ⊢
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
x : α
hx : ContinuousWithinAt f (Ioi x) x
h'x : ContinuousWithinAt f (Iio x) x
⊢ ContinuousAt f x
[PROOFSTEP]
exact continuousAt_iff_continuous_left'_right'.2 ⟨h'x, hx⟩
