-- Mathlib/Topology/Semicontinuous.lean
theorem ContinuousAt.comp_lowerSemicontinuousWithinAt {g : γ → δ} {f : α → γ}
    (hg : ContinuousAt g (f x)) (hf : LowerSemicontinuousWithinAt f s x) (gmon : Monotone g) :
    LowerSemicontinuousWithinAt (g ∘ f) s x

Proof state:
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ∃ l, l < f x
z : γ
zlt : z < f x
hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y
a : α
ha : z < f a
⊢ f x ⊓ f a ∈ Ioc z (f x)

Tactic:
simp [zlt, ha, le_refl]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ∃ l, l < f x
z : γ
zlt : z < f x
hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y
a : α
ha : z < f a
⊢ y < (g ∘ f) a

Tactic:
calc
  y < g (min (f x) (f a)) := hz (by simp [zlt, ha, le_refl])
  _ ≤ g (f a) := gmon (min_le_right _ _)

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ¬∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (g ∘ f) x'

Tactic:
simp only [not_exists, not_lt] at h

Result:
case neg
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ∀ (x_1 : γ), f x ≤ x_1
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (g ∘ f) x'

Proof state:
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (g ∘ f) x'

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

Result:
case pos
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (g ∘ f) x'

case neg
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ¬∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (g ∘ f) x'

Proof state:
case pos.intro.intro
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ∃ l, l < f x
z : γ
zlt : z < f x
hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (g ∘ f) x'

Tactic:
filter_upwards [hf z zlt] with a ha

Result:
case h
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ∃ l, l < f x
z : γ
zlt : z < f x
hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y
a : α
ha : z < f a
⊢ y < (g ∘ f) a

Proof state:
case neg
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ∀ (x_1 : γ), f x ≤ x_1
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (g ∘ f) x'

Tactic:
exact Filter.Eventually.of_forall fun a => hy.trans_le (gmon (h (f a)))

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ∃ l, l < f x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (g ∘ f) x'

Tactic:
obtain ⟨z, zlt, hz⟩ : ∃ z < f x, Ioc z (f x) ⊆ g ⁻¹' Ioi y :=
  exists_Ioc_subset_of_mem_nhds (hg (Ioi_mem_nhds hy)) h

Result:
case pos.intro.intro
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
h : ∃ l, l < f x
z : γ
zlt : z < f x
hz : Ioc z (f x) ⊆ g ⁻¹' Ioi y
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (g ∘ f) x'

Proof state:
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
⊢ LowerSemicontinuousWithinAt (g ∘ f) s x

Tactic:
intro y hy

Result:
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
s : Set α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousWithinAt f s x
gmon : Monotone g
y : δ
hy : y < (g ∘ f) x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (g ∘ f) x'