awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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Ω
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this_1 : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), norm.{u_3} (E := F) ((fs n : (a : Ω) → F) ω : F) ≤ c
this :
  Eq (α := Ω → G) μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) | m]
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
n : ℕ
neg :
  EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    μ[(fun (n : ℕ) (ω : Ω) ↦
          ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
        n |
      m]
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[(fun (n : ℕ) (ω : Ω) ↦
          ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G))
        n |
      m]
    μ[(fun (n : ℕ) (ω : Ω) ↦
          ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
        n |
      m]

Tactic:
refine (condExp_stronglyMeasurable_simpleFunc_bilin B hm _ hg).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_stronglyMeasurable_simpleFunc_bilin
-- 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Ω
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this_1 : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), norm.{u_3} (E := F) ((fs n : (a : Ω) → F) ω : F) ≤ c
this :
  Eq (α := Ω → G) μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) | m]
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
n : ℕ
neg :
  StronglyMeasurable.{u_1, u_4} (α := Ω) (β := G)
    ((fun (n : ℕ) (ω : Ω) ↦
        ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
      n)
neg₁ :
  Integrable.{u_4, u_1} (ε := G)
    ((fun (n : ℕ) (ω : Ω) ↦
        ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
      n)
    μ
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    μ[(fun (n : ℕ) (ω : Ω) ↦
          ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
        n |
      m]

Tactic:
nth_rw 2 [condExp_of_stronglyMeasurable hm]

Premises used: MeasureTheory.condExp_of_stronglyMeasurable
-- 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Ω
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this_1 : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), norm.{u_3} (E := F) ((fs n : (a : Ω) → F) ω : F) ≤ c
this :
  Eq (α := Ω → G) μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) | m]
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
n : ℕ
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (z : F × E) ↦
    (((B : (a : F) → E →L[ℝ] G) z.1 : E →L[ℝ] G) : (a : E) → G) z.2

Tactic:
fun_prop
-- 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Ω
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this_1 : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), norm.{u_3} (E := F) ((fs n : (a : Ω) → F) ω : F) ≤ c
this :
  Eq (α := Ω → G) μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) | m]
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
n : ℕ
⊢ StronglyMeasurable.{u_1, u_4} (α := Ω) (β := G)
    ((fun (n : ℕ) (ω : Ω) ↦
        ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
      n)

Tactic:
exact Continuous.comp_stronglyMeasurable (g := (fun z : F × E ↦ B z.1 z.2)) (by fun_prop)
        ((fs n).stronglyMeasurable.prodMk stronglyMeasurable_condExp)

Premises used: Continuous.comp_stronglyMeasurable, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.prodMk, MeasureTheory.SimpleFunc.stronglyMeasurable
-- 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Ω
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this_1 : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), norm.{u_3} (E := F) ((fs n : (a : Ω) → F) ω : F) ≤ c
this :
  Eq (α := Ω → G) μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) | m]
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
n : ℕ
⊢ Integrable.{u_4, u_1} (ε := G)
    ((fun (n : ℕ) (ω : Ω) ↦
        ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
      n)
    μ

Tactic:
B.integrable_of_bilin_of_bdd_left c
      ((fs n).stronglyMeasurable.mono hm).aestronglyMeasurable (ae_of_all _ <| hfs_bound n)
      integrable_condExp

Premises used: ContinuousLinearMap.integrable_of_bilin_of_bdd_left, MeasureTheory.integrable_condExp, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.ae_of_all, MeasureTheory.StronglyMeasurable.mono, MeasureTheory.SimpleFunc.stronglyMeasurable
-- 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Ω
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this_1 : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), norm.{u_3} (E := F) ((fs n : (a : Ω) → F) ω : F) ≤ c
this :
  Eq (α := Ω → G) μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) | m]
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
n : ℕ
⊢ Integrable.{u_4, u_1} (ε := G)
    ((fun (n : ℕ) (ω : Ω) ↦
        ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
      n)
    μ

Tactic:
exact B.integrable_of_bilin_of_bdd_left c
      ((fs n).stronglyMeasurable.mono hm).aestronglyMeasurable (ae_of_all _ <| hfs_bound n)
      integrable_condExp

Premises used: ContinuousLinearMap.integrable_of_bilin_of_bdd_left, MeasureTheory.integrable_condExp, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.ae_of_all, MeasureTheory.StronglyMeasurable.mono, MeasureTheory.SimpleFunc.stronglyMeasurable
-- 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Ω
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
h :
  EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]

Tactic:
apply condExp_congr_ae

Premises used: MeasureTheory.condExp_congr_ae
-- 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Ω
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
a : Ω
ha : f a = AEStronglyMeasurable.mk f hf a
rw rw₁ :
  Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf a) : E →L[ℝ] G) : (a : E) → G) (g a) : G)
    ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf a) : E →L[ℝ] G) : (a : E) → G) (g a) : G)
⊢ Eq.{u_4 + 1} (α := G) ((((B : (a : F) → E →L[ℝ] G) (f a) : E →L[ℝ] G) : (a : E) → G) (g a) : G)
    ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf a) : E →L[ℝ] G) : (a : E) → G) (g a) : G)

Tactic:
rw [ha]
-- 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Ω
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ f x = AEStronglyMeasurable.mk f hf x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦
                  Eq.{u_4 + 1} (α := G)
                    ((fun (ω : Ω) ↦ ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)) x)
                    ((fun (ω : Ω) ↦
                        ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G)
                            (g ω) :
                          G))
                      x))
                x}
            x}
      a
h₁ h₂ :
  ∀ (a : Ω) (ha : f a = AEStronglyMeasurable.mk f hf a),
    Eq.{u_4 + 1} (α := G) ((((B : (a : F) → E →L[ℝ] G) (f a) : E →L[ℝ] G) : (a : E) → G) (g a) : G)
      ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf a) : E →L[ℝ] G) : (a : E) → G) (g a) : G)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω)

Tactic:
filter_upwards [hf.ae_eq_mk] with a ha using by rw [ha]

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- 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Ω
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)

Tactic:
condExp_stronglyMeasurable_bilin_of_bound B hm hf.stronglyMeasurable_mk
      hg c ?_

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.condExp_stronglyMeasurable_bilin_of_bound
-- 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Ω
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
refine : ∀ᵐ (ω : Ω) ∂μ, ‖AEStronglyMeasurable.mk f hf ω‖ ≤ c
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)

Tactic:
refine condExp_stronglyMeasurable_bilin_of_bound B hm hf.stronglyMeasurable_mk
      hg c ?_

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.condExp_stronglyMeasurable_bilin_of_bound
-- 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Ω
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
h : ∀ (ω : Ω) (hω1 : ‖f ω‖ ≤ c) (hω2 : f ω = AEStronglyMeasurable.mk f hf ω), ‖AEStronglyMeasurable.mk f hf ω‖ ≤ c
⊢ ∀ᵐ (ω : Ω) ∂μ, ‖AEStronglyMeasurable.mk f hf ω‖ ≤ c

Tactic:
filter_upwards [hf_bound, hf.ae_eq_mk] with ω hω1 hω2

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- 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Ω
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
ω : Ω
hω1 : ‖f ω‖ ≤ c
hω2 : f ω = AEStronglyMeasurable.mk f hf ω
h h₁ h₂ h₃ : ‖f ω‖ ≤ c
⊢ ‖AEStronglyMeasurable.mk f hf ω‖ ≤ c

Tactic:
rwa [← hω2]
-- 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Ω
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
ω : Ω
hω : f ω = AEStronglyMeasurable.mk f hf ω
rw rw₁ :
  Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)
    ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)
⊢ Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)
    ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)

Tactic:
rw [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Ω
inst_8 : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ f x = AEStronglyMeasurable.mk f hf x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦
                  Eq.{u_4 + 1} (α := G)
                    ((fun (ω : Ω) ↦
                        ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G)
                            (μ[g | m] ω) :
                          G))
                      x)
                    ((fun (ω : Ω) ↦ ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
                      x))
                x}
            x}
      a
h₁ h₂ :
  ∀ (ω : Ω) (hω : f ω = AEStronglyMeasurable.mk f hf ω),
    Eq.{u_4 + 1} (α := G)
      ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)
      ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)

Tactic:
filter_upwards [hf.ae_eq_mk] with ω hω using by rw [hω]

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
pos :
  ∀ (hm : m ≤ mΩ),
    EventuallyEq.{u_1, u_4} (β := G) (ae μ)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
neg :
  ∀ (hm : ¬m ≤ mΩ),
    EventuallyEq.{u_1, u_4} (β := G) (ae μ)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)

Tactic:
by_cases hm : m ≤ mΩ
-- 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
hm : ¬m ≤ mΩ
⊢ ∀ (a : Ω),
    Eq.{u_4 + 1} (α := G) (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] a)
      ((fun (ω : Ω) ↦ ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)) a)

Tactic:
simp [condExp_of_not_le hm]

Premises used: MeasureTheory.condExp_of_not_le
-- 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
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
hm : ¬m ≤ mΩ
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)

Tactic:
exact ae_of_all _ <| by simp [condExp_of_not_le hm]

Premises used: MeasureTheory.ae_of_all