awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
⊢ Eq (α := Measure (G × H)) (map (fun (ω : Ω) ↦ (Z ω, U ω)) P) (Measure.prod (map Z P) (map U P))
have refine : ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
  (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (Z ω, U ω)) P) fun (p : G × H) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)) =
    HMul.hMul (α := ℝ) (@integral _ _ _ _ inst_1 (map Z P) fun (z : G) ↦ (f : (a : G) → ℝ) z)
      (@integral _ _ _ _ inst_5 (map U P) fun (t : H) ↦ (g : (a : H) → ℝ) t)
Tactic: refine eq_prod_of_integral_mul_boundedContinuousFunction fun f g ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (Z ω, U ω)) P) fun (p : G × H) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)) =
    HMul.hMul (α := ℝ) (@integral _ _ _ _ inst_1 (map Z P) fun (z : G) ↦ (f : (a : G) → ℝ) z)
      (@integral _ _ _ _ inst_5 (map U P) fun (t : H) ↦ (g : (a : H) → ℝ) t)
have rw : ∫ (x : Ω), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z x, U x).1 : ℝ) ((g : (a : H) → ℝ) (Z x, U x).2 : ℝ) ∂P =
  HMul.hMul (α := ℝ) (∫ (x : Ω), (f : (a : G) → ℝ) (Z x) ∂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
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
rw :
  ∫ (x : Ω), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z x, U x).1 : ℝ) ((g : (a : H) → ℝ) (Z x, U x).2 : ℝ) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), (f : (a : G) → ℝ) (Z x) ∂P) (∫ (x : Ω), (g : (a : H) → ℝ) (U x) ∂P)
hφ : AEMeasurable U P
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (Z ω, U ω)) P) fun (p : G × H) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)) =
    HMul.hMul (α := ℝ) (@integral _ _ _ _ inst_1 (map Z P) fun (z : G) ↦ (f : (a : G) → ℝ) z)
      (@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
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
rw :
  ∫ (x : Ω), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z x, U x).1 : ℝ) ((g : (a : H) → ℝ) (Z x, U x).2 : ℝ) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), (f : (a : G) → ℝ) (Z x) ∂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 Z P
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (Z ω, U ω)) P) fun (p : G × H) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)) =
    HMul.hMul (α := ℝ) (@integral _ _ _ _ inst_1 (map Z P) fun (z : G) ↦ (f : (a : G) → ℝ) z)
      (@integral _ _ _ _ inst_5 (map U P) fun (t : H) ↦ (g : (a : H) → ℝ) t)
have hfm₁ : AEStronglyMeasurable (β := ℝ) (m₀ := inst_1) (⇑f : (a : G) → ℝ) (map Z P)
Tactic: rw [integral_map, integral_map, integral_map]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
rw :
  ∫ (x : Ω), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z x, U x).1 : ℝ) ((g : (a : H) → ℝ) (Z x, U x).2 : ℝ) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), (f : (a : G) → ℝ) (Z x) ∂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 Z P
hfm₁ : AEStronglyMeasurable (β := ℝ) (m₀ := inst_1) (⇑f : (a : G) → ℝ) (map Z P)
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (Z ω, U ω)) P) fun (p : G × H) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)) =
    HMul.hMul (α := ℝ) (@integral _ _ _ _ inst_1 (map Z P) fun (z : G) ↦ (f : (a : G) → ℝ) z)
      (@integral _ _ _ _ inst_5 (map U P) fun (t : H) ↦ (g : (a : H) → ℝ) t)
have hφ₂ : AEMeasurable (β := G × H) (fun (ω : Ω) ↦ (Z ω, U ω)) P
Tactic: rw [integral_map, integral_map, integral_map]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
rw :
  ∫ (x : Ω), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) (Z x, U x).1 : ℝ) ((g : (a : H) → ℝ) (Z x, U x).2 : ℝ) ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), (f : (a : G) → ℝ) (Z x) ∂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 Z P
hfm₁ : AEStronglyMeasurable (β := ℝ) (m₀ := inst_1) (⇑f : (a : G) → ℝ) (map Z P)
hφ₂ : AEMeasurable (β := G × H) (fun (ω : Ω) ↦ (Z ω, U ω)) P
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace (map (fun (ω : Ω) ↦ (Z ω, U ω)) P) fun (p : G × H) ↦
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)) =
    HMul.hMul (α := ℝ) (@integral _ _ _ _ inst_1 (map Z P) fun (z : G) ↦ (f : (a : G) → ℝ) z)
      (@integral _ _ _ _ inst_5 (map U P) fun (t : H) ↦ (g : (a : H) → ℝ) t)
have hfm₂ : AEStronglyMeasurable (β := ℝ) (m₀ := Prod.instMeasurableSpace)
  (fun (p : G × H) ↦ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ))
  (map (fun (ω : Ω) ↦ (Z ω, U ω)) P)
Tactic: rw [integral_map, integral_map, integral_map]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ Measurable (β := ℝ) fun (p : G × H) ↦
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)
have funProp : inst_1 ≤ inst_1
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
funProp : inst_1 ≤ inst_1
⊢ Measurable (β := ℝ) fun (p : G × H) ↦
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)
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
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
funProp : inst_1 ≤ inst_1
funProp₁ : MeasurableEmbedding (β := ℝ) fun (a0 : G) ↦ (f : (a : G) → ℝ) a0
⊢ Measurable (β := ℝ) fun (p : G × H) ↦
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)
have funProp₂ : inst_5 ≤ inst_5
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
inst_4 : TopologicalSpace H
inst_5 : MeasurableSpace H
inst_6 : BorelSpace H
inst_7 : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst_8 : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z) ((⇑g : (a : H) → ℝ) ∘ U) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P) (∫ (x : Ω), ((⇑g : (a : H) → ℝ) ∘ U) x ∂P)
f : G →ᵇ ℝ
g : H →ᵇ ℝ
funProp : inst_1 ≤ inst_1
funProp₁ : MeasurableEmbedding (β := ℝ) fun (a0 : G) ↦ (f : (a : G) → ℝ) a0
funProp₂ : inst_5 ≤ inst_5
⊢ Measurable (β := ℝ) fun (p : G × H) ↦
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : G) → ℝ) p.1 : ℝ) ((g : (a : H) → ℝ) p.2 : ℝ)
have funProp₃ : MeasurableEmbedding (β := ℝ) fun (a0 : H) ↦ (g : (a : H) → ℝ) a0
Tactic: 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
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
⊢ A.indicator 1 ⟂ᵢ[P] fun (ω : Ω) (s : S) ↦ X s ω
have refine : ∀ (f : ℝ →ᵇ ℝ) (g : (t : S) → E t →ᵇ ℝ),
  ∫ (x : Ω),
      HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) (Function.comp (β := ℝ) (⇑f : (a : ℝ) → ℝ) (A.indicator 1))
        (∏ t : S, (⇑(g t) : (a : E t) → ℝ) ∘ X t) x ∂P =
    HMul.hMul (α := ℝ) (∫ (x : Ω), Function.comp (β := ℝ) (⇑f : (a : ℝ) → ℝ) (A.indicator 1) x ∂P)
      (∫ (x : Ω), (∏ t : S, (⇑(g t) : (a : E t) → ℝ) ∘ X t) x ∂P)
Tactic: refine indepFun_pi_of_prod_bcf
    ((aemeasurable_indicator_const_iff 1).2 mA) mX 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
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
ω : Ω
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
    A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω +
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
      A.indicator
        (fun (ω : Ω) ↦
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
        ω
have rw : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (if ω ∈ A then 1 ω else 0) : ℝ)
    (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
  A.indicator
        (fun (ω : Ω) ↦
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
        ω +
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
    A.indicator
      (fun (ω : Ω) ↦ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
      ω
Tactic: rw [Set.indicator_apply]
-- 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
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
ω : Ω
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (if ω ∈ A then 1 ω else 0) : ℝ)
      (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
    A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω +
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
      A.indicator
        (fun (ω : Ω) ↦
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
        ω
have pos : ω ∈ A →
  HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
    A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω +
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
      A.indicator
        (fun (ω : Ω) ↦
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
        ω
Tactic: split_ifs
-- 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
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
ω : Ω
pos :
  ω ∈ A →
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (if ω ∈ A then 1 ω else 0) : ℝ)
      (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
    A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω +
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
      A.indicator
        (fun (ω : Ω) ↦
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
        ω
have neg : ω ∉ A →
  HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
    A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω +
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
      A.indicator
        (fun (ω : Ω) ↦
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
        ω
Tactic: split_ifs
-- 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
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)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
ω : Ω
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
    A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω +
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
      A.indicator
        (fun (ω : Ω) ↦
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
        ω
have rw : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (if ω ∈ A then 1 ω else 0) : ℝ)
    (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
  A.indicator
        (fun (ω : Ω) ↦
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
        ω +
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
    A.indicator
      (fun (ω : Ω) ↦ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
      ω
Tactic: classical
    rw [Set.indicator_apply]
    split_ifs <;> simp_all