awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 : IsProbabilityMeasure P
inst_5 : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ),
    ∫ (ω : Ω) in A, (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P =
      P.real A * ∫ (ω : Ω), (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P
have : ∀ (this : Fintype S), A.indicator 1 ⟂ᵢ[P] fun (ω : Ω) (s : S) ↦ X s ω
⊢ A.indicator 1 ⟂ᵢ[P] fun (ω : Ω) (s : S) ↦ X s ω

Tactic:
have := Fintype.ofFinite S
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 : IsProbabilityMeasure P
inst_5 : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ),
    ∫ (ω : Ω) in A, (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P =
      P.real A * ∫ (ω : Ω), (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P
this : Fintype S
⊢ A.indicator 1 ⟂ᵢ[P] fun (ω : Ω) (s : S) ↦ X s ω

Tactic:
indicator_indepFun_pi_of_prod_bcf mA mX fun f ↦ ?_

Premises used: indicator_indepFun_pi_of_prod_bcf
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 : IsProbabilityMeasure P
inst_5 : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ),
    ∫ (ω : Ω) in A, (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P =
      P.real A * ∫ (ω : Ω), (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P
this : Fintype S
refine :
  ∀ (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 ω

Tactic:
refine indicator_indepFun_pi_of_prod_bcf mA mX fun f ↦ ?_

Premises used: indicator_indepFun_pi_of_prod_bcf
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 : IsProbabilityMeasure P
inst_5 : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ),
    ∫ (ω : Ω) in A, (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P =
      P.real A * ∫ (ω : Ω), (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
s : S
⊢ Continuous (X := (s : S) → E s) (Function.eval (β := E) s)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 : IsProbabilityMeasure P
inst_5 : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ),
    ∫ (ω : Ω) in A, (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P =
      P.real A * ∫ (ω : Ω), (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
h₁ h₂ :
  ∀ (x : Ω),
    Eq (α := ℝ) (∏ s : S, (f s : (a : E s) → ℝ) (X s x) : ℝ)
      ((∏ s : S, (f s).compContinuous { toFun := Function.eval (β := E) s, continuous_toFun := ⋯ } :
            (a : (s : S) → E s) → ℝ)
          fun (x_1 : S) ↦ X x_1 x :
        ℝ)
⊢ ∫ (ω : Ω) 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

Tactic:
convert! h (∏ s, (f s).compContinuous ⟨Function.eval s, by fun_prop⟩)

Premises used: Finset.univ, ContinuousMap.mk, Function.eval, BoundedContinuousFunction.compContinuous, Finset.prod
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 : IsProbabilityMeasure P
inst_5 : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ),
    ∫ (ω : Ω) in A, (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P =
      P.real A * ∫ (ω : Ω), (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
x : Ω
⊢ Eq (α := ℝ) (∏ s : S, (f s : (a : E s) → ℝ) (X s x) : ℝ)
    ((∏ s : S, (f s).compContinuous { toFun := Function.eval (β := E) s, continuous_toFun := ⋯ } :
          (a : (s : S) → E s) → ℝ)
        fun (x_1 : S) ↦ X x_1 x :
      ℝ)

Tactic:
simp
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
Z : Ω → G
inst_4 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, (f : (a : G) → ℝ) (Z ω) ∂P = P.real A * ∫ (ω : Ω), (f : (a : G) → ℝ) (Z ω) ∂P
suffices : A.indicator 1 ⟂ᵢ[P] fun (ω : Ω) (x : Unit) ↦ Z ω
⊢ A.indicator 1 ⟂ᵢ[P] Z

Tactic:
suffices (A.indicator (1 : Ω → ℝ)) ⟂ᵢ[P] (fun ω (_ : Unit) ↦ Z ω) from
    this.comp (measurable_id) (measurable_pi_apply ())
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
Z : Ω → G
inst_4 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, (f : (a : G) → ℝ) (Z ω) ∂P = P.real A * ∫ (ω : Ω), (f : (a : G) → ℝ) (Z ω) ∂P
⊢ A.indicator 1 ⟂ᵢ[P] fun (ω : Ω) (x : Unit) ↦ Z ω

Tactic:
indicator_indepFun_pi_of_prod_bcf mA (fun _ ↦ mZ) fun f ↦ ?_

Premises used: indicator_indepFun_pi_of_prod_bcf
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
Z : Ω → G
inst_4 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, (f : (a : G) → ℝ) (Z ω) ∂P = P.real A * ∫ (ω : Ω), (f : (a : G) → ℝ) (Z ω) ∂P
refine :
  ∀ (f : (s : Unit) → G →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : Unit, (f s : (a : G) → ℝ) (Z ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : Unit, (f s : (a : G) → ℝ) (Z ω) ∂P
⊢ A.indicator 1 ⟂ᵢ[P] fun (ω : Ω) (x : Unit) ↦ Z ω

Tactic:
refine indicator_indepFun_pi_of_prod_bcf mA (fun _ ↦ mZ) fun f ↦ ?_

Premises used: indicator_indepFun_pi_of_prod_bcf
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
Z : Ω → G
inst_4 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, (f : (a : G) → ℝ) (Z ω) ∂P = P.real A * ∫ (ω : Ω), (f : (a : G) → ℝ) (Z ω) ∂P
f : (s : Unit) → G →ᵇ ℝ
⊢ ∫ (ω : Ω) in A, (f () : (a : G) → ℝ) (Z ω) ∂P = P.real A * ∫ (ω : Ω), (f () : (a : G) → ℝ) (Z ω) ∂P

Tactic:
h (f ())

Premises used: Unit.unit
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
Z : Ω → G
inst_4 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, (f : (a : G) → ℝ) (Z ω) ∂P = P.real A * ∫ (ω : Ω), (f : (a : G) → ℝ) (Z ω) ∂P
f : (s : Unit) → G →ᵇ ℝ
h₁ h₂ : ∀ (x : Ω), Eq (α := ℝ) (∏ s : Unit, (f s : (a : G) → ℝ) (Z x) : ℝ) ((f () : (a : G) → ℝ) (Z x) : ℝ)
⊢ ∫ (ω : Ω) in A, ∏ s : Unit, (f s : (a : G) → ℝ) (Z ω) ∂P =
    P.real A * ∫ (ω : Ω), ∏ s : Unit, (f s : (a : G) → ℝ) (Z ω) ∂P

Tactic:
convert! h (f ())

Premises used: Unit.unit
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
Z : Ω → G
inst_4 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, (f : (a : G) → ℝ) (Z ω) ∂P = P.real A * ∫ (ω : Ω), (f : (a : G) → ℝ) (Z ω) ∂P
f : (s : Unit) → G →ᵇ ℝ
x : Ω
⊢ Eq (α := ℝ) (∏ s : Unit, (f s : (a : G) → ℝ) (Z x) : ℝ) ((f () : (a : G) → ℝ) (Z x) : ℝ)

Tactic:
simp
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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
𝒜 : Set (Set Ω)
m𝒜 : ∀ A ∈ 𝒜, NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ A ∈ 𝒜,
    ∀ (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
⊢ IndepSets 𝒜 {A : Set Ω | MeasurableSet A} P

Tactic:
indepSets_iff_singleton_indepSets.2 fun A hA ↦ IndepFun.singleton_indepSets_of_indicator
    (indicator_indepFun_pi_of_prod_bcf (m𝒜 A hA) mX (h A hA))

Premises used: Iff.mpr, indicator_indepFun_pi_of_prod_bcf, ProbabilityTheory.indepSets_iff_singleton_indepSets, IndepFun.singleton_indepSets_of_indicator
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 : IsProbabilityMeasure P
inst_5 : Finite S
𝒜 : Set (Set Ω)
m𝒜 : ∀ A ∈ 𝒜, NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ A ∈ 𝒜,
    ∀ (f : ((s : S) → E s) →ᵇ ℝ),
      ∫ (ω : Ω) in A, (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P =
        P.real A * ∫ (ω : Ω), (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P
⊢ IndepSets 𝒜 {A : Set Ω | MeasurableSet A} P

Tactic:
indepSets_iff_singleton_indepSets.2 fun A hA ↦ IndepFun.singleton_indepSets_of_indicator
    (indicator_indepFun_pi_of_bcf (m𝒜 A hA) mX (h A hA))

Premises used: Iff.mpr, indicator_indepFun_pi_of_bcf, ProbabilityTheory.indepSets_iff_singleton_indepSets, IndepFun.singleton_indepSets_of_indicator
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
Z : Ω → G
inst_4 : IsProbabilityMeasure P
𝒜 : Set (Set Ω)
m𝒜 : ∀ A ∈ 𝒜, NullMeasurableSet A P
mZ : AEMeasurable Z P
h :
  ∀ A ∈ 𝒜, ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, (f : (a : G) → ℝ) (Z ω) ∂P = P.real A * ∫ (ω : Ω), (f : (a : G) → ℝ) (Z ω) ∂P
⊢ IndepSets 𝒜 {A : Set Ω | MeasurableSet A} P

Tactic:
indepSets_iff_singleton_indepSets.2 fun A hA ↦ IndepFun.singleton_indepSets_of_indicator
    (indicator_indepFun_of_bcf (m𝒜 A hA) mZ (h A hA))

Premises used: Iff.mpr, indicator_indepFun_of_bcf, ProbabilityTheory.indepSets_iff_singleton_indepSets, IndepFun.singleton_indepSets_of_indicator
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
m 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
hm : m ≤ mΩ
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (A : Set Ω),
    MeasurableSet A →
      ∀ (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
⊢ Indep m (MeasurableSpace.comap (β := (s : S) → E s) (fun (ω : Ω) (s : S) ↦ X s ω) (MeasurableSpace.pi (X := E))) P

Tactic:
(Indep_iff_IndepSets _ _ P).2
    (indepSets_comap_pi_of_prod_bcf (fun A hA ↦ (hm A hA).nullMeasurableSet) mX h)

Premises used: Iff.mpr, MeasurableSet.nullMeasurableSet, indepSets_comap_pi_of_prod_bcf, ProbabilityTheory.Indep_iff_IndepSets
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
S : Type u_2
m 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 : IsProbabilityMeasure P
inst_5 : Finite S
hm : m ≤ mΩ
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (A : Set Ω),
    MeasurableSet A →
      ∀ (f : ((s : S) → E s) →ᵇ ℝ),
        ∫ (ω : Ω) in A, (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P =
          P.real A * ∫ (ω : Ω), (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P
⊢ Indep m (MeasurableSpace.comap (β := (s : S) → E s) (fun (ω : Ω) (s : S) ↦ X s ω) (MeasurableSpace.pi (X := E))) P

Tactic:
(Indep_iff_IndepSets _ _ P).2
    (indepSets_comap_pi_of_bcf (fun A hA ↦ (hm A hA).nullMeasurableSet) mX h)

Premises used: Iff.mpr, MeasurableSet.nullMeasurableSet, indepSets_comap_pi_of_bcf, ProbabilityTheory.Indep_iff_IndepSets
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
Z : Ω → G
inst_4 : IsProbabilityMeasure P
hm : m ≤ mΩ
mZ : AEMeasurable Z P
h :
  ∀ (A : Set Ω),
    MeasurableSet A →
      ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, (f : (a : G) → ℝ) (Z ω) ∂P = P.real A * ∫ (ω : Ω), (f : (a : G) → ℝ) (Z ω) ∂P
⊢ Indep m (MeasurableSpace.comap Z inferInstance) P

Tactic:
(Indep_iff_IndepSets _ _ P).2
    (indepSets_comap_of_bcf (fun A hA ↦ (hm A hA).nullMeasurableSet) mZ h)

Premises used: Iff.mpr, MeasurableSet.nullMeasurableSet, indepSets_comap_of_bcf, ProbabilityTheory.Indep_iff_IndepSets
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (I : Finset S) (J : Finset T) (f : (s : ↥I) → E (↑s : S) →ᵇ ℝ) (g : (t : ↥J) → F (↑t : T) →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ)
          (∏ s : ↥I, Function.comp (β := E (↑s : S)) (⇑(f s) : (a : E (↑s : S)) → ℝ) (X (↑s : S)))
          (∏ t : ↥J, Function.comp (β := F (↑t : T)) (⇑(g t) : (a : F (↑t : T)) → ℝ) (Y (↑t : T))) x ∂P =
      HMul.hMul (α := ℝ)
        (∫ (x : Ω), (∏ s : ↥I, Function.comp (β := E (↑s : S)) (⇑(f s) : (a : E (↑s : S)) → ℝ) (X (↑s : S))) x ∂P)
        (∫ (x : Ω), (∏ t : ↥J, Function.comp (β := F (↑t : T)) (⇑(g t) : (a : F (↑t : T)) → ℝ) (Y (↑t : T))) x ∂P)
I : Finset S
J : Finset T
⊢ ∀ (s : ↥I), AEMeasurable (β := E (↑s : S)) (X (↑s : S)) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (I : Finset S) (J : Finset T) (f : (s : ↥I) → E (↑s : S) →ᵇ ℝ) (g : (t : ↥J) → F (↑t : T) →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ)
          (∏ s : ↥I, Function.comp (β := E (↑s : S)) (⇑(f s) : (a : E (↑s : S)) → ℝ) (X (↑s : S)))
          (∏ t : ↥J, Function.comp (β := F (↑t : T)) (⇑(g t) : (a : F (↑t : T)) → ℝ) (Y (↑t : T))) x ∂P =
      HMul.hMul (α := ℝ)
        (∫ (x : Ω), (∏ s : ↥I, Function.comp (β := E (↑s : S)) (⇑(f s) : (a : E (↑s : S)) → ℝ) (X (↑s : S))) x ∂P)
        (∫ (x : Ω), (∏ t : ↥J, Function.comp (β := F (↑t : T)) (⇑(g t) : (a : F (↑t : T)) → ℝ) (Y (↑t : T))) x ∂P)
I : Finset S
J : Finset T
⊢ ∀ (t : ↥J), AEMeasurable (β := F (↑t : T)) (Y (↑t : T)) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (I : Finset S) (J : Finset T) (f : ((s : ↥I) → E (↑s : S)) →ᵇ ℝ) (g : ((t : ↥J) → F (↑t : T)) →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (s : ↥I) → E (↑s : S)) → ℝ) fun (x : ↥I) ↦ X (↑x : S) ω : ℝ)
              ((g : (a : (t : ↥J) → F (↑t : T)) → ℝ) fun (x : ↥J) ↦ Y (↑x : T) ω : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ)
        (∫ (x : Ω), (fun (ω : Ω) ↦ ((f : (a : (s : ↥I) → E (↑s : S)) → ℝ) fun (x : ↥I) ↦ X (↑x : S) ω : ℝ)) x ∂P)
        (∫ (x : Ω), (fun (ω : Ω) ↦ ((g : (a : (t : ↥J) → F (↑t : T)) → ℝ) fun (x : ↥J) ↦ Y (↑x : T) ω : ℝ)) x ∂P)
I : Finset S
J : Finset T
⊢ ∀ (s : ↥I), AEMeasurable (β := E (↑s : S)) (X (↑s : S)) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.BoundedContinuousFunction
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 : IsZeroOrProbabilityMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (I : Finset S) (J : Finset T) (f : ((s : ↥I) → E (↑s : S)) →ᵇ ℝ) (g : ((t : ↥J) → F (↑t : T)) →ᵇ ℝ),
    ∫ (x : Ω),
        (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (s : ↥I) → E (↑s : S)) → ℝ) fun (x : ↥I) ↦ X (↑x : S) ω : ℝ)
              ((g : (a : (t : ↥J) → F (↑t : T)) → ℝ) fun (x : ↥J) ↦ Y (↑x : T) ω : ℝ))
          x ∂P =
      HMul.hMul (α := ℝ)
        (∫ (x : Ω), (fun (ω : Ω) ↦ ((f : (a : (s : ↥I) → E (↑s : S)) → ℝ) fun (x : ↥I) ↦ X (↑x : S) ω : ℝ)) x ∂P)
        (∫ (x : Ω), (fun (ω : Ω) ↦ ((g : (a : (t : ↥J) → F (↑t : T)) → ℝ) fun (x : ↥J) ↦ Y (↑x : T) ω : ℝ)) x ∂P)
I : Finset S
J : Finset T
⊢ ∀ (t : ↥J), AEMeasurable (β := F (↑t : T)) (Y (↑t : T)) 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 : IsZeroOrProbabilityMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (J : Finset T) (g : (t : ↥J) → F (↑t : T) →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z)
          (∏ t : ↥J, Function.comp (β := F (↑t : T)) (⇑(g t) : (a : F (↑t : T)) → ℝ) (Y (↑t : T))) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
        (∫ (x : Ω), (∏ t : ↥J, Function.comp (β := F (↑t : T)) (⇑(g t) : (a : F (↑t : T)) → ℝ) (Y (↑t : T))) x ∂P)
J : Finset T
⊢ 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 : IsZeroOrProbabilityMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (J : Finset T) (g : (t : ↥J) → F (↑t : T) →ᵇ ℝ),
    ∫ (x : Ω),
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) ((⇑f : (a : G) → ℝ) ∘ Z)
          (∏ t : ↥J, Function.comp (β := F (↑t : T)) (⇑(g t) : (a : F (↑t : T)) → ℝ) (Y (↑t : T))) x ∂P =
      HMul.hMul (α := ℝ) (∫ (x : Ω), ((⇑f : (a : G) → ℝ) ∘ Z) x ∂P)
        (∫ (x : Ω), (∏ t : ↥J, Function.comp (β := F (↑t : T)) (⇑(g t) : (a : F (↑t : T)) → ℝ) (Y (↑t : T))) x ∂P)
J : Finset T
⊢ ∀ (t : ↥J), AEMeasurable (β := F (↑t : T)) (Y (↑t : T)) P

Tactic:
fun_prop