-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem smul_compLp {𝕜'} [NormedRing 𝕜'] [Module 𝕜' F] [BoundedSMul 𝕜' F] [SMulCommClass 𝕜 𝕜' F]
    (c : 𝕜') (L : E →L[𝕜] F) (f : Lp E p μ) : (c • L).compLp f = c • L.compLp f

Proof state:
case h
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
𝕜 : Type u_7
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
𝕜' : Type u_8
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : BoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
c : 𝕜'
L : E →L[𝕜] F
f : ↥(Lp E p μ)
x : α
hx : ↑↑(L.compLp f) x = (fun a => L (↑↑f a)) x
⊢ (fun a => (c • L) (↑↑f a)) x = (c • ↑↑(L.compLp f)) x

Tactic:
rw [Pi.smul_apply, hx, coe_smul', Pi.smul_def]

Result:
no goals

Proof state:
case h
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
𝕜 : Type u_7
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
𝕜' : Type u_8
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : BoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
c : 𝕜'
L : E →L[𝕜] F
f : ↥(Lp E p μ)
⊢ ↑↑((c • L).compLp f) =ᶠ[ae μ] ↑↑(c • L.compLp f)

Tactic:
refine (coeFn_compLp' (c • L) f).trans ?_

Result:
case h
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
𝕜 : Type u_7
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
𝕜' : Type u_8
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : BoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
c : 𝕜'
L : E →L[𝕜] F
f : ↥(Lp E p μ)
⊢ (fun a => (c • L) (↑↑f a)) =ᶠ[ae μ] ↑↑(c • L.compLp f)

Proof state:
case h
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
𝕜 : Type u_7
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
𝕜' : Type u_8
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : BoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
c : 𝕜'
L : E →L[𝕜] F
f : ↥(Lp E p μ)
⊢ (fun a => (c • L) (↑↑f a)) =ᶠ[ae μ] ↑↑(c • L.compLp f)

Tactic:
refine EventuallyEq.trans ?_ (Lp.coeFn_smul _ _).symm

Result:
case h
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
𝕜 : Type u_7
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
𝕜' : Type u_8
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : BoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
c : 𝕜'
L : E →L[𝕜] F
f : ↥(Lp E p μ)
⊢ (fun a => (c • L) (↑↑f a)) =ᶠ[ae μ] c • ↑↑(L.compLp f)

Proof state:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
𝕜 : Type u_7
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
𝕜' : Type u_8
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : BoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
c : 𝕜'
L : E →L[𝕜] F
f : ↥(Lp E p μ)
⊢ (c • L).compLp f = c • L.compLp f

Tactic:
ext1

Result:
case h
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
𝕜 : Type u_7
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
𝕜' : Type u_8
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : BoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
c : 𝕜'
L : E →L[𝕜] F
f : ↥(Lp E p μ)
⊢ ↑↑((c • L).compLp f) =ᶠ[ae μ] ↑↑(c • L.compLp f)

Proof state:
case h
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
𝕜 : Type u_7
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
𝕜' : Type u_8
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : BoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
c : 𝕜'
L : E →L[𝕜] F
f : ↥(Lp E p μ)
⊢ (fun a => (c • L) (↑↑f a)) =ᶠ[ae μ] c • ↑↑(L.compLp f)

Tactic:
refine (L.coeFn_compLp' f).mono fun x hx => ?_

Result:
case h
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
𝕜 : Type u_7
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 F
𝕜' : Type u_8
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : BoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
c : 𝕜'
L : E →L[𝕜] F
f : ↥(Lp E p μ)
x : α
hx : ↑↑(L.compLp f) x = (fun a => L (↑↑f a)) x
⊢ (fun a => (c • L) (↑↑f a)) x = (c • ↑↑(L.compLp f)) x