no goals
α : Type u_2
β : Type u_3
γ : Type u_1
δ : Type ?u.244028
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a✝ b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ (∀ (i : γ), i ∈ ∅ → HasSum (f i) (a i)) → HasSum (fun b => ∑ i in ∅, f i b) (∑ i in ∅, a i)
simp only [hasSum_zero, sum_empty, forall_true_iff]
α : Type u_2
β : Type u_3
γ : Type u_1
δ : Type ?u.244028
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a✝ b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ ∀ ⦃a_1 : γ⦄ {s : Finset γ},
    ¬a_1 ∈ s →
      ((∀ (i : γ), i ∈ s → HasSum (f i) (a i)) → HasSum (fun b => ∑ i in s, f i b) (∑ i in s, a i)) →
        HasSum (f a_1) (a a_1) →
          (∀ (a_5 : γ), a_5 ∈ s → HasSum (f a_5) (a a_5)) →
            HasSum (fun b => f a_1 b + ∑ i in s, f i b) (a a_1 + ∑ i in s, a i)
α : Type u_2
β : Type u_3
γ : Type u_1
δ : Type ?u.244028
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a✝ b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ ∀ ⦃a_1 : γ⦄ {s : Finset γ},
    ¬a_1 ∈ s →
      ((∀ (i : γ), i ∈ s → HasSum (f i) (a i)) → HasSum (fun b => ∑ i in s, f i b) (∑ i in s, a i)) →
        (∀ (i : γ), i ∈ insert a_1 s → HasSum (f i) (a i)) →
          HasSum (fun b => ∑ i in insert a_1 s, f i b) (∑ i in insert a_1 s, a i)
simp (config := { contextual := true }) only [mem_insert, forall_eq_or_imp, not_false_iff,
  sum_insert, and_imp]
no goals
α : Type u_2
β : Type u_3
γ : Type u_1
δ : Type ?u.244028
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
f✝ g : β → α
a✝ b : α
s✝ : Finset β
inst✝ : ContinuousAdd α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ ∀ ⦃a_1 : γ⦄ {s : Finset γ},
    ¬a_1 ∈ s →
      ((∀ (i : γ), i ∈ s → HasSum (f i) (a i)) → HasSum (fun b => ∑ i in s, f i b) (∑ i in s, a i)) →
        HasSum (f a_1) (a a_1) →
          (∀ (a_5 : γ), a_5 ∈ s → HasSum (f a_5) (a a_5)) →
            HasSum (fun b => f a_1 b + ∑ i in s, f i b) (a a_1 + ∑ i in s, a i)
exact fun x s _ IH hx h ↦ hx.add (IH h)