awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
refine_2 : AEMeasurable Prod.snd (μ.prod ν)
refine_2₁ : AEMeasurable.mk Y mY =ᶠ[ae (F := Measure Ω') (Measure.map Prod.snd (μ.prod ν))] Y
⊢ AEMeasurable.mk Y mY ∘ Prod.snd =ᶠ[ae (μ.prod ν)] Y ∘ Prod.snd

Tactic:
apply ae_eq_comp

Premises used: MeasureTheory.ae_eq_comp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable Prod.snd (μ.prod ν)

Tactic:
measurable_snd.aemeasurable

Premises used: Measurable.aemeasurable, measurable_snd
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable Prod.snd (μ.prod ν)

Tactic:
exact measurable_snd.aemeasurable

Premises used: Measurable.aemeasurable, measurable_snd
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
refine_2 : AEMeasurable.mk Y mY =ᶠ[ae ν] Y
⊢ AEMeasurable.mk Y mY =ᶠ[ae (F := Measure Ω') (Measure.map Prod.snd (μ.prod ν))] Y

Tactic:
rw [measurePreserving_snd.map_eq]

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.measurePreserving_snd
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable.mk Y mY =ᶠ[ae ν] Y

Tactic:
(AEMeasurable.ae_eq_mk mY).symm

Premises used: AEMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst_2 : MeasurableSpace 𝓧
inst_3 : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun (ω : Ω × Ω') ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun (ω : Ω × Ω') ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable.mk Y mY =ᶠ[ae ν] Y

Tactic:
exact (AEMeasurable.ae_eq_mk mY).symm

Premises used: AEMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
γ : Type u_8
γ' : Type u_9
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
_mβ : MeasurableSpace β
_mβ' : MeasurableSpace β'
_mγ : MeasurableSpace γ
_mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : f ⟂ᵢ[μ] g
hφ : Measurable φ
hψ : Measurable ψ
⊢ (φ ∘ f) ⟂ᵢ[μ] ψ ∘ g

Tactic:
Kernel.IndepFun.comp hfg hφ hψ

Premises used: ProbabilityTheory.Kernel.IndepFun.comp, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
γ : Type u_8
γ' : Type u_9
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
_mβ : MeasurableSpace β
_mβ' : MeasurableSpace β'
_mγ : MeasurableSpace γ
_mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : f ⟂ᵢ[μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hφ : AEMeasurable (_m := _mβ) φ (Measure.map f μ)
hψ : AEMeasurable (_m := _mβ') ψ (Measure.map g μ)
⊢ AEMeasurable (_m := _mΩ) f
    (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
      (⇑(Kernel.const Unit μ) : (a : Unit) → Measure Ω))

Tactic:
simp [hf]
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
γ : Type u_8
γ' : Type u_9
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
_mβ : MeasurableSpace β
_mβ' : MeasurableSpace β'
_mγ : MeasurableSpace γ
_mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : f ⟂ᵢ[μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hφ : AEMeasurable (_m := _mβ) φ (Measure.map f μ)
hψ : AEMeasurable (_m := _mβ') ψ (Measure.map g μ)
⊢ AEMeasurable (_m := _mΩ) g
    (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
      (⇑(Kernel.const Unit μ) : (a : Unit) → Measure Ω))

Tactic:
simp [hg]
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
γ : Type u_8
γ' : Type u_9
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
_mβ : MeasurableSpace β
_mβ' : MeasurableSpace β'
_mγ : MeasurableSpace γ
_mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : f ⟂ᵢ[μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hφ : AEMeasurable (_m := _mβ) φ (Measure.map f μ)
hψ : AEMeasurable (_m := _mβ') ψ (Measure.map g μ)
⊢ AEMeasurable (_m := _mβ) φ
    (Measure.map f
      (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
        (⇑(Kernel.const Unit μ) : (a : Unit) → Measure Ω)))

Tactic:
simp [hφ]
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
γ : Type u_8
γ' : Type u_9
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
_mβ : MeasurableSpace β
_mβ' : MeasurableSpace β'
_mγ : MeasurableSpace γ
_mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : f ⟂ᵢ[μ] g
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hφ : AEMeasurable (_m := _mβ) φ (Measure.map f μ)
hψ : AEMeasurable (_m := _mβ') ψ (Measure.map g μ)
⊢ AEMeasurable (_m := _mβ') ψ
    (Measure.map g
      (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
        (⇑(Kernel.const Unit μ) : (a : Unit) → Measure Ω)))

Tactic:
simp [hψ]
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsZeroOrProbabilityMeasure μ
c : β
X : Ω → β'
⊢ (fun (x : Ω) ↦ c) ⟂ᵢ[μ] X

Tactic:
Kernel.indepFun_const_left c X

Premises used: ProbabilityTheory.Kernel.indepFun_const_left, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsZeroOrProbabilityMeasure μ
X : Ω → β
c : β'
⊢ X ⟂ᵢ[μ] fun (x : Ω) ↦ c

Tactic:
Kernel.indepFun_const_right X c

Premises used: ProbabilityTheory.IndepFun, ProbabilityTheory.Kernel.indepFun_const_right
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
_mβ : MeasurableSpace β
_mβ' : MeasurableSpace β'
inst : Neg β'
inst_1 : MeasurableNeg β'
hfg : f ⟂ᵢ[μ] g
⊢ f ⟂ᵢ[μ] -g

Tactic:
hfg.comp measurable_id measurable_neg

Premises used: measurable_id, MeasurableNeg.measurable_neg, ProbabilityTheory.IndepFun.comp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
_mβ : MeasurableSpace β
_mβ' : MeasurableSpace β'
inst : Neg β
inst_1 : MeasurableNeg β
hfg : f ⟂ᵢ[μ] g
⊢ (-f) ⟂ᵢ[μ] g

Tactic:
hfg.comp measurable_neg measurable_id

Premises used: measurable_id, MeasurableNeg.measurable_neg, ProbabilityTheory.IndepFun.comp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h : iIndepFun (β := β) f μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simpa using h.meas_biInter (S := ∅) (s := fun _ ↦ univ)

Premises used: ProbabilityTheory.iIndepFun.meas_biInter
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
⊢ (fun (a : Ω) (i : ↥S) ↦ f (↑i : ι) a) ⟂ᵢ[μ] fun (a : Ω) (i : ↥T) ↦ f (↑i : ι) a

Tactic:
Kernel.iIndepFun.indepFun_finset S T hST hf_Indep hf_meas

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_finset, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun (β := β) f μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) μ
⊢ ∀ (i : ι),
    AEMeasurable (_m := _mΩ) (f i)
      (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
        (⇑(Kernel.const Unit μ) : (a : Unit) → Measure Ω))

Tactic:
simp [hf_meas]
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_Indep : iIndepFun (β := β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ (fun (a : Ω) ↦ (f i a, f j a)) ⟂ᵢ[μ] f k

Tactic:
Kernel.iIndepFun.indepFun_prodMk hf_Indep hf_meas i j k hik hjk

Premises used: ProbabilityTheory.IndepFun, ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_Indep : iIndepFun (β := β) f μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) μ
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ ∀ (i : ι),
    AEMeasurable (_m := _mΩ) (f i)
      (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
        (⇑(Kernel.const Unit μ) : (a : Unit) → Measure Ω))

Tactic:
simp [hf_meas]
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h_indep : iIndepFun (β := β) f μ
hf : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ (fun (a : Ω) ↦ (f i a, f j a)) ⟂ᵢ[μ] fun (a : Ω) ↦ (f k a, f l a)

Tactic:
Kernel.iIndepFun.indepFun_prodMk_prodMk h_indep hf i j k l hik hil hjk hjl

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h_indep : iIndepFun (β := β) f μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ ∀ (i : ι),
    AEMeasurable (_m := _mΩ) (f i)
      (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
        (⇑(Kernel.const Unit μ) : (a : Unit) → Measure Ω))

Tactic:
simp [hf]
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ β (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → β i) f) μ
rw :
  ∀ (s : Finset ι) {f' : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (f' i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f' i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f' i) : ℝ≥0∞)
⊢ iIndepFun (β := β) f μ

Tactic:
rw [iIndepFun_iff]

Premises used: ProbabilityTheory.iIndepFun_iff
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f_1 : (i : ι) → Ω → β i
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ β (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → β i) f_1) μ
s : Finset ι
f : ι → Set Ω
hs : ∀ i ∈ s, MeasurableSet (f i)
h₁ : ∀ (x : Ω), Membership.mem (γ := Set Ω) (⋂ i ∈ s, f i) x ↔ Membership.mem (γ := Set Ω) (⋂ (i : ↥s), f (↑i : ι)) x
⊢ Eq.{u_1 + 1} (α := Set Ω) (⋂ i ∈ s, f i) (⋂ (i : ↥s), f (↑i : ι))

Tactic:
ext
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f_1 : (i : ι) → Ω → β i
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ β (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → β i) f_1) μ
s : Finset ι
f : ι → Set Ω
hs : ∀ i ∈ s, MeasurableSet (f i)
x : Ω
⊢ Membership.mem (γ := Set Ω) (⋂ i ∈ s, f i) x ↔ Membership.mem (γ := Set Ω) (⋂ (i : ↥s), f (↑i : ι)) x

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f_1 : (i : ι) → Ω → β i
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ β (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → β i) f_1) μ
s : Finset ι
f : ι → Set Ω
hs : ∀ i ∈ s, MeasurableSet (f i)
⊢ Eq.{u_1 + 1} (α := Set Ω) (⋂ i ∈ s, f i) (⋂ (i : ↥s), f (↑i : ι))

Tactic:
have : ⋂ i ∈ s, f i = ⋂ i : s, f i := by ext; simp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f_1 : (i : ι) → Ω → β i
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ β (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → β i) f_1) μ
s : Finset ι
f : ι → Set Ω
hs : ∀ i ∈ s, MeasurableSet (f i)
this : Eq.{u_1 + 1} (α := Set Ω) (⋂ i ∈ s, f i) (⋂ (i : ↥s), f (↑i : ι))
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ↥s), f (↑i : ι)) : ℝ≥0∞)
    (∏ i : ↥s, (μ : (a : Set Ω) → ℝ≥0∞) (f (↑i : ι)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
rw [← Finset.prod_coe_sort, this]

Premises used: Finset.prod_coe_sort
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f_1 : (i : ι) → Ω → β i
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ β (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → β i) f_1) μ
s : Finset ι
f : ι → Set Ω
hs : ∀ i ∈ s, MeasurableSet (f i)
this : Eq.{u_1 + 1} (α := Set Ω) (⋂ i ∈ s, f i) (⋂ (i : ↥s), f (↑i : ι))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ↥s), f (↑i : ι)) : ℝ≥0∞)
    (∏ i : ↥s, (μ : (a : Set Ω) → ℝ≥0∞) (f (↑i : ι)) : ℝ≥0∞)

Tactic:
(h s).meas_iInter fun i ↦ hs i i.2

Premises used: ProbabilityTheory.iIndepFun.meas_iInter, Subtype.val, Subtype.property
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f_1 : (i : ι) → Ω → β i
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ β (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → β i) f_1) μ
s : Finset ι
f : ι → Set Ω
hs : ∀ i ∈ s, MeasurableSet (f i)
this : Eq.{u_1 + 1} (α := Set Ω) (⋂ i ∈ s, f i) (⋂ (i : ↥s), f (↑i : ι))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ↥s), f (↑i : ι)) : ℝ≥0∞)
    (∏ i : ↥s, (μ : (a : Set Ω) → ℝ≥0∞) (f (↑i : ι)) : ℝ≥0∞)

Tactic:
exact (h s).meas_iInter fun i ↦ hs i i.2

Premises used: ProbabilityTheory.iIndepFun.meas_iInter, Subtype.val, Subtype.property
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h : iIndepFun (β := β) f μ
⊢ IsProbabilityMeasure μ

Tactic:
have := h.isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h : iIndepFun (β := β) f μ
this : IsProbabilityMeasure μ
⊢ ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)

Tactic:
rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h

Premises used: ProbabilityTheory.iIndepFun_iff_measure_inter_preimage_eq_mul
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h : iIndepFun (β := β) f μ
this : IsProbabilityMeasure μ
h₁ :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
⊢ IsProbabilityMeasure μ

Tactic:
rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h

Premises used: ProbabilityTheory.iIndepFun_iff_measure_inter_preimage_eq_mul
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
this : IsProbabilityMeasure μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
left :
  Eq (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i))
    (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (s i))
right :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' s i) : ℝ≥0∞)
    ((Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ : (a : Set ((i : ι) → β i)) → ℝ≥0∞) (Set.pi (α := β) univ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i))
      (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (s i)) ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' s i) : ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ : (a : Set ((i : ι) → β i)) → ℝ≥0∞) (Set.pi (α := β) univ s) : ℝ≥0∞)

Tactic:
constructor
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
this : IsProbabilityMeasure μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
left :
  ∀ (x : ι),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x) : ℝ≥0∞)
      (((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) (s x) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i))
    (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (s i))

Tactic:
congr with x
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
this : IsProbabilityMeasure μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
x : ι
left left₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x) : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x) : ℝ≥0∞)
    (((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) (s x) : ℝ≥0∞)

Tactic:
rw [Measure.map_apply_of_aemeasurable (hf x) (hm x)]

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
this : IsProbabilityMeasure μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
right :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' s i) : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) ((fun (c : Ω) (x : ι) ↦ f x c) ⁻¹' Set.pi (α := β) univ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' s i) : ℝ≥0∞)
    ((Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ : (a : Set ((i : ι) → β i)) → ℝ≥0∞) (Set.pi (α := β) univ s) : ℝ≥0∞)

Tactic:
rw [Measure.map_apply_of_aemeasurable (aemeasurable_pi_lambda _ fun x ↦ hf x)
        (.univ_pi hm)]

Premises used: aemeasurable_pi_lambda, MeasureTheory.Measure.map_apply_of_aemeasurable, MeasurableSet.univ_pi
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
this : IsProbabilityMeasure μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
right :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω) (⋂ (i : ι), f i ⁻¹' s i) x ↔
      Membership.mem (γ := Set Ω) ((fun (c : Ω) (x : ι) ↦ f x c) ⁻¹' Set.pi (α := β) univ s) x
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' s i) : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) ((fun (c : Ω) (x : ι) ↦ f x c) ⁻¹' Set.pi (α := β) univ s) : ℝ≥0∞)

Tactic:
congr with x