awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
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 : (t : T) → TopologicalSpace (F t)
inst_5 : (t : T) → MeasurableSpace (F t)
inst_6 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_7 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst_8 : Fintype S
inst_9 : Fintype T
inst_10 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s)
          (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
f : (i : S) → E i →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, fun (a : T) ↦ Y a ω)) P)
      fun (p : ((i : S) → E i) × ((j : T) → F j)) ↦
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i)) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j))) =
    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 _ _ _ _ (MeasurableSpace.pi (X := F)) (map (fun (c : Ω) (a : T) ↦ Y a c) P) fun (y : (j : T) → F j) ↦
        ∏ j : T, (g j : (a : F j) → ℝ) (y j))
have rw : ∫ (x : Ω),
    HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).1 i))
      (∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).2 j)) ∂P =
  HMul.hMul (α := ℝ) (∫ (x : Ω), ∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x) i) ∂P)
    (∫ (x : Ω), ∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : T) ↦ Y a x) j) ∂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
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
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 : (t : T) → TopologicalSpace (F t)
inst_5 : (t : T) → MeasurableSpace (F t)
inst_6 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_7 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst_8 : Fintype S
inst_9 : Fintype T
inst_10 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s)
          (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
f : (i : S) → E i →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
rw :
  ∫ (x : Ω),
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).1 i))
        (∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).2 j)) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), ∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x) i) ∂P)
      (∫ (x : Ω), ∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : T) ↦ Y a x) j) ∂P)
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, fun (a : T) ↦ Y a ω)) P)
      fun (p : ((i : S) → E i) × ((j : T) → F j)) ↦
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i)) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j))) =
    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 _ _ _ _ (MeasurableSpace.pi (X := F)) (map (fun (c : Ω) (a : T) ↦ Y a c) P) fun (y : (j : T) → F j) ↦
        ∏ j : T, (g j : (a : F j) → ℝ) (y j))
have hφ : AEMeasurable (β := (j : T) → F j) (fun (c : Ω) (a : T) ↦ Y 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
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
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 : (t : T) → TopologicalSpace (F t)
inst_5 : (t : T) → MeasurableSpace (F t)
inst_6 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_7 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst_8 : Fintype S
inst_9 : Fintype T
inst_10 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s)
          (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
f : (i : S) → E i →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
rw :
  ∫ (x : Ω),
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).1 i))
        (∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).2 j)) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), ∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x) i) ∂P)
      (∫ (x : Ω), ∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : T) ↦ Y a x) j) ∂P)
hφ : AEMeasurable (β := (j : T) → F j) (fun (c : Ω) (a : T) ↦ Y a c) P
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, fun (a : T) ↦ Y a ω)) P)
      fun (p : ((i : S) → E i) × ((j : T) → F j)) ↦
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i)) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j))) =
    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 _ _ _ _ (MeasurableSpace.pi (X := F)) (map (fun (c : Ω) (a : T) ↦ Y a c) P) fun (y : (j : T) → F j) ↦
        ∏ j : T, (g j : (a : F j) → ℝ) (y j))
have hfm : AEStronglyMeasurable (β := ℝ) (m₀ := MeasurableSpace.pi (X := F))
  (fun (y : (j : T) → F j) ↦ ∏ j : T, (g j : (a : F j) → ℝ) (y j)) (map (fun (c : Ω) (a : T) ↦ Y 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
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
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 : (t : T) → TopologicalSpace (F t)
inst_5 : (t : T) → MeasurableSpace (F t)
inst_6 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_7 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst_8 : Fintype S
inst_9 : Fintype T
inst_10 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s)
          (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
f : (i : S) → E i →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
rw :
  ∫ (x : Ω),
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).1 i))
        (∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).2 j)) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), ∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x) i) ∂P)
      (∫ (x : Ω), ∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : T) ↦ Y a x) j) ∂P)
hφ : AEMeasurable (β := (j : T) → F j) (fun (c : Ω) (a : T) ↦ Y a c) P
hfm :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasurableSpace.pi (X := F))
    (fun (y : (j : T) → F j) ↦ ∏ j : T, (g j : (a : F j) → ℝ) (y j)) (map (fun (c : Ω) (a : T) ↦ Y a c) P)
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, fun (a : T) ↦ Y a ω)) P)
      fun (p : ((i : S) → E i) × ((j : T) → F j)) ↦
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i)) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j))) =
    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 _ _ _ _ (MeasurableSpace.pi (X := F)) (map (fun (c : Ω) (a : T) ↦ Y a c) P) fun (y : (j : T) → F j) ↦
        ∏ j : T, (g j : (a : F j) → ℝ) (y j))
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
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
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 : (t : T) → TopologicalSpace (F t)
inst_5 : (t : T) → MeasurableSpace (F t)
inst_6 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_7 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst_8 : Fintype S
inst_9 : Fintype T
inst_10 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s)
          (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
f : (i : S) → E i →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
rw :
  ∫ (x : Ω),
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).1 i))
        (∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).2 j)) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), ∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x) i) ∂P)
      (∫ (x : Ω), ∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : T) ↦ Y a x) j) ∂P)
hφ : AEMeasurable (β := (j : T) → F j) (fun (c : Ω) (a : T) ↦ Y a c) P
hfm :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasurableSpace.pi (X := F))
    (fun (y : (j : T) → F j) ↦ ∏ j : T, (g j : (a : F j) → ℝ) (y j)) (map (fun (c : Ω) (a : T) ↦ Y a c) 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 ω, fun (a : T) ↦ Y a ω)) P)
      fun (p : ((i : S) → E i) × ((j : T) → F j)) ↦
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i)) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j))) =
    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 _ _ _ _ (MeasurableSpace.pi (X := F)) (map (fun (c : Ω) (a : T) ↦ Y a c) P) fun (y : (j : T) → F j) ↦
        ∏ j : T, (g j : (a : F j) → ℝ) (y j))
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]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
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 : (t : T) → TopologicalSpace (F t)
inst_5 : (t : T) → MeasurableSpace (F t)
inst_6 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_7 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst_8 : Fintype S
inst_9 : Fintype T
inst_10 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s)
          (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
f : (i : S) → E i →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
rw :
  ∫ (x : Ω),
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).1 i))
        (∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).2 j)) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), ∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x) i) ∂P)
      (∫ (x : Ω), ∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : T) ↦ Y a x) j) ∂P)
hφ : AEMeasurable (β := (j : T) → F j) (fun (c : Ω) (a : T) ↦ Y a c) P
hfm :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasurableSpace.pi (X := F))
    (fun (y : (j : T) → F j) ↦ ∏ j : T, (g j : (a : F j) → ℝ) (y j)) (map (fun (c : Ω) (a : T) ↦ Y a c) P)
hφ₁ : AEMeasurable (β := (i : S) → E i) (fun (c : Ω) (a : S) ↦ X a c) P
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)
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, fun (a : T) ↦ Y a ω)) P)
      fun (p : ((i : S) → E i) × ((j : T) → F j)) ↦
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i)) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j))) =
    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 _ _ _ _ (MeasurableSpace.pi (X := F)) (map (fun (c : Ω) (a : T) ↦ Y a c) P) fun (y : (j : T) → F j) ↦
        ∏ j : T, (g j : (a : F j) → ℝ) (y j))
have hφ₂ : AEMeasurable (β := ((i : S) → E i) × ((j : T) → F j)) (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, fun (a : T) ↦ Y a ω)) 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
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
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 : (t : T) → TopologicalSpace (F t)
inst_5 : (t : T) → MeasurableSpace (F t)
inst_6 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_7 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst_8 : Fintype S
inst_9 : Fintype T
inst_10 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s)
          (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
f : (i : S) → E i →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
rw :
  ∫ (x : Ω),
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).1 i))
        (∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).2 j)) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), ∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x) i) ∂P)
      (∫ (x : Ω), ∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : T) ↦ Y a x) j) ∂P)
hφ : AEMeasurable (β := (j : T) → F j) (fun (c : Ω) (a : T) ↦ Y a c) P
hfm :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasurableSpace.pi (X := F))
    (fun (y : (j : T) → F j) ↦ ∏ j : T, (g j : (a : F j) → ℝ) (y j)) (map (fun (c : Ω) (a : T) ↦ Y a c) P)
hφ₁ : AEMeasurable (β := (i : S) → E i) (fun (c : Ω) (a : S) ↦ X a c) P
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)
hφ₂ : AEMeasurable (β := ((i : S) → E i) × ((j : T) → F j)) (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, fun (a : T) ↦ Y a ω)) P
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, fun (a : T) ↦ Y a ω)) P)
      fun (p : ((i : S) → E i) × ((j : T) → F j)) ↦
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i)) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j))) =
    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 _ _ _ _ (MeasurableSpace.pi (X := F)) (map (fun (c : Ω) (a : T) ↦ Y a c) P) fun (y : (j : T) → F j) ↦
        ∏ j : T, (g j : (a : F j) → ℝ) (y j))
have hfm₂ : AEStronglyMeasurable (β := ℝ) (m₀ := Prod.instMeasurableSpace)
  (fun (p : ((i : S) → E i) × ((j : T) → F j)) ↦
    HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) (p.1 i)) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j)))
  (map (fun (ω : Ω) ↦ (fun (a : S) ↦ X a ω, fun (a : T) ↦ Y a ω)) 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
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
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 : (t : T) → TopologicalSpace (F t)
inst_5 : (t : T) → MeasurableSpace (F t)
inst_6 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_7 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst_8 : Fintype S
inst_9 : Fintype T
inst_10 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s)
          (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
f : (i : S) → E i →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
⊢ ∫ (x : Ω),
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).1 i))
        (∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).2 j)) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), ∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x) i) ∂P)
      (∫ (x : Ω), ∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : T) ↦ Y a x) j) ∂P)
have h₁ : ∀ (x : Ω),
  HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).1 i))
      (∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).2 j)) =
    HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s)
      (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x
Tactic: convert! h f g
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
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 : (t : T) → TopologicalSpace (F t)
inst_5 : (t : T) → MeasurableSpace (F t)
inst_6 : ∀ (t : T), BorelSpace.{u_5} (F t)
inst_7 : ∀ (t : T), HasOuterApproxClosed.{u_5} (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst_8 : Fintype S
inst_9 : Fintype T
inst_10 : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s)
          (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x ∂P)
        (∫ (x : Ω), (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x ∂P)
f : (i : S) → E i →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
h₁ :
  ∀ (x : Ω),
    HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).1 i))
        (∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).2 j)) =
      HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s)
        (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x
⊢ ∫ (x : Ω),
      HMul.hMul (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).1 i))
        (∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : S) ↦ X a x, fun (a : T) ↦ Y a x).2 j)) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), ∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x) i) ∂P)
      (∫ (x : Ω), ∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : T) ↦ Y a x) j) ∂P)
have h₂ : ∀ (x : Ω),
  Eq (α := ℝ) (∏ i : S, (f i : (a : E i) → ℝ) ((fun (a : S) ↦ X a x) i)) ((∏ s : S, (⇑(f s) : (a : E s) → ℝ) ∘ X s) x)
Tactic: convert! h f g