awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst : (t : T) → TopologicalSpace (F t)
inst_1 : (t : T) → MeasurableSpace (F t)
inst_2 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_3 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
inst_4 : TopologicalSpace G
inst_5 : MeasurableSpace G
inst_6 : BorelSpace G
inst_7 : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst_8 : Fintype T
inst_9 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
        (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
f : G →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
funProp : ∀ (i : T), Membership.mem (γ := Finset T) Finset.univ i → inst_1 i ≤ inst_1 i
⊢ Measurable (β := ℝ) fun (y : (j : T) → F j) ↦ ∏ j : T, (g j : (a : F j) → ℝ) (y j)
have funProp₁ : ∀ (i : T),
  Membership.mem (γ := Finset T) Finset.univ i → MeasurableEmbedding (β := ℝ) fun (a1 : F i) ↦ (g i : (a : F i) → ℝ) a1
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst : (t : T) → TopologicalSpace (F t)
inst_1 : (t : T) → MeasurableSpace (F t)
inst_2 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_3 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
inst_4 : TopologicalSpace G
inst_5 : MeasurableSpace G
inst_6 : BorelSpace G
inst_7 : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst_8 : Fintype T
inst_9 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
        (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
f : G →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
⊢ Measurable (β := ℝ) fun (p : G × ((j : T) → F j)) ↦
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j) : ℝ)
have funProp : inst_5 ≤ inst_5
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst : (t : T) → TopologicalSpace (F t)
inst_1 : (t : T) → MeasurableSpace (F t)
inst_2 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_3 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
inst_4 : TopologicalSpace G
inst_5 : MeasurableSpace G
inst_6 : BorelSpace G
inst_7 : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst_8 : Fintype T
inst_9 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
        (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
f : G →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
funProp : inst_5 ≤ inst_5
⊢ Measurable (β := ℝ) fun (p : G × ((j : T) → F j)) ↦
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j) : ℝ)
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (a0 : G) ↦ (f : (a : G) → ℝ) a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst : (t : T) → TopologicalSpace (F t)
inst_1 : (t : T) → MeasurableSpace (F t)
inst_2 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_3 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
inst_4 : TopologicalSpace G
inst_5 : MeasurableSpace G
inst_6 : BorelSpace G
inst_7 : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst_8 : Fintype T
inst_9 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
        (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
f : G →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
funProp : inst_5 ≤ inst_5
funProp₁ : MeasurableEmbedding (β := ℝ) fun (a0 : G) ↦ (f : (a : G) → ℝ) a0
⊢ Measurable (β := ℝ) fun (p : G × ((j : T) → F j)) ↦
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j) : ℝ)
have funProp₂ : ∀ (i : T), Membership.mem (γ := Finset T) Finset.univ i → inst_1 i ≤ inst_1 i
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst : (t : T) → TopologicalSpace (F t)
inst_1 : (t : T) → MeasurableSpace (F t)
inst_2 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_3 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
inst_4 : TopologicalSpace G
inst_5 : MeasurableSpace G
inst_6 : BorelSpace G
inst_7 : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst_8 : Fintype T
inst_9 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
        (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
f : G →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
funProp : inst_5 ≤ inst_5
funProp₁ : MeasurableEmbedding (β := ℝ) fun (a0 : G) ↦ (f : (a : G) → ℝ) a0
funProp₂ : ∀ (i : T), Membership.mem (γ := Finset T) Finset.univ i → inst_1 i ≤ inst_1 i
⊢ Measurable (β := ℝ) fun (p : G × ((j : T) → F j)) ↦
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j) : ℝ)
have funProp₃ : ∀ (i : T),
  Membership.mem (γ := Finset T) Finset.univ i → MeasurableEmbedding (β := ℝ) fun (a1 : F i) ↦ (g i : (a : F i) → ℝ) a1
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst : (t : T) → TopologicalSpace (F t)
inst_1 : (t : T) → MeasurableSpace (F t)
inst_2 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_3 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
inst_4 : TopologicalSpace G
inst_5 : MeasurableSpace G
inst_6 : BorelSpace G
inst_7 : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst_8 : IsFiniteMeasure P
inst_9 : Finite T
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : ((t : T) → F t) →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z ω) : ℝ)
              ((g : (a : (t : T) → F t) → ℝ) fun (x : T) ↦ Y x ω : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
        (∫ (x : Ω), (fun (ω : Ω) ↦ ((g : (a : (t : T) → F t) → ℝ) fun (x : T) ↦ Y x ω : ℝ)) x ∂P)
⊢ Z ⟂ᵢ[P] fun (ω : Ω) (t : T) ↦ Y t ω
have have : ∀ (this : Fintype T), Z ⟂ᵢ[P] fun (ω : Ω) (t : T) ↦ Y t ω
Tactic: have := Fintype.ofFinite T
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst : (t : T) → TopologicalSpace (F t)
inst_1 : (t : T) → MeasurableSpace (F t)
inst_2 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_3 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
inst_4 : TopologicalSpace G
inst_5 : MeasurableSpace G
inst_6 : BorelSpace G
inst_7 : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst_8 : IsFiniteMeasure P
inst_9 : Finite T
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : ((t : T) → F t) →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z ω) : ℝ)
              ((g : (a : (t : T) → F t) → ℝ) fun (x : T) ↦ Y x ω : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
        (∫ (x : Ω), (fun (ω : Ω) ↦ ((g : (a : (t : T) → F t) → ℝ) fun (x : T) ↦ Y x ω : ℝ)) x ∂P)
this : Fintype T
⊢ Z ⟂ᵢ[P] fun (ω : Ω) (t : T) ↦ Y t ω
have refine : ∀ (f : G →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
  ∫ (x : Ω),
      HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
      (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
Tactic: refine indepFun_pi_of_prod_bcf mZ mY fun f g ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst : (t : T) → TopologicalSpace (F t)
inst_1 : (t : T) → MeasurableSpace (F t)
inst_2 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_3 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
inst_4 : TopologicalSpace G
inst_5 : MeasurableSpace G
inst_6 : BorelSpace G
inst_7 : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst_8 : IsFiniteMeasure P
inst_9 : Finite T
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : ((t : T) → F t) →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z ω) : ℝ)
              ((g : (a : (t : T) → F t) → ℝ) fun (x : T) ↦ Y x ω : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
        (∫ (x : Ω), (fun (ω : Ω) ↦ ((g : (a : (t : T) → F t) → ℝ) fun (x : T) ↦ Y x ω : ℝ)) x ∂P)
this : Fintype T
f : G →ᵇ ℝ
g : (t : T) → F t →ᵇ ℝ
⊢ ∫ (x : Ω),
      HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
      (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
have h₁ : ∀ (x x : Ω),
  HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x =
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z x) : ℝ)
      ((∏ t : T, (g t).compContinuous { toFun := Function.eval (β := F) t, continuous_toFun := sorry } :
            (a : (t : T) → F t) → ℝ)
          fun (x_1 : T) ↦ Y x_1 x :
        ℝ)
Tactic: convert! h f (∏ t, (g t).compContinuous ⟨Function.eval t, by fun_prop⟩)
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst : (t : T) → TopologicalSpace (F t)
inst_1 : (t : T) → MeasurableSpace (F t)
inst_2 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_3 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
inst_4 : TopologicalSpace G
inst_5 : MeasurableSpace G
inst_6 : BorelSpace G
inst_7 : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst_8 : IsFiniteMeasure P
inst_9 : Finite T
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : ((t : T) → F t) →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z ω) : ℝ)
              ((g : (a : (t : T) → F t) → ℝ) fun (x : T) ↦ Y x ω : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
        (∫ (x : Ω), (fun (ω : Ω) ↦ ((g : (a : (t : T) → F t) → ℝ) fun (x : T) ↦ Y x ω : ℝ)) x ∂P)
this : Fintype T
f : G →ᵇ ℝ
g : (t : T) → F t →ᵇ ℝ
h₁ :
  ∀ (x x : Ω),
    HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x =
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z x) : ℝ)
        ((∏ t : T, (g t).compContinuous { toFun := Function.eval (β := F) t, continuous_toFun := ⋯ } :
              (a : (t : T) → F t) → ℝ)
            fun (x_1 : T) ↦ Y x_1 x :
          ℝ)
⊢ ∫ (x : Ω),
      HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
      (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
have h₂ : ∀ (x x : Ω),
  Eq (α := ℝ) ((∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x : ℝ)
    ((∏ t : T, (g t).compContinuous { toFun := Function.eval (β := F) t, continuous_toFun := sorry } :
          (a : (t : T) → F t) → ℝ)
        fun (x_1 : T) ↦ Y x_1 x :
      ℝ)
Tactic: convert! h f (∏ t, (g t).compContinuous ⟨Function.eval t, by fun_prop⟩)
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : Fintype S
inst_9 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
⊢ (fun (ω : Ω) (s : S) ↦ X s ω) ⟂ᵢ[P] U
have rw : Eq (α := Measure (((a : S) → E a) × H)) (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, U ω)) P)
  (Measure.prod (map (fun (c : Ω) (a : S) ↦ X a c) P) (map U P))
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map (aemeasurable_pi_lambda _ mX) mU]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : Fintype S
inst_9 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
⊢ Eq (α := Measure (((a : S) → E a) × H)) (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, U ω)) P)
    (Measure.prod (map (fun (c : Ω) (a : S) ↦ X a c) P) (map U P))
have refine : ∀ (f : (i : S) → E i →ᵇ ℝ) (g : H →ᵇ ℝ),
  (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, U ω)) P)
      fun (p : ((i : S) → E i) × H) ↦
      HMul.hMul (α := ℝ) (β := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i) : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ (MeasurableSpace.pi (X := E)) (map (fun (c : Ω) (a : S) ↦ X a c) P) fun (x : (i : S) → E i) ↦
        ∏ i : S, (f i : (a : E i) → ℝ) (x i))
      (@integral _ _ _ _ inst_5 (map U P) fun (t : H) ↦ (g : (a : H) → ℝ) t)
Tactic: refine eq_prod_of_integral_prod_mul_boundedContinuousFunction fun f g ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : Fintype S
inst_9 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, U ω)) P)
      fun (p : ((i : S) → E i) × H) ↦
      HMul.hMul (α := ℝ) (β := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i) : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ (MeasurableSpace.pi (X := E)) (map (fun (c : Ω) (a : S) ↦ X a c) P) fun (x : (i : S) → E i) ↦
        ∏ i : S, (f i : (a : E i) → ℝ) (x i))
      (@integral _ _ _ _ inst_5 (map U P) fun (t : H) ↦ (g : (a : H) → ℝ) t)
have rw : ∫ (x : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x, U x).1 i) : ℝ)
      ((g : (a : H) → ℝ) (fun (a : S) ↦ X a x, U x).2 : ℝ) ∂P =
  HMul.hMul (α := ℝ) (∫ (x : Ω), ∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x) i) ∂P)
    (∫ (x : Ω), (g : (a : H) → ℝ) (U x) ∂P)
Tactic: rw [integral_map, integral_map, integral_map]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : Fintype S
inst_9 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
rw :
  ∫ (x : Ω),
      HMul.hMul (α := ℝ) (β := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x, U x).1 i) : ℝ)
        ((g : (a : H) → ℝ) (fun (a : S) ↦ X a x, U x).2 : ℝ) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), ∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x) i) ∂P)
      (∫ (x : Ω), (g : (a : H) → ℝ) (U x) ∂P)
hφ : AEMeasurable U P
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, U ω)) P)
      fun (p : ((i : S) → E i) × H) ↦
      HMul.hMul (α := ℝ) (β := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i) : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ (MeasurableSpace.pi (X := E)) (map (fun (c : Ω) (a : S) ↦ X a c) P) fun (x : (i : S) → E i) ↦
        ∏ i : S, (f i : (a : E i) → ℝ) (x i))
      (@integral _ _ _ _ inst_5 (map U P) fun (t : H) ↦ (g : (a : H) → ℝ) t)
have hfm : AEStronglyMeasurable (β := ℝ) (m₀ := inst_5) (⇑g : (a : H) → ℝ) (map U P)
Tactic: rw [integral_map, integral_map, integral_map]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : Fintype S
inst_9 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
rw :
  ∫ (x : Ω),
      HMul.hMul (α := ℝ) (β := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x, U x).1 i) : ℝ)
        ((g : (a : H) → ℝ) (fun (a : S) ↦ X a x, U x).2 : ℝ) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), ∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x) i) ∂P)
      (∫ (x : Ω), (g : (a : H) → ℝ) (U x) ∂P)
hφ : AEMeasurable U P
hfm : AEStronglyMeasurable (β := ℝ) (m₀ := inst_5) (⇑g : (a : H) → ℝ) (map U P)
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, U ω)) P)
      fun (p : ((i : S) → E i) × H) ↦
      HMul.hMul (α := ℝ) (β := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i) : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ (MeasurableSpace.pi (X := E)) (map (fun (c : Ω) (a : S) ↦ X a c) P) fun (x : (i : S) → E i) ↦
        ∏ i : S, (f i : (a : E i) → ℝ) (x i))
      (@integral _ _ _ _ inst_5 (map U P) fun (t : H) ↦ (g : (a : H) → ℝ) t)
have hφ₁ : AEMeasurable (β := (i : S) → E i) (fun (c : Ω) (a : S) ↦ X a c) P
Tactic: rw [integral_map, integral_map, integral_map]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst_8 : Fintype S
inst_9 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
rw :
  ∫ (x : Ω),
      HMul.hMul (α := ℝ) (β := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x, U x).1 i) : ℝ)
        ((g : (a : H) → ℝ) (fun (a : S) ↦ X a x, U x).2 : ℝ) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), ∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x) i) ∂P)
      (∫ (x : Ω), (g : (a : H) → ℝ) (U x) ∂P)
hφ : AEMeasurable U P
hfm : AEStronglyMeasurable (β := ℝ) (m₀ := inst_5) (⇑g : (a : H) → ℝ) (map U P)
hφ₁ : AEMeasurable (β := (i : S) → E i) (fun (c : Ω) (a : S) ↦ X a c) P
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, U ω)) P)
      fun (p : ((i : S) → E i) × H) ↦
      HMul.hMul (α := ℝ) (β := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i) : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ (MeasurableSpace.pi (X := E)) (map (fun (c : Ω) (a : S) ↦ X a c) P) fun (x : (i : S) → E i) ↦
        ∏ i : S, (f i : (a : E i) → ℝ) (x i))
      (@integral _ _ _ _ inst_5 (map U P) fun (t : H) ↦ (g : (a : H) → ℝ) t)
have hfm₁ : AEStronglyMeasurable (β := ℝ) (m₀ := MeasurableSpace.pi (X := E))
  (fun (x : (i : S) → E i) ↦ ∏ i : S, (f i : (a : E i) → ℝ) (x i)) (map (fun (c : Ω) (a : S) ↦ X a c) P)
Tactic: rw [integral_map, integral_map, integral_map]