-- 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
α : 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

Tactic:
rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩

Result:
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

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 : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
filter_upwards [h₂ u fxu] with a lfa

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 : ∀ (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

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 : ¬∃ l, l < f x
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
simp only [not_exists, not_lt] at Hl

Result:
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

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
⊢ ∀ (x : α), f x ∈ v

Tactic:
intro a

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 : α
⊢ f a ∈ v

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

Tactic:
refine ⟨fun h => ⟨h.lowerSemicontinuousWithinAt, h.upperSemicontinuousWithinAt⟩, ?_⟩

Result:
α : 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

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 : ∃ l, l < f x
l : γ
lfx : l < f x
hl : Ioc l (f x) ⊆ v
Hu : ¬∃ u, f x < u
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
simp only [not_exists, not_lt] at Hu

Result:
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 : ∀ (x_1 : γ), x_1 ≤ f x
⊢ f ⁻¹' v ∈ 𝓝[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 : α
this : f a = f x
⊢ f x ∈ v

Tactic:
exact mem_of_mem_nhds hv

Result:
no goals

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
⊢ ContinuousWithinAt f s x

Tactic:
intro v hv

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
v : Set γ
hv : v ∈ 𝓝 (f x)
⊢ v ∈ map f (𝓝[s] x)

Proof state:
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

Tactic:
rcases exists_Ico_subset_of_mem_nhds hv Hu with ⟨u, fxu, hu⟩

Result:
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 : ∀ (x_1 : γ), f x ≤ x_1
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
⊢ f ⁻¹' v ∈ 𝓝[s] x

Proof state:
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

Tactic:
rcases exists_Ioc_subset_of_mem_nhds hv Hl with ⟨l, lfx, hl⟩

Result:
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