-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem setIntegral_condExpL1CLM_of_measure_ne_top (f : α →₁[μ] F') (hs : MeasurableSet[m] s)
    (hμs : μ s ≠ ∞) : ∫ x in s, condExpL1CLM F' hm μ f x ∂μ = ∫ x in s, f x ∂μ

Proof state:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ),
    Disjoint (Function.support f) (Function.support g) →
      (fun f => ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ) (MemLp.toLp f hf) →
        (fun f => ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ) (MemLp.toLp g hg) →
          (fun f => ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ)
            (MemLp.toLp f hf + MemLp.toLp g hg)

Tactic:
intro f g hf_Lp hg_Lp _ hf hg

Result:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp)) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) x ∂μ

Proof state:
case refine_4
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ Continuous fun f => ∫ (x : α) in s, ↑↑f x ∂μ

Tactic:
exact continuous_setIntegral s

Result:
no goals

Proof state:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F'
t : Set α
ht : MeasurableSet t
hμt : μ t < ⊤
⊢ ∫ (x_1 : α) in s, ↑↑((condExpInd F' hm μ t) x) x_1 ∂μ =
    ∫ (x_1 : α) in s, ↑↑↑(simpleFunc.indicatorConst 1 ht ⋯ x) x_1 ∂μ

Tactic:
rw [Lp.simpleFunc.coe_indicatorConst, setIntegral_indicatorConstLp (hm _ hs)]

Result:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F'
t : Set α
ht : MeasurableSet t
hμt : μ t < ⊤
⊢ ∫ (x_1 : α) in s, ↑↑((condExpInd F' hm μ t) x) x_1 ∂μ = (μ (t ∩ s)).toReal • x

Proof state:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∀ (c : F') {s_1 : Set α} (hs : MeasurableSet s_1) (hμs : μ s_1 < ⊤),
    (fun f => ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ)
      ↑(simpleFunc.indicatorConst 1 hs ⋯ c)

Tactic:
intro x t ht hμt

Result:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F'
t : Set α
ht : MeasurableSet t
hμt : μ t < ⊤
⊢ ∫ (x_1 : α) in s, ↑↑((condExpL1CLM F' hm μ) ↑(simpleFunc.indicatorConst 1 ht ⋯ x)) x_1 ∂μ =
    ∫ (x_1 : α) in s, ↑↑↑(simpleFunc.indicatorConst 1 ht ⋯ x) x_1 ∂μ

Proof state:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp) + (condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) x ∂μ

Tactic:
rw [setIntegral_congr_ae (hm s hs) ((Lp.coeFn_add (condExpL1CLM F' hm μ (hf_Lp.toLp f))
  (condExpL1CLM F' hm μ (hg_Lp.toLp g))).mono fun x hx _ => hx)]

Result:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s,
      (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) + ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp))) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) x ∂μ

Proof state:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s,
      (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) + ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp))) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp + MemLp.toLp g hg_Lp) x ∂μ

Tactic:
rw [setIntegral_congr_ae (hm s hs)
  ((Lp.coeFn_add (hf_Lp.toLp f) (hg_Lp.toLp g)).mono fun x hx _ => hx)]

Result:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s,
      (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) + ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp))) x ∂μ =
    ∫ (x : α) in s, (↑↑(MemLp.toLp f hf_Lp) + ↑↑(MemLp.toLp g hg_Lp)) x ∂μ