-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpIndL1Fin_smul (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (c : ℝ) (x : G) :
    condExpIndL1Fin hm hs hμs (c • x) = c • condExpIndL1Fin hm hs hμs x

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
⊢ 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
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
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
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
⊢ ↑↑(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
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
⊢ ↑↑(c • condExpIndSMul hm hs hμs x) =ᶠ[ae μ] c • ↑↑(condExpIndL1Fin hm hs hμs x)

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
⊢ ↑↑(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
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
⊢ c • ↑↑(condExpIndSMul hm hs hμs x) =ᶠ[ae μ] c • ↑↑(condExpIndL1Fin hm hs hμs x)

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
⊢ condExpIndL1Fin hm hs hμs (c • x) = c • condExpIndL1Fin hm hs hμs x

Tactic:
ext1

Result:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
⊢ ↑↑(condExpIndL1Fin hm hs hμs (c • x)) =ᶠ[ae μ] ↑↑(c • condExpIndL1Fin hm hs hμs x)

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
⊢ ↑↑(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
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
⊢ ↑↑(condExpIndSMul hm hs hμs (c • x)) =ᶠ[ae μ] c • ↑↑(condExpIndL1Fin hm hs hμs x)

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
⊢ ↑↑(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
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
⊢ ↑↑(condExpIndSMul hm hs hμs (c • x)) =ᶠ[ae μ] ↑↑(c • condExpIndL1Fin hm hs hμs x)

Proof state:
case h
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
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