-- Mathlib/Topology/Order/LeftRightLim.lean
theorem countable_not_continuousAt [SecondCountableTopology β] :
    Set.Countable { x | ¬ContinuousAt f 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} ∪ {x | ¬ContinuousWithinAt f (Iio x) x})ᶜ ⊆ {x | ¬ContinuousAt f x}ᶜ

Tactic:
simp only [compl_union]

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 | ¬ContinuousWithinAt f (Iio x) x}ᶜ ⊆ {x | ¬ContinuousAt f 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 | ¬ContinuousAt f x}.Countable

Tactic:
apply
  (hf.countable_not_continuousWithinAt_Ioi.union hf.countable_not_continuousWithinAt_Iio).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 | ¬ContinuousAt f x} ⊆ {x | ¬ContinuousWithinAt f (Ioi x) x} ∪ {x | ¬ContinuousWithinAt f (Iio x) x}

Proof state:
case 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 : ContinuousWithinAt f (Ioi x) x
h'x : ContinuousWithinAt f (Iio x) x
⊢ ContinuousAt f x

Tactic:
exact continuousAt_iff_continuous_left'_right'.2 ⟨h'x, hx⟩

Result:
no goals

Proof state:
case 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 : x ∈ {x | ¬ContinuousWithinAt f (Ioi x) x}ᶜ
h'x : x ∈ {x | ¬ContinuousWithinAt f (Iio x) x}ᶜ
⊢ x ∈ {x | ¬ContinuousAt f x}ᶜ

Tactic:
simp only [mem_setOf_eq, Classical.not_not, mem_compl_iff] at hx h'x ⊢

Result:
case 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 : ContinuousWithinAt f (Ioi x) x
h'x : ContinuousWithinAt f (Iio x) x
⊢ ContinuousAt f 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}ᶜ ∩ {x | ¬ContinuousWithinAt f (Iio x) x}ᶜ ⊆ {x | ¬ContinuousAt f x}ᶜ

Tactic:
rintro x ⟨hx, h'x⟩

Result:
case 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 : x ∈ {x | ¬ContinuousWithinAt f (Ioi x) x}ᶜ
h'x : x ∈ {x | ¬ContinuousWithinAt f (Iio x) x}ᶜ
⊢ x ∈ {x | ¬ContinuousAt f 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 | ¬ContinuousAt f x} ⊆ {x | ¬ContinuousWithinAt f (Ioi x) x} ∪ {x | ¬ContinuousWithinAt f (Iio x) x}

Tactic:
refine compl_subset_compl.1 ?_

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 | ¬ContinuousWithinAt f (Iio x) x})ᶜ ⊆ {x | ¬ContinuousAt f x}ᶜ