awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
pos :
  ∀ (s : Set 𝓧) (hs : MeasurableSet s) (hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Integrable (ε := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ
⊢ ∀ (s : Set 𝓧),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) s μ

Tactic:
refine fun s hs hsμ ↦ Integrable.integrableOn ?_

Premises used: MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ AEMeasurable μ⁻[f|m] μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : ∫⁻ (x : 𝓧), μ⁻[f|m] x ∂μ ≠ ∞
pos₁ pos₂ pos₃ pos₄ : ∫⁻ (ω : 𝓧), f ω ∂μ ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ

Tactic:
rwa [integrable_toReal_iff (by fun_prop) (condLExp_ne_top hf), lintegral_condLExp]

Premises used: MeasureTheory.integrable_toReal_iff, MeasureTheory.lintegral_condLExp, MeasureTheory.condLExp_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ AEMeasurable μ⁻[f|m] (μ.restrict s)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ AEMeasurable f (μ.restrict s)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : ∀ᵐ (x : 𝓧) ∂μ.restrict s, f x < ∞
pos₁ : ∀ᵐ (x : 𝓧) ∂μ.restrict s, μ⁻[f|m] x < ∞
⊢ Eq (α := ℝ) (∫ (x : 𝓧) in s, (μ⁻[f|m] x).toReal ∂μ) (∫ (x : 𝓧) in s, (f x).toReal ∂μ)

Tactic:
rw [integral_toReal (by fun_prop), integral_toReal (by fun_prop),
      setLIntegral_condLExp _ _ _ hs]

Premises used: MeasureTheory.setLIntegral_condLExp, MeasureTheory.integral_toReal
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : 𝓧) ∂μ.restrict s, f x < ∞

Tactic:
ae_lt_top' hf_meas.restrict ((setLIntegral_le_lintegral _ _).trans_lt hf.lt_top).ne

Premises used: AEMeasurable.restrict, Ne.lt_top, MeasureTheory.ae_lt_top', LE.le.trans_lt, MeasureTheory.setLIntegral_le_lintegral, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : 𝓧) ∂μ.restrict s, f x < ∞

Tactic:
exact ae_lt_top' hf_meas.restrict ((setLIntegral_le_lintegral _ _).trans_lt hf.lt_top).ne

Premises used: AEMeasurable.restrict, Ne.lt_top, MeasureTheory.ae_lt_top', LE.le.trans_lt, MeasureTheory.setLIntegral_le_lintegral, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : 𝓧) ∂μ.restrict s, μ⁻[f|m] x < ∞

Tactic:
ae_restrict_of_ae (condLExp_lt_top hf)

Premises used: MeasureTheory.ae_restrict_of_ae, MeasureTheory.condLExp_lt_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : 𝓧) ∂μ.restrict s, μ⁻[f|m] x < ∞

Tactic:
exact ae_restrict_of_ae (condLExp_lt_top hf)

Premises used: MeasureTheory.ae_restrict_of_ae, MeasureTheory.condLExp_lt_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
⊢ StronglyMeasurable (β := ℝ) fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : 𝓧) ↦ (μ⁻[f|m] x).toReal) μ

Tactic:
exact StronglyMeasurable.aestronglyMeasurable (by fun_prop)

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f_1 : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
s : Set Ω
c : F
f : Ω → E
h :
  ∀ (ω : Ω),
    Eq.{u_4 + 1} (α := G)
      ((((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω) : G)
      (s.indicator (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω)) ω : G)
⊢ Eq (α := (ω : Ω) → G)
    (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
    (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))

Tactic:
ext ω
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f_1 : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
s : Set Ω
c : F
f : Ω → E
ω : Ω
pos :
  ∀ (hω : ω ∈ s),
    Eq.{u_4 + 1} (α := G)
      ((((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω) : G)
      (s.indicator (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω)) ω : G)
neg :
  ∀ (hω : ω ∉ s),
    Eq.{u_4 + 1} (α := G)
      ((((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω) : G)
      (s.indicator (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω)) ω : G)
⊢ Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω) : G)
    (s.indicator (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω)) ω : G)

Tactic:
by_cases hω : ω ∈ s
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f_1 : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
s : Set Ω
c : F
f : Ω → E
ω : Ω
hω : ω ∈ s
⊢ Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω) : G)
    (s.indicator (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω)) ω : G)

Tactic:
simp [hω]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f_1 : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
s : Set Ω
c : F
f : Ω → E
ω : Ω
hω : ω ∉ s
⊢ Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω) : G)
    (s.indicator (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω)) ω : G)

Tactic:
simp [hω]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
⊢ ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))

Tactic:
have : ∀ (s c) (f : Ω → E),
      (fun ω ↦ B (Set.indicator s (Function.const Ω c) ω) (f ω)) =
        s.indicator (fun ω ↦ B c (f ω)) := by
    intro s c f
    ext ω
    by_cases hω : ω ∈ s <;> simp [hω]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
apply :
  ∀ (c : F) (s : Set Ω) (hs : MeasurableSet s),
    EventuallyEq.{u_1, u_4} (β := G) (ae μ)
      μ[fun (ω : Ω) ↦
        (((B : (a : F) → E →L[ℝ] G)
                ((SimpleFunc.piecewise s hs (SimpleFunc.const Ω c) (SimpleFunc.const Ω 0) : (a : Ω) → F) ω) :
              E →L[ℝ] G) :
            (a : E) → G)
          (g ω) |
        m]
      fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G)
              ((SimpleFunc.piecewise s hs (SimpleFunc.const Ω c) (SimpleFunc.const Ω 0) : (a : Ω) → F) ω) :
            E →L[ℝ] G) :
          (a : E) → G)
        (μ[g | m] ω)
apply₁ :
  ∀ (g₁ g₂ : SimpleFunc Ω F),
    Disjoint.{u_1} (α := Set Ω) (Function.support.{u_1, u_3} (M := F) (⇑g₁ : (a : Ω) → F))
        (Function.support.{u_1, u_3} (M := F) (⇑g₂ : (a : Ω) → F)) →
      ∀
        (h_eq₁ :
          (fun (f : SimpleFunc Ω F) ↦
              EventuallyEq.{u_1, u_4} (β := G) (ae μ)
                μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
                fun (ω : Ω) ↦
                (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
            g₁)
        (h_eq₂ :
          (fun (f : SimpleFunc Ω F) ↦
              EventuallyEq.{u_1, u_4} (β := G) (ae μ)
                μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
                fun (ω : Ω) ↦
                (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
            g₂),
        EventuallyEq.{u_1, u_4} (β := G) (ae μ)
          μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ + g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
          fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ + g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)

Tactic:
apply @SimpleFunc.induction _ _ m _ (fun f ↦ _)
    (fun c s hs ↦ ?_) (fun g₁ g₂ _ h_eq₁ h_eq₂ ↦ ?_) f

Premises used: MeasureTheory.SimpleFunc.induction
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
c : F
s : Set Ω
hs : MeasurableSet s
simp :
  EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) |
      m]
    fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G)
              ((SimpleFunc.piecewise s hs (SimpleFunc.const Ω c) (SimpleFunc.const Ω 0) : (a : Ω) → F) ω) :
            E →L[ℝ] G) :
          (a : E) → G)
        (g ω) |
      m]
    fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G)
            ((SimpleFunc.piecewise s hs (SimpleFunc.const Ω c) (SimpleFunc.const Ω 0) : (a : Ω) → F) ω) :
          E →L[ℝ] G) :
        (a : E) → G)
      (μ[g | m] ω)

Tactic:
simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
      SimpleFunc.coe_zero, Set.piecewise_eq_indicator]

Premises used: MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, MeasureTheory.SimpleFunc.const_zero, Set.piecewise_eq_indicator, MeasureTheory.SimpleFunc.coe_const
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
c : F
s : Set Ω
hs : MeasurableSet s
rw :
  EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) |
      m]
    fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)

Tactic:
rw [this, this]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
c : F
s : Set Ω
hs : MeasurableSet s
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))

Tactic:
(condExp_indicator ((B c).integrable_comp hg) hs).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_indicator, ContinuousLinearMap.integrable_comp, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
c : F
s : Set Ω
hs : MeasurableSet s
refine :
  EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (s.indicator μ[fun (a : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (g a) | m])
    (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))

Tactic:
refine (condExp_indicator ((B c).integrable_comp hg) hs).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_indicator, ContinuousLinearMap.integrable_comp, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
c : F
s : Set Ω
hs : MeasurableSet s
h :
  ∀ (ω : Ω)
    (hω :
      Eq.{u_4 + 1} (α := G) (((⇑((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) ∘ μ[g | m]) ω)
        (μ[(⇑((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) ∘ g | m] ω)),
    Eq.{u_4 + 1} (α := G)
      (s.indicator μ[fun (a : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (g a) | m] ω)
      (s.indicator (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)) ω)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (s.indicator μ[fun (a : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (g a) | m])
    (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))

Tactic:
filter_upwards [(B c).comp_condExp_comm hg (m := m)] with ω hω

Premises used: ContinuousLinearMap.comp_condExp_comm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
c : F
s : Set Ω
hs : MeasurableSet s
ω : Ω
hω :
  Eq.{u_4 + 1} (α := G) ((((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)
    (μ[(⇑((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) ∘ g | m] ω : G)
⊢ Eq.{u_4 + 1} (α := G)
    (s.indicator μ[fun (a : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (g a) | m] ω)
    (s.indicator (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)) ω)

Tactic:
simp only [Set.indicator, hω, Function.comp_def]

Premises used: Set.indicator, Function.comp_def