-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuousWithinAt_ciSup {f : ι → α → δ'}
    (bdd : ∀ᶠ y in 𝓝[s] x, BddAbove (range fun i => f i y))
    (h : ∀ i, LowerSemicontinuousWithinAt (f i) s x) :
    LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x

Proof state:
case inl
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
s : Set α
ι : Sort u_3
δ' : Type u_5
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : IsEmpty ι
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x

Tactic:
simpa only [iSup_of_empty'] using lowerSemicontinuousWithinAt_const

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
s : Set α
ι : Sort u_3
δ' : Type u_5
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
s : Set α
ι : Sort u_3
δ' : Type u_5
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : IsEmpty ι
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x

case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
s : Set α
ι : Sort u_3
δ' : Type u_5
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x

Proof state:
case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
s : Set α
ι : Sort u_3
δ' : Type u_5
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x

Tactic:
intro y hy

Result:
case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
s : Set α
ι : Sort u_3
δ' : Type u_5
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y : δ'
hy : y < (fun x' => ⨆ i, f i x') x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun x' => ⨆ i, f i x') x'

Proof state:
case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
s : Set α
ι : Sort u_3
δ' : Type u_5
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y : δ'
hy : y < (fun x' => ⨆ i, f i x') x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun x' => ⨆ i, f i x') x'

Tactic:
rcases exists_lt_of_lt_ciSup hy with ⟨i, hi⟩

Result:
case inr.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
s : Set α
ι : Sort u_3
δ' : Type u_5
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y : δ'
hy : y < (fun x' => ⨆ i, f i x') x
i : ι
hi : y < f i x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun x' => ⨆ i, f i x') x'

Proof state:
case inr.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
s : Set α
ι : Sort u_3
δ' : Type u_5
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
h✝ : Nonempty ι
y : δ'
hy : y < (fun x' => ⨆ i, f i x') x
i : ι
hi : y < f i x
⊢ ∀ᶠ (x' : α) in 𝓝[s] x, y < (fun x' => ⨆ i, f i x') x'

Tactic:
filter_upwards [h i y hi, bdd] with y hy hy' using hy.trans_le (le_ciSup hy' i)

Result:
no goals