-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuousWithinAt_sum {f : ι → α → γ} {a : Finset ι}
    (ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) s x) :
    LowerSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) s x

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
x : α
s : Set α
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) s x

Tactic:
classical
  induction a using Finset.induction_on with
  | empty => exact lowerSemicontinuousWithinAt_const
  | insert ia IH =>
    simp only [ia, Finset.sum_insert, not_false_iff]
    exact
      LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self ..))
        (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))

Result:
no goals

Proof state:
case insert
α : Type u_1
inst✝⁴ : TopologicalSpace α
x : α
s : Set α
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a✝ : ι
s✝ : Finset ι
ia : a✝ ∉ s✝
IH : (∀ i ∈ s✝, LowerSemicontinuousWithinAt (f i) s x) → LowerSemicontinuousWithinAt (fun z => ∑ i ∈ s✝, f i z) s x
ha : ∀ i ∈ insert a✝ s✝, LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun z => f a✝ z + ∑ i ∈ s✝, f i z) s x

Tactic:
exact
  LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self ..))
    (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
x : α
s : Set α
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ i ∈ a, LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) s x

Tactic:
induction a using Finset.induction_on with
| empty => exact lowerSemicontinuousWithinAt_const
| insert ia IH =>
  simp only [ia, Finset.sum_insert, not_false_iff]
  exact
    LowerSemicontinuousWithinAt.add (ha _ (Finset.mem_insert_self ..))
      (IH fun j ja => ha j (Finset.mem_insert_of_mem ja))

Result:
no goals

Proof state:
case empty
α : Type u_1
inst✝⁴ : TopologicalSpace α
x : α
s : Set α
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
ha : ∀ i ∈ ∅, LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i ∈ ∅, f i z) s x

Tactic:
exact lowerSemicontinuousWithinAt_const

Result:
no goals

Proof state:
case insert
α : Type u_1
inst✝⁴ : TopologicalSpace α
x : α
s : Set α
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a✝ : ι
s✝ : Finset ι
ia : a✝ ∉ s✝
IH : (∀ i ∈ s✝, LowerSemicontinuousWithinAt (f i) s x) → LowerSemicontinuousWithinAt (fun z => ∑ i ∈ s✝, f i z) s x
ha : ∀ i ∈ insert a✝ s✝, LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i ∈ insert a✝ s✝, f i z) s x

Tactic:
simp only [ia, Finset.sum_insert, not_false_iff]

Result:
case insert
α : Type u_1
inst✝⁴ : TopologicalSpace α
x : α
s : Set α
ι : Type u_3
γ : Type u_4
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a✝ : ι
s✝ : Finset ι
ia : a✝ ∉ s✝
IH : (∀ i ∈ s✝, LowerSemicontinuousWithinAt (f i) s x) → LowerSemicontinuousWithinAt (fun z => ∑ i ∈ s✝, f i z) s x
ha : ∀ i ∈ insert a✝ s✝, LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun z => f a✝ z + ∑ i ∈ s✝, f i z) s x