-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpIndL1Fin_smul' [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (hs : MeasurableSet s)
    (hμs : μ s ≠ ∞) (c : 𝕜) (x : F) :
    condExpIndL1Fin hm hs hμs (c • x) = c • condExpIndL1Fin hm hs hμs x

Proof state:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝² : SigmaFinite (μ.trim hm)
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : 𝕜
x : F
⊢ ↑↑(condExpIndSMul hm hs hμs (c • x)) =ᶠ[ae μ] ↑↑(c • condExpIndL1Fin hm hs hμs x)

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

Result:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝² : SigmaFinite (μ.trim hm)
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : 𝕜
x : F
⊢ ↑↑(condExpIndSMul hm hs hμs (c • x)) =ᶠ[ae μ] c • ↑↑(condExpIndL1Fin hm hs hμs x)

Proof state:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝² : SigmaFinite (μ.trim hm)
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : 𝕜
x : F
⊢ c • ↑↑(condExpIndSMul hm hs hμs x) =ᶠ[ae μ] c • ↑↑(condExpIndL1Fin hm hs hμs x)

Tactic:
refine (condExpIndL1Fin_ae_eq_condExpIndSMul hm hs hμs x).mono fun y hy => ?_

Result:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝² : SigmaFinite (μ.trim hm)
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : 𝕜
x : F
y : α
hy : ↑↑(condExpIndL1Fin hm hs hμs x) y = ↑↑(condExpIndSMul hm hs hμs x) y
⊢ (c • ↑↑(condExpIndSMul hm hs hμs x)) y = (c • ↑↑(condExpIndL1Fin hm hs hμs x)) y

Proof state:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝² : SigmaFinite (μ.trim hm)
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : 𝕜
x : F
⊢ ↑↑(condExpIndSMul hm hs hμs (c • x)) =ᶠ[ae μ] c • ↑↑(condExpIndL1Fin hm hs hμs x)

Tactic:
rw [condExpIndSMul_smul' hs hμs c x]

Result:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝² : SigmaFinite (μ.trim hm)
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : 𝕜
x : F
⊢ ↑↑(c • condExpIndSMul hm hs hμs x) =ᶠ[ae μ] c • ↑↑(condExpIndL1Fin hm hs hμs x)

Proof state:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝² : SigmaFinite (μ.trim hm)
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : 𝕜
x : F
y : α
hy : ↑↑(condExpIndL1Fin hm hs hμs x) y = ↑↑(condExpIndSMul hm hs hμs x) y
⊢ (c • ↑↑(condExpIndSMul hm hs hμs x)) y = (c • ↑↑(condExpIndL1Fin hm hs hμs x)) y

Tactic:
simp only [Pi.smul_apply, hy]

Result:
no goals

Proof state:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝² : SigmaFinite (μ.trim hm)
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : 𝕜
x : F
⊢ ↑↑(condExpIndL1Fin hm hs hμs (c • x)) =ᶠ[ae μ] ↑↑(c • condExpIndL1Fin hm hs hμs x)

Tactic:
refine (MemLp.coeFn_toLp q).trans ?_

Result:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝² : SigmaFinite (μ.trim hm)
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : 𝕜
x : F
⊢ ↑↑(condExpIndSMul hm hs hμs (c • x)) =ᶠ[ae μ] ↑↑(c • condExpIndL1Fin hm hs hμs x)

Proof state:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝² : SigmaFinite (μ.trim hm)
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : 𝕜
x : F
⊢ ↑↑(c • condExpIndSMul hm hs hμs x) =ᶠ[ae μ] c • ↑↑(condExpIndL1Fin hm hs hμs x)

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

Result:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝² : SigmaFinite (μ.trim hm)
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : 𝕜
x : F
⊢ c • ↑↑(condExpIndSMul hm hs hμs x) =ᶠ[ae μ] c • ↑↑(condExpIndL1Fin hm hs hμs x)

Proof state:
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝² : SigmaFinite (μ.trim hm)
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : 𝕜
x : F
⊢ condExpIndL1Fin hm hs hμs (c • x) = c • condExpIndL1Fin hm hs hμs x

Tactic:
ext1

Result:
case h
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst✝² : SigmaFinite (μ.trim hm)
inst✝¹ : NormedSpace ℝ F
inst✝ : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : 𝕜
x : F
⊢ ↑↑(condExpIndL1Fin hm hs hμs (c • x)) =ᶠ[ae μ] ↑↑(c • condExpIndL1Fin hm hs hμs x)