refine' Set.Finite.induction_on hI _ _
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
⊢ (∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ I, f i x) s a
case refine'_1
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
⊢ (∀ i ∈ ∅, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ ∅, f i x) s a

case refine'_2
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
⊢ ∀ {a_1 : ι} {s_1 : Set ι},
    a_1 ∉ s_1 →
      Set.Finite s_1 →
        ((∀ i ∈ s_1, LowerSemicontinuousWithinAt (f i) s a) →
            LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ s_1, f i x) s a) →
          (∀ i ∈ insert a_1 s_1, LowerSemicontinuousWithinAt (f i) s a) →
            LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ insert a_1 s_1, f i x) s a