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
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Ω
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
this : IsFiniteMeasure (μ.restrict (sets n))
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae (μ.restrict (sets n)))
    (μ.restrict (sets n))[fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) ((sets n).indicator f ω) : E →L[ℝ] G) : (a : E) → G) ((μ.restrict (sets n))[g | m] ω)
have pos : ∀ᵐ (ω : Ω) ∂μ.restrict (sets n), ‖(sets n).indicator f ω‖ ≤ (↑n : ℝ)
Tactic: refine condExp_stronglyMeasurable_bilin_of_bound B hm (hf.indicator (h_meas n))
    hg.integrableOn n ?_
-- 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
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Ω
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
this : IsFiniteMeasure (μ.restrict (sets n))
⊢ ∀ᵐ (ω : Ω) ∂μ.restrict (sets n), ‖(sets n).indicator f ω‖ ≤ (↑n : ℝ)
have pos : ∀ (ω : Ω), ‖(sets n).indicator f ω‖ ≤ (↑n : ℝ)
Tactic: filter_upwards with ω
-- 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
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Ω
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
this : IsFiniteMeasure (μ.restrict (sets n))
ω : Ω
⊢ ‖(sets n).indicator f ω‖ ≤ (↑n : ℝ)
have pos : ∀ (hωs : ω ∈ sets n), ‖(sets n).indicator f ω‖ ≤ (↑n : ℝ)
Tactic: by_cases hωs : ω ∈ sets n
-- 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
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Ω
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
n : ℕ
this : IsFiniteMeasure (μ.restrict (sets n))
ω : Ω
pos : ∀ (hωs : ω ∈ sets n), ‖(sets n).indicator f ω‖ ≤ (↑n : ℝ)
⊢ ‖(sets n).indicator f ω‖ ≤ (↑n : ℝ)
have neg : ∀ (hωs : ω ∉ sets n), ‖(sets n).indicator f ω‖ ≤ (↑n : ℝ)
Tactic: by_cases hωs : ω ∈ sets n
-- 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 F
f : Ω → F
g : Ω → E
hg : StronglyMeasurable g
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hf : Integrable 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 | m] ω) : E →L[ℝ] G) : (a : E) → G) (g ω)
have simp_rw : EventuallyEq.{u_1, u_4} (β := G) (ae μ)
  μ[fun (ω : Ω) ↦ (((B.flip : (a : E) → F →L[ℝ] G) (g ω) : F →L[ℝ] G) : (a : F) → G) (f ω) | m] fun (ω : Ω) ↦
  (((B.flip : (a : E) → F →L[ℝ] G) (g ω) : F →L[ℝ] G) : (a : F) → G) (μ[f | m] ω)
Tactic: simp_rw [← B.flip_apply] at hfg ⊢
-- 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
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable 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 μ
⊢ 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]
have 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 ω)
Tactic: apply condExp_congr_ae
-- 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
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable 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 μ
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)
have 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)
Tactic: rw [ha]
-- 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
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable 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 μ
⊢ 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 ω)
have 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
Tactic: filter_upwards [hf.ae_eq_mk] with a ha using by rw [ha]
-- 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
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable 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 μ
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
⊢ 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 ω)
have h₁ : ∀ (a : Ω),
  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)
Tactic: filter_upwards [hf.ae_eq_mk] with a ha using by rw [ha]
-- 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
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable 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 μ
⊢ 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] ω)
have refine : 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: refine condExp_bilin_of_stronglyMeasurable_left B hf.stronglyMeasurable_mk
      ((integrable_congr ?_).mp hfg) hg
-- 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
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable 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 μ
ω : Ω
hω : f ω = AEStronglyMeasurable.mk f hf ω
⊢ Eq.{u_4 + 1} (α := G) ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)
    ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)
have rw : Eq.{u_4 + 1} (α := G)
  ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)
  ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)
Tactic: rw [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
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable 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 μ
⊢ 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 ω)
have 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
Tactic: filter_upwards [hf.ae_eq_mk] with ω hω using by rw [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
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable 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 μ
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
⊢ 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 ω)
have h₁ : ∀ (a : Ω),
  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)
Tactic: filter_upwards [hf.ae_eq_mk] with ω hω using by rw [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
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable 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 μ
a : Ω
ha : f a = AEStronglyMeasurable.mk f hf a
⊢ Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf a) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] a) : G)
    ((((B : (a : F) → E →L[ℝ] G) (f a) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] a) : G)
have rw : Eq.{u_4 + 1} (α := G)
  ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf a) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] a) : G)
  ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf a) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] a) : G)
Tactic: rw [ha]
-- 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
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable 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 μ
⊢ 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] ω)
have 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
Tactic: filter_upwards [hf.ae_eq_mk] with a ha using by rw [ha]
-- 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
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable 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 μ
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
⊢ 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] ω)
have h₁ : ∀ (a : Ω),
  f a = AEStronglyMeasurable.mk f hf a →
    Eq.{u_4 + 1} (α := G)
      ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf a) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] a) : G)
      ((((B : (a : F) → E →L[ℝ] G) (f a) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] a) : G)
Tactic: filter_upwards [hf.ae_eq_mk] with a ha using by rw [ha]
-- 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 F
f : Ω → F
g : Ω → E
hg : AEStronglyMeasurable g μ
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hf : Integrable 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 | m] ω) : E →L[ℝ] G) : (a : E) → G) (g ω)
have simp_rw : EventuallyEq.{u_1, u_4} (β := G) (ae μ)
  μ[fun (ω : Ω) ↦ (((B.flip : (a : E) → F →L[ℝ] G) (g ω) : F →L[ℝ] G) : (a : F) → G) (f ω) | m] fun (ω : Ω) ↦
  (((B.flip : (a : E) → F →L[ℝ] G) (g ω) : F →L[ℝ] G) : (a : F) → G) (μ[f | m] ω)
Tactic: simp_rw [← B.flip_apply] at hfg ⊢
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (hypothesis)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
⊢ SigmaFinite (ν.trim ⋯)
have hσ₁ : SigmaFinite (m0 := m𝓨) (Measure.map g (ν.trim sorry))
Tactic: rw [← map_trim_comap hg] at hσ
Cleared hypotheses: hσ