α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.33769
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
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'
α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.33769
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y z : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
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
intro y hy
case pos
α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.33769
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
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_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.33769
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
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'
α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.33769
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
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'
by_cases h : ∃ l, l < f x
case pos.intro.intro
α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.33769
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
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'
case pos
α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.33769
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
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'
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
case h
α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.33769
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
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
case pos.intro.intro
α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.33769
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
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'
filter_upwards [hf z zlt]with a ha
no goals
case h
α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.33769
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
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
calc
  y < g (min (f x) (f a)) := hz (by simp [zlt, ha, le_refl])
  _ ≤ g (f a) := gmon (min_le_right _ _)
no goals
α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.33769
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z✝ : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
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
⊢ min (f x) (f a) ∈ Ioc z (f x)
simp [zlt, ha, le_refl]
case neg
α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.33769
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
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'
case neg
α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.33769
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
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'
simp only [not_exists, not_lt] at h
no goals
case neg
α : Type u_3
inst✝⁷ : TopologicalSpace α
β : Type ?u.33769
inst✝⁶ : Preorder β
f✝ g✝ : α → β
x : α
s t : Set α
y✝ z : β
γ : Type u_1
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_2
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'
exact Filter.eventually_of_forall fun a => hy.trans_le (gmon (h (f a)))