-- Mathlib/Topology/Semicontinuous.lean
theorem continuousWithinAt_iff_lower_upperSemicontinuousWithinAt {f : α → γ} :
    ContinuousWithinAt f s x ↔
      LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x

Proof state:
case pos.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
by_cases Hu : ∃ u, f x < u

Result:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x

case neg
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ¬∃ u, f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x

Proof state:
case pos.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
filter_upwards [h₁ l lfx, h₂ u fxu] with a lfa fau

Result:
case h
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : l < f a
fau : f a < u
⊢ a ∈ f ⁻¹' v

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
⊢ LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x → ContinuousWithinAt f s x

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case intro
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
⊢ ContinuousWithinAt f s x

Proof state:
case neg.hp
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∀ (x_1 : γ), x_1 ≤ f x
a : α
⊢ f a ∈ v

Tactic:
have : f a = f x := le_antisymm (Hu _) (Hl _)

Result:
case neg.hp
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∀ (x_1 : γ), x_1 ≤ f x
a : α
this : f a = f x
⊢ f a ∈ v

Proof state:
case intro
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
by_cases Hl : ∃ l, l < f x

Result:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
⊢ f ⁻¹' v ∈ 𝓝[s] x

case neg
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ¬∃ l, l < f x
⊢ f ⁻¹' v ∈ 𝓝[s] x

Proof state:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
by_cases Hu : ∃ u, f x < u

Result:
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∃ u, f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x

case neg
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ¬∃ u, f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x

Proof state:
case h.inr
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : l < f a
fau : f a < u
h : f a > f x
⊢ a ∈ f ⁻¹' v

Tactic:
exact hu ⟨le_of_lt h, fau⟩

Result:
no goals

Proof state:
case h.inl
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : l < f a
fau : f a < u
h : f a ≤ f x
⊢ a ∈ f ⁻¹' v

Tactic:
exact hl ⟨lfa, h⟩

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a < u
⊢ a ∈ f ⁻¹' v

Tactic:
apply hu

Result:
case h.a
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a < u
⊢ f a ∈ Ico (f x) u