-- Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
theorem memLp_finset_sum {ι} (s : Finset ι) {f : ι → α → E} (hf : ∀ i ∈ s, MemLp (f i) p μ) :
    MemLp (fun a => ∑ i ∈ s, f i a) p μ

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s : Finset ι
f : ι → α → E
this : DecidableEq ι
⊢ (∀ i ∈ s, MemLp (f i) p μ) → MemLp (fun a => ∑ i ∈ s, f i a) p μ

Tactic:
refine Finset.induction_on s ?_ ?_

Result:
case refine_1
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s : Finset ι
f : ι → α → E
this : DecidableEq ι
⊢ (∀ i ∈ ∅, MemLp (f i) p μ) → MemLp (fun a => ∑ i ∈ ∅, f i a) p μ

case refine_2
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s : Finset ι
f : ι → α → E
this : DecidableEq ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∀ i ∈ s, MemLp (f i) p μ) → MemLp (fun a => ∑ i ∈ s, f i a) p μ) →
        (∀ i ∈ insert a s, MemLp (f i) p μ) → MemLp (fun a_3 => ∑ i ∈ insert a s, f i a_3) p μ

Proof state:
case refine_2
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s✝ : Finset ι
f : ι → α → E
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, MemLp (f i) p μ) → MemLp (fun a => ∑ i ∈ s, f i a) p μ
hf : ∀ i_1 ∈ insert i s, MemLp (f i_1) p μ
⊢ MemLp (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_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s✝ : Finset ι
f : ι → α → E
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, MemLp (f i) p μ) → MemLp (fun a => ∑ i ∈ s, f i a) p μ
hf : ∀ i_1 ∈ insert i s, MemLp (f i_1) p μ
⊢ MemLp (fun a => f i a + ∑ i ∈ s, f i a) p μ

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
⊢ MemLp (fun a => ∑ i ∈ s, f i a) p μ

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

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
this : DecidableEq ι
⊢ MemLp (fun a => ∑ i ∈ s, f i a) p μ

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, MemLp (f i) p μ
this : DecidableEq ι
⊢ MemLp (fun a => ∑ i ∈ s, f i a) p μ

Tactic:
revert hf

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s : Finset ι
f : ι → α → E
this : DecidableEq ι
⊢ (∀ i ∈ s, MemLp (f i) p μ) → MemLp (fun a => ∑ i ∈ s, f i a) p μ

Proof state:
case refine_2
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s✝ : Finset ι
f : ι → α → E
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, MemLp (f i) p μ) → MemLp (fun a => ∑ i ∈ s, f i a) p μ
hf : ∀ i_1 ∈ insert i s, MemLp (f i_1) p μ
⊢ MemLp (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_1
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s : Finset ι
f : ι → α → E
this : DecidableEq ι
⊢ (∀ i ∈ ∅, MemLp (f i) p μ) → MemLp (fun a => ∑ i ∈ ∅, f i a) p μ

Tactic:
simp only [MemLp.zero', Finset.sum_empty, imp_true_iff]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s : Finset ι
f : ι → α → E
this : DecidableEq ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    a ∉ s →
      ((∀ i ∈ s, MemLp (f i) p μ) → MemLp (fun a => ∑ i ∈ s, f i a) p μ) →
        (∀ i ∈ insert a s, MemLp (f i) p μ) → MemLp (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_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
ι : Type u_3
s✝ : Finset ι
f : ι → α → E
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, MemLp (f i) p μ) → MemLp (fun a => ∑ i ∈ s, f i a) p μ
hf : ∀ i_1 ∈ insert i s, MemLp (f i_1) p μ
⊢ MemLp (fun a => ∑ i ∈ insert i s, f i a) p μ