awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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 ω))
g₁ g₂ : SimpleFunc Ω F
h :
  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₂
h_add : (⇑(g₁ + g₂) : (a : Ω) → F) = HAdd.hAdd (α := (a : Ω) → F) (⇑g₁ : (a : Ω) → F) (⇑g₂ : (a : Ω) → F)
⊢ μ[fun (ω : Ω) ↦
      (HAdd.hAdd (α := E →L[ℝ] G) (β := E →L[ℝ] G) ((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G)
            ((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) :
          (a : E) → G)
        (g ω) |
      m] =ᶠ[ae μ]
    HAdd.hAdd (α := Ω → G)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
have obtain : ∀ (C₁ : ℝ) (hC₁ : ∀ (x : Ω), norm.{u_3} (E := F) ((g₁ : (a : Ω) → F) x : F) ≤ C₁),
  μ[fun (ω : Ω) ↦
      (HAdd.hAdd (α := E →L[ℝ] G) (β := E →L[ℝ] G) ((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G)
            ((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) :
          (a : E) → G)
        (g ω) |
      m] =ᶠ[ae μ]
    HAdd.hAdd (α := Ω → G)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
Tactic: obtain ⟨C₁, hC₁⟩ := @SimpleFunc.exists_forall_norm_le _ _ m _ g₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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 ω))
g₁ g₂ : SimpleFunc Ω F
h :
  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₂
h_add : (⇑(g₁ + g₂) : (a : Ω) → F) = HAdd.hAdd (α := (a : Ω) → F) (⇑g₁ : (a : Ω) → F) (⇑g₂ : (a : Ω) → F)
C₁ : ℝ
hC₁ : ∀ (x : Ω), norm.{u_3} (E := F) ((g₁ : (a : Ω) → F) x : F) ≤ C₁
⊢ μ[fun (ω : Ω) ↦
      (HAdd.hAdd (α := E →L[ℝ] G) (β := E →L[ℝ] G) ((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G)
            ((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) :
          (a : E) → G)
        (g ω) |
      m] =ᶠ[ae μ]
    HAdd.hAdd (α := Ω → G)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
have obtain : ∀ (C₂ : ℝ) (hC₂ : ∀ (x : Ω), norm.{u_3} (E := F) ((g₂ : (a : Ω) → F) x : F) ≤ C₂),
  μ[fun (ω : Ω) ↦
      (HAdd.hAdd (α := E →L[ℝ] G) (β := E →L[ℝ] G) ((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G)
            ((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) :
          (a : E) → G)
        (g ω) |
      m] =ᶠ[ae μ]
    HAdd.hAdd (α := Ω → G)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
Tactic: obtain ⟨C₂, hC₂⟩ := @SimpleFunc.exists_forall_norm_le _ _ m _ g₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (hypothesis)
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
⊢ 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] ω)
have hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (x : ℕ) ↦ (fs x : (a : Ω) → F) ω) atTop (𝓝 (f ω))
Tactic: have hfs_tendsto : ∀ᵐ ω ∂μ, Tendsto (fs · ω) atTop (𝓝 (f ω)) :=
    hf.tendsto_approxBounded_ae hf_bound
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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 ω))
⊢ 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] ω)
have pos : ∀ (hμ : μ = 0),
  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 hμ : μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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 ω))
pos :
  ∀ (hμ : μ = 0),
    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] ω)
have neg : ∀ (hμ : ¬μ = 0),
  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 hμ : μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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
⊢ 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] ω)
have pos : EventuallyEq.{u_1, u_4} (β := G) ⊥
  (condExp m (m₀ := mΩ) 0 fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω))
  fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (condExp m (m₀ := mΩ) 0 g ω)
Tactic: simp only [hμ, ae_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (hypothesis)
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
⊢ 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] ω)
have this : (ae μ).NeBot
Tactic: have : (ae μ).NeBot := ae_neBot.2 hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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 : (ae μ).NeBot
⊢ 0 ≤ c
have rcases : ∀ (w : Ω) (h : ‖f w‖ ≤ c), 0 ≤ c
Tactic: rcases hf_bound.exists with ⟨_, h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (hypothesis)
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 : (ae μ).NeBot
⊢ 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] ω)
have hc : 0 ≤ c
Tactic: have hc : 0 ≤ c := by
    rcases hf_bound.exists with ⟨_, h⟩
    exact (norm_nonneg _).trans h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (hypothesis)
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 : (ae μ).NeBot
hc : 0 ≤ c
⊢ 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] ω)
have hfs_bound : ∀ (n : ℕ) (ω : Ω), norm.{u_3} (E := F) ((fs n : (a : Ω) → F) ω : F) ≤ c
Tactic: have hfs_bound : ∀ n ω, ‖fs n ω‖ ≤ c := hf.norm_approxBounded_le hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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 : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), norm.{u_3} (E := F) ((fs n : (a : Ω) → F) ω : F) ≤ c
⊢ 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] ω)
have refine_1 : StronglyMeasurable.{u_1, u_4} (β := G) fun (ω : Ω) ↦
  (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
Tactic: refine condExp_of_stronglyMeasurable hm ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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 : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), norm.{u_3} (E := F) ((fs n : (a : Ω) → F) ω : F) ≤ c
refine_1 :
  StronglyMeasurable.{u_1, u_4} (β := G) fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
⊢ 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] ω)
have refine_2 : Integrable.{u_4, u_1} (ε := G)
  (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)) μ
Tactic: refine condExp_of_stronglyMeasurable hm ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (hypothesis)
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 : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), norm.{u_3} (E := F) ((fs n : (a : Ω) → F) ω : F) ≤ c
⊢ 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] ω)
have 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] ω)
Tactic: have : μ[fun ω ↦ B (f ω) (μ[g | m] ω) | m] = fun ω ↦ B (f ω) (μ[g | m] ω) := by
    refine condExp_of_stronglyMeasurable hm ?_ ?_
    · exact Continuous.comp_stronglyMeasurable (g := (fun z : F × E ↦ B z.1 z.2)) (by fun_prop)
        (hf.prodMk stronglyMeasurable_condExp)
    · exact B.integrable_of_bilin_of_bdd_left c (hf.mono hm).aestronglyMeasurable hf_bound
        integrable_condExp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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] ω)
⊢ 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] ω)
have neg : 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] ω) | m]
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut (goal)
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] ω)
⊢ 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] ω) | m]
have neg : ∀ (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 ω) : G))
      n)
    μ
Tactic: refine tendsto_condExp_unique (fun n ω ↦ B (fs n ω) (g ω))
    (fun n ω ↦ B (fs n ω) (μ[g | m] ω)) (fun ω ↦ B (f ω) (g ω))
    (fun ω ↦ B (f ω) (μ[g | m] ω)) ?_ ?_ ?_ ?_ (‖B‖ * c * ‖g ·‖) ?_ (‖B‖ * c * ‖(μ[g | m]) ·‖)
    ?_ ?_ ?_ ?_