-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem lpMeasToLpTrim_smul (hm : m ≤ m0) (c : 𝕜) (f : lpMeas F 𝕜 m p μ) :
    lpMeasToLpTrim F 𝕜 p μ hm (c • f) = c • lpMeasToLpTrim F 𝕜 p μ hm f

Proof state:
case h.refine_1
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ StronglyMeasurable (c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f))

Tactic:
exact (Lp.stronglyMeasurable _).const_smul c

Result:
no goals

Proof state:
case h.refine_2
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ ↑↑↑(c • f) =ᶠ[ae μ] c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)

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

Result:
case h.refine_2
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ c • ↑↑↑f =ᶠ[ae μ] c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)

Proof state:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ ↑↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) =ᶠ[ae (μ.trim hm)] ↑↑(c • lpMeasToLpTrim F 𝕜 p μ hm f)

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

Result:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ ↑↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) =ᶠ[ae (μ.trim hm)] c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)

Proof state:
case h.refine_2
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ c • ↑↑↑f =ᶠ[ae μ] c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)

Tactic:
refine (lpMeasToLpTrim_ae_eq hm f).mono fun x hx => ?_

Result:
case h.refine_2
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
x : α
hx : ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f) x = ↑↑↑f x
⊢ (c • ↑↑↑f) x = (c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)) x

Proof state:
case h.refine_2
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
x : α
hx : ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f) x = ↑↑↑f x
⊢ (c • ↑↑↑f) x = (c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)) x

Tactic:
simp only [Pi.smul_apply, hx]

Result:
no goals

Proof state:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ ↑↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) =ᶠ[ae (μ.trim hm)] c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)

Tactic:
refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm ?_ ?_

Result:
case h.refine_1
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ StronglyMeasurable (c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f))

case h.refine_2
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ ↑↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) =ᶠ[ae μ] c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)

Proof state:
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ lpMeasToLpTrim F 𝕜 p μ hm (c • f) = c • lpMeasToLpTrim F 𝕜 p μ hm f

Tactic:
ext1

Result:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ ↑↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) =ᶠ[ae (μ.trim hm)] ↑↑(c • lpMeasToLpTrim F 𝕜 p μ hm f)

Proof state:
case h.refine_2
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ ↑↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) =ᶠ[ae μ] c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)

Tactic:
refine (lpMeasToLpTrim_ae_eq hm _).trans ?_

Result:
case h.refine_2
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ ↑↑↑(c • f) =ᶠ[ae μ] c • ↑↑(lpMeasToLpTrim F 𝕜 p μ hm f)