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

Proof state:
α : 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
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ

Tactic:
have hs_eq : s = ⋃ i, S i ∩ s := by
  simp_rw [Set.inter_comm]
  rw [← Set.inter_iUnion, iUnion_spanningSets (μ.trim hm), Set.inter_univ]

Result:
α : 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
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ i, S i ∩ s
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ

Proof state:
α : 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
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ

Tactic:
have hS_meas0 : ∀ i, MeasurableSet (S i) := fun i => hm _ (hS_meas i)

Result:
α : 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
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
⊢ ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ

Proof state:
α : 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
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ i, S i ∩ s
hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ⊤
h_mono : Monotone fun i => S i ∩ s
h_eq_forall :
  (fun i => ∫ (x : α) in S i ∩ s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ) = fun i => ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ
h_right : Tendsto (fun i => ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ) atTop (𝓝 (∫ (x : α) in s, ↑↑f x ∂μ))
⊢ Tendsto (fun i => ∫ (x : α) in S i ∩ s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ))

Tactic:
have h := tendsto_setIntegral_of_monotone (fun i => (hS_meas0 i).inter (hm s hs)) h_mono
  (L1.integrable_coeFn (condExpL1CLM F' hm μ f)).integrableOn

Result:
α : 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
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ i, S i ∩ s
hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ⊤
h_mono : Monotone fun i => S i ∩ s
h_eq_forall :
  (fun i => ∫ (x : α) in S i ∩ s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ) = fun i => ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ
h_right : Tendsto (fun i => ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ) atTop (𝓝 (∫ (x : α) in s, ↑↑f x ∂μ))
h :
  Tendsto (fun i => ∫ (x : α) in S i ∩ s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ) atTop
    (𝓝 (∫ (x : α) in ⋃ n, S n ∩ s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ))
⊢ Tendsto (fun i => ∫ (x : α) in S i ∩ s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ))

Proof state:
α : 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
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ i, S i ∩ s
hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ⊤
i j : ℕ
hij : i ≤ j
x : α
⊢ x ∈ S i ∧ x ∈ s → x ∈ S j ∧ x ∈ s

Tactic:
exact fun h => ⟨monotone_spanningSets (μ.trim hm) hij h.1, h.2⟩

Result:
no goals

Proof state:
α : 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
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ i, S i ∩ s
hS_finite : ∀ (i : ℕ), μ (S i ∩ s) < ⊤
h_mono : Monotone fun i => S i ∩ s
h_eq_forall :
  (fun i => ∫ (x : α) in S i ∩ s, ↑↑((condExpL1CLM F' hm μ) f) x ∂μ) = fun i => ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ
h : Tendsto (fun i => ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ) atTop (𝓝 (∫ (x : α) in ⋃ n, S n ∩ s, ↑↑f x ∂μ))
⊢ Tendsto (fun i => ∫ (x : α) in S i ∩ s, ↑↑f x ∂μ) atTop (𝓝 (∫ (x : α) in s, ↑↑f x ∂μ))

Tactic:
rwa [← hs_eq] at h

Result:
no goals