-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem finset_sum {ι} (s : Finset ι) {f : ι → ∀ i, E i} (hf : ∀ i ∈ s, Memℓp (f i) p) :
    Memℓp (fun a => ∑ i ∈ s, f i a) p

Proof state:
case refine_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ (∀ i ∈ ∅, Memℓp (f i) p) → Memℓp (fun a => ∑ i ∈ ∅, f i a) p

Tactic:
simp only [zero_mem_ℓp', Finset.sum_empty, imp_true_iff]

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ (∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a => ∑ i ∈ s, f i a) p

Tactic:
refine Finset.induction_on s ?_ ?_

Result:
case refine_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ (∀ i ∈ ∅, Memℓp (f i) p) → Memℓp (fun a => ∑ i ∈ ∅, f i a) p

case refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a => ∑ i ∈ s, f i a) p) →
        (∀ i ∈ insert a s, Memℓp (f i) p) → Memℓp (fun a_3 => ∑ i ∈ insert a s, f i a_3) p

Proof state:
case refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a => ∑ i ∈ s, f i a) p) →
        (∀ i ∈ insert a s, Memℓp (f i) p) → Memℓp (fun a_3 => ∑ i ∈ insert a s, f i a_3) p

Tactic:
intro i s his ih hf

Result:
case refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s✝ : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a => ∑ i ∈ s, f i a) p
hf : ∀ i_1 ∈ insert i s, Memℓp (f i_1) p
⊢ Memℓp (fun a => ∑ i ∈ insert i s, f i a) p

Proof state:
case refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s✝ : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a => ∑ i ∈ s, f i a) p
hf : ∀ i_1 ∈ insert i s, Memℓp (f i_1) p
⊢ Memℓp (fun a => f i a + ∑ i ∈ s, f i a) p

Tactic:
exact (hf i (s.mem_insert_self i)).add (ih fun j hj => hf j (Finset.mem_insert_of_mem hj))

Result:
no goals

Proof state:
case refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s✝ : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a => ∑ i ∈ s, f i a) p
hf : ∀ i_1 ∈ insert i s, Memℓp (f i_1) p
⊢ Memℓp (fun a => ∑ i ∈ insert i s, f i a) p

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

Result:
case refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s✝ : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a => ∑ i ∈ s, f i a) p
hf : ∀ i_1 ∈ insert i s, Memℓp (f i_1) p
⊢ Memℓp (fun a => f i a + ∑ i ∈ s, f i a) p

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
hf : ∀ i ∈ s, Memℓp (f i) p
this : DecidableEq ι
⊢ Memℓp (fun a => ∑ i ∈ s, f i a) p

Tactic:
revert hf

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ (∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a => ∑ i ∈ s, f i a) p

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
hf : ∀ i ∈ s, Memℓp (f i) p
⊢ Memℓp (fun a => ∑ i ∈ s, f i a) p

Tactic:
haveI : DecidableEq ι := Classical.decEq _

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
hf : ∀ i ∈ s, Memℓp (f i) p
this : DecidableEq ι
⊢ Memℓp (fun a => ∑ i ∈ s, f i a) p