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
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Ω
pos :
  ∀ (hμm : SigmaFinite (μ.trim hm)),
    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 :
  ∀ (hμm : ¬SigmaFinite (μ.trim hm)),
    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 hμm : SigmaFinite (μ.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- 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Ω
hμm : ¬SigmaFinite (μ.trim hm)
⊢ ∀ (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_sigmaFinite hm hμm]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite
-- 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Ω
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 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_sigmaFinite hm hμm]

Premises used: MeasureTheory.ae_of_all
-- 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Ω
hμm : SigmaFinite (μ.trim hm)
pos :
  ∀ (sets : ℕ → Set Ω)
    (sets_prop :
      ∀ (n : ℕ),
        MeasurableSet (sets n) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ sets n, ‖f x‖ ≤ (↑n : ℝ))
    (h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ),
    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:
obtain ⟨sets, sets_prop, h_univ⟩ := hf.exists_spanning_measurableSet_norm_le hm μ

Premises used: Filter.sets, MeasureTheory.StronglyMeasurable.exists_spanning_measurableSet_norm_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Ω
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
sets_prop :
  ∀ (n : ℕ),
    MeasurableSet (sets n) ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ sets n, ‖f x‖ ≤ (↑n : ℝ)
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
⊢ (∀ (x : ℕ), MeasurableSet (sets x)) ∧
    (∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)) ∧
      ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)

Tactic:
simp_rw [forall_and] at sets_prop

Premises used: forall_and
-- 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Ω
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : Eq.{u_1 + 1} (α := Set Ω) (⋃ (i : ℕ), sets i) Set.univ
sets_prop :
  (∀ (x : ℕ), MeasurableSet (sets x)) ∧
    (∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)) ∧
      ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
⊢ ∀ (x : ℕ), MeasurableSet (sets x)

Tactic:
obtain ⟨h_meas, h_finite, h_norm⟩ := sets_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
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
sets_prop :
  (∀ (x : ℕ), MeasurableSet (sets x)) ∧
    (∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)) ∧
      ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
⊢ ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
obtain ⟨h_meas, h_finite, h_norm⟩ := sets_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
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
sets_prop :
  (∀ (x : ℕ), MeasurableSet (sets x)) ∧
    (∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)) ∧
      ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (sets x) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ (↑x : ℝ)

Tactic:
obtain ⟨h_meas, h_finite, h_norm⟩ := sets_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
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 : ℝ)
this :
  ∀ (n : ℕ),
    ∀ᵐ (ω : Ω) ∂μ,
      ω ∈ sets n →
        Eq.{u_4 + 1} (α := G)
          (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ (i : ℕ),
      a ∈ sets i →
        Eq.{u_4 + 1} (α := G)
          (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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:
rw [← ae_all_iff] at this

Premises used: MeasureTheory.ae_all_iff
-- 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Ω
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 : ℝ)
this :
  ∀ᵐ (a : Ω) ∂μ,
    ∀ (i : ℕ),
      a ∈ sets i →
        Eq.{u_4 + 1} (α := G)
          (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
h :
  ∀ (ω : Ω)
    (hω :
      ∀ (i : ℕ),
        ω ∈ sets i →
          Eq.{u_4 + 1} (α := G)
            (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)),
    Eq.{u_4 + 1} (α := G)
      (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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) (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:
filter_upwards [this] 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
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 : ℝ)
this :
  ∀ᵐ (a : Ω) ∂μ,
    ∀ (i : ℕ),
      a ∈ sets i →
        Eq.{u_4 + 1} (α := G)
          (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
ω : Ω
hω :
  ∀ (i : ℕ),
    ω ∈ sets i →
      Eq.{u_4 + 1} (α := G)
        (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
rw : Membership.mem (γ := Set Ω) Set.univ ω
⊢ Membership.mem (γ := Set Ω) (⋃ (i : ℕ), sets i) ω

Tactic:
rw [h_univ]
-- 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Ω
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 : ℝ)
this :
  ∀ᵐ (a : Ω) ∂μ,
    ∀ (i : ℕ),
      a ∈ sets i →
        Eq.{u_4 + 1} (α := G)
          (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
ω : Ω
hω :
  ∀ (i : ℕ),
    ω ∈ sets i →
      Eq.{u_4 + 1} (α := G)
        (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
⊢ Membership.mem (γ := Set Ω) Set.univ ω

Tactic:
Set.mem_univ _

Premises used: Set.mem_univ
-- 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Ω
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 : ℝ)
this :
  ∀ᵐ (a : Ω) ∂μ,
    ∀ (i : ℕ),
      a ∈ sets i →
        Eq.{u_4 + 1} (α := G)
          (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
ω : Ω
hω :
  ∀ (i : ℕ),
    ω ∈ sets i →
      Eq.{u_4 + 1} (α := G)
        (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
⊢ Membership.mem (γ := Set Ω) Set.univ ω

Tactic:
exact Set.mem_univ _

Premises used: Set.mem_univ
-- 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Ω
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 : ℝ)
this :
  ∀ᵐ (a : Ω) ∂μ,
    ∀ (i : ℕ),
      a ∈ sets i →
        Eq.{u_4 + 1} (α := G)
          (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
ω : Ω
hω :
  ∀ (i : ℕ),
    ω ∈ sets i →
      Eq.{u_4 + 1} (α := G)
        (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
⊢ Membership.mem (γ := Set Ω) (⋃ (i : ℕ), sets i) ω

Tactic:
have h_mem : ω ∈ ⋃ i, sets i := by rw [h_univ]; exact Set.mem_univ _
-- 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Ω
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 : ℝ)
this :
  ∀ᵐ (a : Ω) ∂μ,
    ∀ (i : ℕ),
      a ∈ sets i →
        Eq.{u_4 + 1} (α := G)
          (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
ω : Ω
hω :
  ∀ (i : ℕ),
    ω ∈ sets i →
      Eq.{u_4 + 1} (α := G)
        (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
h_mem : Membership.mem (γ := Set Ω) (⋃ (i : ℕ), sets i) ω
⊢ ∃ (i : ℕ), ω ∈ sets i

Tactic:
simpa using h_mem
-- 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Ω
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 : ℝ)
this :
  ∀ᵐ (a : Ω) ∂μ,
    ∀ (i : ℕ),
      a ∈ sets i →
        Eq.{u_4 + 1} (α := G)
          (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
ω : Ω
hω h :
  ∀ (i : ℕ) (hi : ω ∈ sets i),
    Eq.{u_4 + 1} (α := G)
      (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
⊢ Eq.{u_4 + 1} (α := G) (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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:
obtain ⟨i, hi⟩ : ∃ i, ω ∈ sets i := by
      have h_mem : ω ∈ ⋃ i, sets i := by rw [h_univ]; exact Set.mem_univ _
      simpa using h_mem
-- 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Ω
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 : ℝ)
this :
  ∀ᵐ (a : Ω) ∂μ,
    ∀ (i : ℕ),
      a ∈ sets i →
        Eq.{u_4 + 1} (α := G)
          (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
ω : Ω
hω :
  ∀ (i : ℕ),
    ω ∈ sets i →
      Eq.{u_4 + 1} (α := G)
        (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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)
i : ℕ
hi : ω ∈ sets i
⊢ Eq.{u_4 + 1} (α := G) (μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : 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:
hω i hi