-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem Lp_toLp_restrict_add (f g : Lp E p μ) (s : Set X) :
    ((Lp.memLp (f + g)).restrict s).toLp (⇑(f + g)) =
      ((Lp.memLp f).restrict s).toLp f + ((Lp.memLp g).restrict s).toLp g

Proof state:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x →
      ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x = (↑↑(MemLp.toLp ↑↑f ⋯) + ↑↑(MemLp.toLp ↑↑g ⋯)) x →
        ↑↑(f + g) x = (↑↑f + ↑↑g) x → ↑↑(MemLp.toLp ↑↑(f + g) ⋯) x = ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x

Tactic:
refine (MemLp.coeFn_toLp ((Lp.memLp g).restrict s)).mp ?_

Result:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    ↑↑(MemLp.toLp ↑↑g ⋯) x = ↑↑g x →
      ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x →
        ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x = (↑↑(MemLp.toLp ↑↑f ⋯) + ↑↑(MemLp.toLp ↑↑g ⋯)) x →
          ↑↑(f + g) x = (↑↑f + ↑↑g) x → ↑↑(MemLp.toLp ↑↑(f + g) ⋯) x = ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x

Proof state:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    ↑↑(MemLp.toLp ↑↑g ⋯) x = ↑↑g x →
      ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x →
        ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x = (↑↑(MemLp.toLp ↑↑f ⋯) + ↑↑(MemLp.toLp ↑↑g ⋯)) x →
          ↑↑(f + g) x = (↑↑f + ↑↑g) x → ↑↑(MemLp.toLp ↑↑(f + g) ⋯) x = ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x

Tactic:
refine (MemLp.coeFn_toLp ((Lp.memLp (f + g)).restrict s)).mono fun x hx1 hx2 hx3 hx4 hx5 => ?_

Result:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
x : X
hx1 : ↑↑(MemLp.toLp ↑↑(f + g) ⋯) x = ↑↑(f + g) x
hx2 : ↑↑(MemLp.toLp ↑↑g ⋯) x = ↑↑g x
hx3 : ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x
hx4 : ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x = (↑↑(MemLp.toLp ↑↑f ⋯) + ↑↑(MemLp.toLp ↑↑g ⋯)) x
hx5 : ↑↑(f + g) x = (↑↑f + ↑↑g) x
⊢ ↑↑(MemLp.toLp ↑↑(f + g) ⋯) x = ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x

Proof state:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x = (↑↑(MemLp.toLp ↑↑f ⋯) + ↑↑(MemLp.toLp ↑↑g ⋯)) x →
      ↑↑(f + g) x = (↑↑f + ↑↑g) x → ↑↑(MemLp.toLp ↑↑(f + g) ⋯) x = ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x

Tactic:
refine (MemLp.coeFn_toLp ((Lp.memLp f).restrict s)).mp ?_

Result:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x →
      ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x = (↑↑(MemLp.toLp ↑↑f ⋯) + ↑↑(MemLp.toLp ↑↑g ⋯)) x →
        ↑↑(f + g) x = (↑↑f + ↑↑g) x → ↑↑(MemLp.toLp ↑↑(f + g) ⋯) x = ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ MemLp.toLp ↑↑(f + g) ⋯ = MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯

Tactic:
ext1

Result:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ↑↑(MemLp.toLp ↑↑(f + g) ⋯) =ᶠ[ae (μ.restrict s)] ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯)

Proof state:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    ↑↑(f + g) x = (↑↑f + ↑↑g) x → ↑↑(MemLp.toLp ↑↑(f + g) ⋯) x = ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x

Tactic:
refine
  (Lp.coeFn_add (MemLp.toLp f ((Lp.memLp f).restrict s))
        (MemLp.toLp g ((Lp.memLp g).restrict s))).mp ?_

Result:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x = (↑↑(MemLp.toLp ↑↑f ⋯) + ↑↑(MemLp.toLp ↑↑g ⋯)) x →
      ↑↑(f + g) x = (↑↑f + ↑↑g) x → ↑↑(MemLp.toLp ↑↑(f + g) ⋯) x = ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x

Proof state:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
x : X
hx1 : ↑↑(MemLp.toLp ↑↑(f + g) ⋯) x = ↑↑(f + g) x
hx2 : ↑↑(MemLp.toLp ↑↑g ⋯) x = ↑↑g x
hx3 : ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x
hx4 : ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x = (↑↑(MemLp.toLp ↑↑f ⋯) + ↑↑(MemLp.toLp ↑↑g ⋯)) x
hx5 : ↑↑(f + g) x = (↑↑f + ↑↑g) x
⊢ ↑↑(MemLp.toLp ↑↑(f + g) ⋯) x = ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x

Tactic:
rw [hx4, hx1, Pi.add_apply, hx2, hx3, hx5, Pi.add_apply]

Result:
no goals

Proof state:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ↑↑(MemLp.toLp ↑↑(f + g) ⋯) =ᶠ[ae (μ.restrict s)] ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯)

Tactic:
refine (ae_restrict_of_ae (Lp.coeFn_add f g)).mp ?_

Result:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
f g : ↥(Lp E p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    ↑↑(f + g) x = (↑↑f + ↑↑g) x → ↑↑(MemLp.toLp ↑↑(f + g) ⋯) x = ↑↑(MemLp.toLp ↑↑f ⋯ + MemLp.toLp ↑↑g ⋯) x