awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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)
refine :
  ∀ (f : G →ᵇ ℝ) (g : (j : T) → F j →ᵇ ℝ),
    (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (Z ω, fun (a : T) ↦ Y a ω)) P)
        fun (p : G × ((j : T) → F j)) ↦
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j) : ℝ)) =
      HMul.hMul (α := ℝ) (@integral _ _ _ _ inst_5 (map Z P) fun (z : G) ↦ (f : (a : G) → ℝ) z)
        (@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))
⊢ Eq (α := Measure (G × ((a : T) → F a))) (map (fun (ω : Ω) ↦ (Z ω, fun (a : T) ↦ Y a ω)) P)
    (Measure.prod (map Z P) (map (fun (c : Ω) (a : T) ↦ Y a c) P))

Tactic:
refine eq_prod_of_integral_mul_prod_boundedContinuousFunction fun f g ↦ ?_

Premises used: Measure.eq_prod_of_integral_mul_prod_boundedContinuousFunction
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 →ᵇ ℝ
rw :
  ∫ (x : Ω),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z x, fun (a : T) ↦ Y a x).1 : ℝ)
        (∏ j : T, (g j : (a : F j) → ℝ) ((Z x, fun (a : T) ↦ Y a x).2 j) : ℝ) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), (f : (a : G) → ℝ) (Z x) ∂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 Z P
hfm₁ : AEStronglyMeasurable (β := ℝ) (m₀ := inst_5) (⇑f : (a : G) → ℝ) (map Z P)
hφ₂ : AEMeasurable (β := G × ((j : T) → F j)) (fun (ω : Ω) ↦ (Z ω, fun (a : T) ↦ Y a ω)) P
hfm₂ :
  AEStronglyMeasurable (β := ℝ) (m₀ := Prod.instMeasurableSpace)
    (fun (p : G × ((j : T) → F j)) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j) : ℝ))
    (map (fun (ω : Ω) ↦ (Z ω, fun (a : T) ↦ Y a ω)) P)
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (Z ω, fun (a : T) ↦ Y a ω)) P)
      fun (p : G × ((j : T) → F j)) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j) : ℝ)) =
    HMul.hMul (α := ℝ) (@integral _ _ _ _ inst_5 (map Z P) fun (z : G) ↦ (f : (a : G) → ℝ) z)
      (@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))

Tactic:
rw [integral_map, integral_map, integral_map]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 →ᵇ ℝ
⊢ ∫ (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:
h f g
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 →ᵇ ℝ
h₁ :
  ∀ (x : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z x, fun (a : T) ↦ Y a x).1 : ℝ)
        (∏ j : T, (g j : (a : F j) → ℝ) ((Z x, fun (a : T) ↦ Y a x).2 j) : ℝ) =
      HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x
h₂ :
  ∀ (x : Ω),
    Eq (α := ℝ) (∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : T) ↦ Y a x) j)) ((∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x)
⊢ ∫ (x : Ω),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z x, fun (a : T) ↦ Y a x).1 : ℝ)
        (∏ j : T, (g j : (a : F j) → ℝ) ((Z x, fun (a : T) ↦ Y a x).2 j) : ℝ) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), (f : (a : G) → ℝ) (Z x) ∂P)
      (∫ (x : Ω), ∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : T) ↦ Y a x) j) ∂P)

Tactic:
convert! h f g
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 →ᵇ ℝ
x : Ω
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z x, fun (a : T) ↦ Y a x).1 : ℝ)
      (∏ j : T, (g j : (a : F j) → ℝ) ((Z x, fun (a : T) ↦ Y a x).2 j) : ℝ) =
    HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) (∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x

Tactic:
simp
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 →ᵇ ℝ
x : Ω
⊢ Eq (α := ℝ) (∏ j : T, (g j : (a : F j) → ℝ) ((fun (a : T) ↦ Y a x) j)) ((∏ t : T, (⇑(g t) : (a : F t) → ℝ) ∘ Y t) x)

Tactic:
simp
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 →ᵇ ℝ
⊢ AEMeasurable (β := (j : T) → F j) (fun (c : Ω) (a : T) ↦ Y a c) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 →ᵇ ℝ
⊢ AEMeasurable Z P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 →ᵇ ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := inst_5) (⇑f : (a : G) → ℝ) (map Z P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 →ᵇ ℝ
⊢ AEMeasurable (β := G × ((j : T) → F j)) (fun (ω : Ω) ↦ (Z ω, fun (a : T) ↦ Y a ω)) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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
funProp₁ :
  ∀ (i : T),
    Membership.mem (γ := Finset T) Finset.univ i →
      MeasurableEmbedding (β := ℝ) fun (a1 : F i) ↦ (g i : (a : F i) → ℝ) a1
⊢ Measurable (β := ℝ) fun (y : (j : T) → F j) ↦ ∏ j : T, (g j : (a : F j) → ℝ) (y j)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 →ᵇ ℝ
⊢ 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:
exact Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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
funProp₃ :
  ∀ (i : T),
    Membership.mem (γ := Finset T) Finset.univ i →
      MeasurableEmbedding (β := ℝ) fun (a1 : F i) ↦ (g i : (a : F i) → ℝ) a1
⊢ 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) : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 →ᵇ ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Prod.instMeasurableSpace)
    (fun (p : G × ((j : T) → F j)) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) (∏ j : T, (g j : (a : F j) → ℝ) (p.2 j) : ℝ))
    (map (fun (ω : Ω) ↦ (Z ω, fun (a : T) ↦ Y a ω)) P)

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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)
have : ∀ (this : Fintype T), Z ⟂ᵢ[P] fun (ω : Ω) (t : T) ↦ Y t ω
⊢ Z ⟂ᵢ[P] fun (ω : Ω) (t : T) ↦ Y t ω

Tactic:
have := Fintype.ofFinite T
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 ω

Tactic:
indepFun_pi_of_prod_bcf mZ mY fun f g ↦ ?_

Premises used: indepFun_pi_of_prod_bcf
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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
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)
⊢ Z ⟂ᵢ[P] fun (ω : Ω) (t : T) ↦ Y t ω

Tactic:
refine indepFun_pi_of_prod_bcf mZ mY fun f g ↦ ?_

Premises used: indepFun_pi_of_prod_bcf
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 →ᵇ ℝ
t : T
⊢ Continuous (X := (t : T) → F t) (Function.eval (β := F) t)

Tactic:
fun_prop