-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem Lp_toLp_restrict_smul (c : 𝕜) (f : Lp F p μ) (s : Set X) :
    ((Lp.memLp (c • f)).restrict s).toLp (⇑(c • f)) = c • ((Lp.memLp f).restrict s).toLp f

Proof state:
case h
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ↑↑(c • f) x = (c • ↑↑f) x → ↑↑(MemLp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • MemLp.toLp ↑↑f ⋯) x

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

Result:
case h
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x →
      ↑↑(c • f) x = (c • ↑↑f) x → ↑↑(MemLp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • MemLp.toLp ↑↑f ⋯) x

Proof state:
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ MemLp.toLp ↑↑(c • f) ⋯ = c • MemLp.toLp ↑↑f ⋯

Tactic:
ext1

Result:
case h
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ↑↑(MemLp.toLp ↑↑(c • f) ⋯) =ᶠ[ae (μ.restrict s)] ↑↑(c • MemLp.toLp ↑↑f ⋯)

Proof state:
case h
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
x : X
hx1 : ↑↑(c • MemLp.toLp ↑↑f ⋯) x = (c • ↑↑(MemLp.toLp ↑↑f ⋯)) x
hx2 : ↑↑(MemLp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • f) x
hx3 : ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x
hx4 : ↑↑(c • f) x = (c • ↑↑f) x
⊢ ↑↑(MemLp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • MemLp.toLp ↑↑f ⋯) x

Tactic:
simp only [hx2, hx1, hx3, hx4, Pi.smul_apply]

Result:
no goals

Proof state:
case h
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ↑↑(MemLp.toLp ↑↑(c • f) ⋯) =ᶠ[ae (μ.restrict s)] ↑↑(c • MemLp.toLp ↑↑f ⋯)

Tactic:
refine (ae_restrict_of_ae (Lp.coeFn_smul c f)).mp ?_

Result:
case h
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ↑↑(c • f) x = (c • ↑↑f) x → ↑↑(MemLp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • MemLp.toLp ↑↑f ⋯) x

Proof state:
case h
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    ↑↑(MemLp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • f) x →
      ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x →
        ↑↑(c • f) x = (c • ↑↑f) x → ↑↑(MemLp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • MemLp.toLp ↑↑f ⋯) x

Tactic:
refine
  (Lp.coeFn_smul c (MemLp.toLp f ((Lp.memLp f).restrict s))).mono fun x hx1 hx2 hx3 hx4 => ?_

Result:
case h
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
x : X
hx1 : ↑↑(c • MemLp.toLp ↑↑f ⋯) x = (c • ↑↑(MemLp.toLp ↑↑f ⋯)) x
hx2 : ↑↑(MemLp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • f) x
hx3 : ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x
hx4 : ↑↑(c • f) x = (c • ↑↑f) x
⊢ ↑↑(MemLp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • MemLp.toLp ↑↑f ⋯) x

Proof state:
case h
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x →
      ↑↑(c • f) x = (c • ↑↑f) x → ↑↑(MemLp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • MemLp.toLp ↑↑f ⋯) x

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

Result:
case h
X : Type u_1
F : Type u_4
mX : MeasurableSpace X
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure X
c : 𝕜
f : ↥(Lp F p μ)
s : Set X
⊢ ∀ᵐ (x : X) ∂μ.restrict s,
    ↑↑(MemLp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • f) x →
      ↑↑(MemLp.toLp ↑↑f ⋯) x = ↑↑f x →
        ↑↑(c • f) x = (c • ↑↑f) x → ↑↑(MemLp.toLp ↑↑(c • f) ⋯) x = ↑↑(c • MemLp.toLp ↑↑f ⋯) x