awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f_1 : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hf :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
hg :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
refine_2 :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      HAdd.hAdd (α := F')
        ((↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
          x)
        ((↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
          x) ∂μ)
    (∫ (x : α) in s,
      (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x + (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      HAdd.hAdd (α := α → F') (β := α → F')
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s,
      ((↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') + (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F')) x ∂μ)

Tactic:
simp_rw [Pi.add_apply]

Premises used: Pi.add_apply
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp F' 1 μ)) ↦
    ∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ

Tactic:
(continuous_setIntegral s).comp (condExpL1CLM F' hm μ).continuous

Premises used: Continuous.comp, MeasureTheory.condExpL1CLM, ContinuousLinearMap.continuous, MeasureTheory.continuous_setIntegral
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp F' 1 μ)) ↦
    ∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ

Tactic:
exact (continuous_setIntegral s).comp (condExpL1CLM F' hm μ).continuous

Premises used: Continuous.comp, MeasureTheory.condExpL1CLM, ContinuousLinearMap.continuous, MeasureTheory.continuous_setIntegral
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp F' 1 μ)) ↦
    ∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ

Tactic:
continuous_setIntegral s

Premises used: MeasureTheory.continuous_setIntegral
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp F' 1 μ)) ↦
    ∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ

Tactic:
exact continuous_setIntegral s

Premises used: MeasureTheory.continuous_setIntegral
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
⊢ ∀ (i : ℕ), MeasurableSet (S i)

Tactic:
have hS_meas : ∀ i, MeasurableSet[m] (S i) := measurableSet_spanningSets (μ.trim hm)
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
⊢ ∀ (i : ℕ), MeasurableSet (S i)

Tactic:
have hS_meas0 : ∀ i, MeasurableSet (S i) := fun i => hm _ (hS_meas i)
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
simp_rw : s = ⋃ (i : ℕ), s ∩ S i
⊢ s = ⋃ (i : ℕ), S i ∩ s

Tactic:
simp_rw [Set.inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
rw : s = s ∩ ⋃ (i : ℕ), S i
rw₁ : s = s ∩ Set.univ
rw₂ rw₃ : s = s
⊢ s = ⋃ (i : ℕ), s ∩ S i

Tactic:
rw [← Set.inter_iUnion, iUnion_spanningSets (μ.trim hm), Set.inter_univ]

Premises used: Set.inter_univ, MeasureTheory.Measure.trim, MeasureTheory.iUnion_spanningSets, Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
⊢ s = ⋃ (i : ℕ), S i ∩ s

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]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
⊢ ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
fun i => (measure_mono Set.inter_subset_left).trans_lt ?_

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
refine : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine fun i => (measure_mono Set.inter_subset_left).trans_lt ?_

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
i : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim hm) i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hS_finite_trim := measure_spanningSets_lt_top (μ.trim hm) i
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
i : ℕ
hS_finite_trim : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (spanningSets (μ.trim hm) i) : ℝ≥0∞) (∞ : ℝ≥0∞)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hS_finite_trim : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [trim_measurableSet_eq hm (hS_meas i)] at hS_finite_trim

Premises used: MeasureTheory.trim_measurableSet_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → 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 : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
i j : ℕ
hij : i ≤ j
x : α
⊢ x ∈ S i ∧ x ∈ s → x ∈ S j ∧ x ∈ s

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

Premises used: MeasureTheory.monotone_spanningSets, MeasureTheory.Measure.trim, And.right, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → 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 : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
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⟩
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → 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 : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s

Tactic:
have h_mono : Monotone fun i => S i ∩ s := by
    intro i j hij x
    simp_rw [Set.mem_inter_iff]
    exact fun h => ⟨monotone_spanningSets (μ.trim hm) hij h.1, h.2⟩
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → 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 : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
⊢ Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ

Tactic:
have h_eq_forall :
    (fun i => ∫ x in S i ∩ s, condExpL1CLM F' hm μ f x ∂μ) = fun i => ∫ x in S i ∩ s, f x ∂μ :=
    funext fun i =>
      setIntegral_condExpL1CLM_of_measure_ne_top f (@MeasurableSet.inter α m _ _ (hS_meas i) hs)
        (hS_finite i).ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → 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 : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
⊢ Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in ⋃ (n : ℕ), S n ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))

Tactic:
have h :=
      tendsto_setIntegral_of_monotone (fun i => (hS_meas0 i).inter (hm s hs)) h_mono
        (L1.integrable_coeFn f).integrableOn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → 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 : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
h :
  Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in ⋃ (n : ℕ), S n ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h :
      Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
        (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))),
    Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
      (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
⊢ Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))

Tactic:
rwa [← hs_eq] at h
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → 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 : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
⊢ Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))

Tactic:
have h_right : Tendsto (fun i => ∫ x in S i ∩ s, f x ∂μ) atTop (𝓝 (∫ x in s, f x ∂μ)) := by
    have h :=
      tendsto_setIntegral_of_monotone (fun i => (hS_meas0 i).inter (hm s hs)) h_mono
        (L1.integrable_coeFn f).integrableOn
    rwa [← hs_eq] at h
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → 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 : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
h_right :
  Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
⊢ Tendsto.{0, u_3} (β := F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    atTop
    (𝓝
      (∫ (x : α) in ⋃ (n : ℕ), S n ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → 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
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → 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 : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
h_right :
  Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
h :
  Tendsto.{0, u_3} (β := F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    atTop
    (𝓝
      (∫ (x : α) in ⋃ (n : ℕ), S n ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h :
      Tendsto.{0, u_3} (β := F')
        (fun (i : ℕ) ↦
          ∫ (x : α) in S i ∩ s,
            (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
        atTop
        (𝓝
          (∫ (x : α) in s,
            (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))),
    Tendsto.{0, u_3} (β := F')
      (fun (i : ℕ) ↦
        ∫ (x : α) in S i ∩ s,
          (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
      atTop
      (𝓝
        (∫ (x : α) in s,
          (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))
⊢ Tendsto.{0, u_3} (β := F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    atTop
    (𝓝
      (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))

Tactic:
rwa [← hs_eq] at h