-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpIndL1Fin_add (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x y : G) :
    condExpIndL1Fin hm hs hμs (x + y) =
    condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm hs hμs 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 ≠ ⊤
x y : G
⊢ ↑↑(condExpIndSMul hm hs hμs (x + y)) =ᶠ[ae μ] ↑↑(condExpIndL1Fin hm hs hμs x) + ↑↑(condExpIndL1Fin hm hs hμs y)

Tactic:
refine EventuallyEq.trans ?_
  (EventuallyEq.add (MemLp.coeFn_toLp q).symm (MemLp.coeFn_toLp q).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 ≠ ⊤
x y : G
⊢ ↑↑(condExpIndSMul hm hs hμs (x + y)) =ᶠ[ae μ] fun x_1 =>
    ↑↑(condExpIndSMul hm hs hμs x) x_1 + ↑↑(condExpIndSMul hm hs hμs y) x_1

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 ≠ ⊤
x y : G
a : α
⊢ (↑↑(condExpIndSMul hm hs hμs x) + ↑↑(condExpIndSMul hm hs hμs y)) a =
    (fun x_1 => ↑↑(condExpIndSMul hm hs hμs x) x_1 + ↑↑(condExpIndSMul hm hs hμs y) x_1) a

Tactic:
rfl

Result:
no goals

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 ≠ ⊤
x y : G
⊢ ↑↑(condExpIndL1Fin hm hs hμs (x + y)) =ᶠ[ae μ] ↑↑(condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm hs hμs y)

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 ≠ ⊤
x y : G
⊢ ↑↑(condExpIndSMul hm hs hμs (x + y)) =ᶠ[ae μ] ↑↑(condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm hs hμs y)

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 ≠ ⊤
x y : G
⊢ condExpIndL1Fin hm hs hμs (x + y) = condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm hs hμs y

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 ≠ ⊤
x y : G
⊢ ↑↑(condExpIndL1Fin hm hs hμs (x + y)) =ᶠ[ae μ] ↑↑(condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm hs hμs 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 ≠ ⊤
x y : G
⊢ ↑↑(condExpIndSMul hm hs hμs (x + y)) =ᶠ[ae μ] fun x_1 =>
    ↑↑(condExpIndSMul hm hs hμs x) x_1 + ↑↑(condExpIndSMul hm hs hμs y) x_1

Tactic:
rw [condExpIndSMul_add]

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 ≠ ⊤
x y : G
⊢ ↑↑(condExpIndSMul hm hs hμs x + condExpIndSMul hm hs hμs y) =ᶠ[ae μ] fun x_1 =>
    ↑↑(condExpIndSMul hm hs hμs x) x_1 + ↑↑(condExpIndSMul hm hs hμs y) x_1

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 ≠ ⊤
x y : G
⊢ ↑↑(condExpIndSMul hm hs hμs (x + y)) =ᶠ[ae μ] ↑↑(condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm hs hμs y)

Tactic:
refine EventuallyEq.trans ?_ (Lp.coeFn_add _ _).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 ≠ ⊤
x y : G
⊢ ↑↑(condExpIndSMul hm hs hμs (x + y)) =ᶠ[ae μ] ↑↑(condExpIndL1Fin hm hs hμs x) + ↑↑(condExpIndL1Fin hm hs hμs 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 ≠ ⊤
x y : G
⊢ ↑↑(condExpIndSMul hm hs hμs x + condExpIndSMul hm hs hμs y) =ᶠ[ae μ] fun x_1 =>
    ↑↑(condExpIndSMul hm hs hμs x) x_1 + ↑↑(condExpIndSMul hm hs hμs y) x_1

Tactic:
refine (Lp.coeFn_add _ _).trans (Eventually.of_forall fun a => ?_)

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 ≠ ⊤
x y : G
a : α
⊢ (↑↑(condExpIndSMul hm hs hμs x) + ↑↑(condExpIndSMul hm hs hμs y)) a =
    (fun x_1 => ↑↑(condExpIndSMul hm hs hμs x) x_1 + ↑↑(condExpIndSMul hm hs hμs y) x_1) a