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] ω)
h :
  ∀ (ω : Ω) (hω : Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))),
    Tendsto.{0, u_4} (β := G)
      (fun (n : ℕ) ↦ ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)) atTop
      (𝓝 ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) : Filter G)
⊢ ∀ᵐ (x : Ω) ∂μ,
    Tendsto.{0, u_4} (β := G)
      (fun (n : ℕ) ↦
        (fun (n : ℕ) (ω : Ω) ↦
            ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G))
          n x)
      atTop (𝓝 ((fun (ω : Ω) ↦ ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)) x))

Tactic:
filter_upwards [hfs_tendsto] with ω 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 : 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] ω)
ω : Ω
hω : Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (x : F) ↦ (((B : (a : F) → E →L[ℝ] G) x : E →L[ℝ] G) : (a : E) → G) (g ω)

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] ω)
ω : Ω
hω : Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))
⊢ Tendsto.{0, u_4} (β := G)
    (fun (n : ℕ) ↦ ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)) atTop
    (𝓝 ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) : Filter G)

Tactic:
exact ((by fun_prop : Continuous (fun x ↦ B x (g ω))).tendsto (f ω)).comp hω

Premises used: Continuous.tendsto, Filter.Tendsto.comp
-- 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] ω)
h :
  ∀ (ω : Ω) (hω : Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))),
    Tendsto.{0, u_4} (β := G)
      (fun (n : ℕ) ↦
        ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
      atTop (𝓝 ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)) : Filter G)
⊢ ∀ᵐ (x : Ω) ∂μ,
    Tendsto.{0, u_4} (β := G)
      (fun (n : ℕ) ↦
        (fun (n : ℕ) (ω : Ω) ↦
            ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
          n x)
      atTop (𝓝 ((fun (ω : Ω) ↦ ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)) x))

Tactic:
filter_upwards [hfs_tendsto] with ω 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 : 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] ω)
ω : Ω
hω : Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (x : F) ↦ (((B : (a : F) → E →L[ℝ] G) x : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)

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] ω)
ω : Ω
hω : Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))
⊢ Tendsto.{0, u_4} (β := G)
    (fun (n : ℕ) ↦ ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
    atTop (𝓝 ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)) : Filter G)

Tactic:
exact ((by fun_prop : Continuous (fun x ↦ B x (μ[g | m] ω))).tendsto (f ω)).comp hω

Premises used: Continuous.tendsto, Filter.Tendsto.comp
-- 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] ω)
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ ‖B‖ * c * ‖g x‖) μ

Tactic:
hg.norm.const_mul _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.norm
-- 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] ω)
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ ‖B‖ * c * ‖g x‖) μ

Tactic:
exact hg.norm.const_mul _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.norm
-- 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] ω)
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ ‖B‖ * c * ‖μ[g | m] x‖) μ

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 : ℕ),
    ∀ᵐ (x : Ω) ∂μ,
      norm.{u_4} (E := G)
          ((fun (n : ℕ) (ω : Ω) ↦
              ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G))
            n x) ≤
        (fun (x : Ω) ↦ ‖B‖ * c * ‖g x‖) x

Tactic:
fun n ↦ Eventually.of_forall fun _ ↦ ?_

Premises used: Filter.Eventually.of_forall
-- 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] ω)
neg :
  ∀ (n : ℕ) (x : Ω),
    norm.{u_4} (E := G)
        ((fun (n : ℕ) (ω : Ω) ↦
            ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G))
          n x) ≤
      (fun (x : Ω) ↦ ‖B‖ * c * ‖g x‖) x
⊢ ∀ (n : ℕ),
    ∀ᵐ (x : Ω) ∂μ,
      norm.{u_4} (E := G)
          ((fun (n : ℕ) (ω : Ω) ↦
              ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G))
            n x) ≤
        (fun (x : Ω) ↦ ‖B‖ * c * ‖g x‖) x

Tactic:
refine fun n ↦ Eventually.of_forall fun _ ↦ ?_

Premises used: Filter.Eventually.of_forall
-- 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 : ℕ
x : Ω
neg : ‖B‖ * norm.{u_3} (E := F) ((fs n : (a : Ω) → F) x : F) * ‖g x‖ ≤ (fun (x : Ω) ↦ ‖B‖ * c * ‖g x‖) x
neg₁ neg₂ : ‖B‖ * c * ‖g x‖ ≤ ‖B‖ * c * ‖g x‖
⊢ norm.{u_4} (E := G)
      ((fun (n : ℕ) (ω : Ω) ↦
          ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G))
        n x) ≤
    (fun (x : Ω) ↦ ‖B‖ * c * ‖g x‖) x

Tactic:
grw [B.le_opNorm₂, hfs_bound]

Premises used: ContinuousLinearMap.le_opNorm₂
-- 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 : ℕ),
    ∀ᵐ (x : Ω) ∂μ,
      norm.{u_4} (E := G)
          ((fun (n : ℕ) (ω : Ω) ↦
              ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
            n x) ≤
        (fun (x : Ω) ↦ ‖B‖ * c * ‖μ[g | m] x‖) x

Tactic:
fun n ↦ Eventually.of_forall fun _ ↦ ?_

Premises used: Filter.Eventually.of_forall
-- 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] ω)
neg :
  ∀ (n : ℕ) (x : Ω),
    norm.{u_4} (E := G)
        ((fun (n : ℕ) (ω : Ω) ↦
            ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
          n x) ≤
      (fun (x : Ω) ↦ ‖B‖ * c * ‖μ[g | m] x‖) x
⊢ ∀ (n : ℕ),
    ∀ᵐ (x : Ω) ∂μ,
      norm.{u_4} (E := G)
          ((fun (n : ℕ) (ω : Ω) ↦
              ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
            n x) ≤
        (fun (x : Ω) ↦ ‖B‖ * c * ‖μ[g | m] x‖) x

Tactic:
refine fun n ↦ Eventually.of_forall fun _ ↦ ?_

Premises used: Filter.Eventually.of_forall
-- 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 : ℕ
x : Ω
neg : ‖B‖ * norm.{u_3} (E := F) ((fs n : (a : Ω) → F) x : F) * ‖μ[g | m] x‖ ≤ (fun (x : Ω) ↦ ‖B‖ * c * ‖μ[g | m] x‖) x
neg₁ neg₂ : ‖B‖ * c * ‖μ[g | m] x‖ ≤ ‖B‖ * c * ‖μ[g | m] x‖
⊢ norm.{u_4} (E := G)
      ((fun (n : ℕ) (ω : Ω) ↦
          ((((B : (a : F) → E →L[ℝ] G) ((fs n : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
        n x) ≤
    (fun (x : Ω) ↦ ‖B‖ * c * ‖μ[g | m] x‖) x

Tactic:
grw [B.le_opNorm₂, hfs_bound]

Premises used: ContinuousLinearMap.le_opNorm₂
-- 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 : ℕ
⊢ 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:
(condExp_stronglyMeasurable_simpleFunc_bilin B hm _ hg).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_stronglyMeasurable_simpleFunc_bilin