awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_11
inst : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst_2 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
⊢ iIndepFun (β := 𝓧) (fun (i : ι) (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ)

Tactic:
iIndepFun_iff_map_fun_eq_pi_map ?_ |>.2 ?_

Premises used: Iff.mpr, ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_11
inst : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst_2 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
refine_1 : ∀ (i : ι), AEMeasurable (β := 𝓧 i) (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ)
refine_2 :
  Eq (α := Measure ((i : ι) → 𝓧 i)) (Measure.map (fun (ω : (i : ι) → Ω i) (i : ι) ↦ X i (ω i)) (Measure.pi (α := Ω) μ))
    (Measure.pi (α := 𝓧) fun (i : ι) ↦ Measure.map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ))
⊢ iIndepFun (β := 𝓧) (fun (i : ι) (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ)

Tactic:
refine iIndepFun_iff_map_fun_eq_pi_map ?_ |>.2 ?_

Premises used: Iff.mpr, ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_11
inst : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst_2 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
⊢ ∀ (i : ι), AEMeasurable (β := 𝓧 i) (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ)

Tactic:
fun i ↦ (mX i).comp_quasiMeasurePreserving (Measure.quasiMeasurePreserving_eval _ i)

Premises used: AEMeasurable.comp_quasiMeasurePreserving, MeasureTheory.Measure.quasiMeasurePreserving_eval
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_11
inst : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst_2 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
⊢ ∀ (i : ι), AEMeasurable (β := 𝓧 i) (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ)

Tactic:
exact fun i ↦ (mX i).comp_quasiMeasurePreserving (Measure.quasiMeasurePreserving_eval _ i)

Premises used: AEMeasurable.comp_quasiMeasurePreserving, MeasureTheory.Measure.quasiMeasurePreserving_eval
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_11
inst : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst_2 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
refine_2 :
  Eq (α := Measure ((i : ι) → 𝓧 i)) (Measure.pi (α := 𝓧) fun (i : ι) ↦ Measure.map (X i) (μ i))
    (Measure.pi (α := 𝓧) fun (i : ι) ↦ Measure.map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ))
⊢ Eq (α := Measure ((i : ι) → 𝓧 i)) (Measure.map (fun (ω : (i : ι) → Ω i) (i : ι) ↦ X i (ω i)) (Measure.pi (α := Ω) μ))
    (Measure.pi (α := 𝓧) fun (i : ι) ↦ Measure.map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ))

Tactic:
rw [Measure.pi_map_pi mX]

Premises used: MeasureTheory.Measure.pi_map_pi
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_11
inst : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst_2 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
refine_2 :
  Eq (α := (i : ι) → Measure (𝓧 i)) (fun (i : ι) ↦ Measure.map (X i) (μ i)) fun (i : ι) ↦
    Measure.map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ)
⊢ Eq (α := Measure ((i : ι) → 𝓧 i)) (Measure.pi (α := 𝓧) fun (i : ι) ↦ Measure.map (X i) (μ i))
    (Measure.pi (α := 𝓧) fun (i : ι) ↦ Measure.map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ))

Tactic:
congr
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_11
inst : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst_2 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
refine_2 :
  ∀ (i : ι),
    Eq (α := Measure (𝓧 i)) (Measure.map (X i) (μ i))
      (Measure.map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ))
⊢ Eq (α := (i : ι) → Measure (𝓧 i)) (fun (i : ι) ↦ Measure.map (X i) (μ i)) fun (i : ι) ↦
    Measure.map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ)

Tactic:
ext i : 1
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_11
inst : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst_2 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
i : ι
refine_2 : AEMeasurable (_m := mΩ i) (X i) (Measure.map (Function.eval (β := Ω) i) (Measure.pi (α := Ω) μ))
refine_2₁ : AEMeasurable (Function.eval (β := Ω) i) (Measure.pi (α := Ω) μ)
⊢ Eq (α := Measure (𝓧 i)) (Measure.map (X i) (μ i))
    (Measure.map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ))

Tactic:
rw [← (measurePreserving_eval μ i).map_eq, AEMeasurable.map_map_of_aemeasurable,
    Function.comp_def]

Premises used: MeasureTheory.measurePreserving_eval, MeasureTheory.MeasurePreserving.map_eq, Function.comp_def, AEMeasurable.map_map_of_aemeasurable
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_11
inst : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst_2 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
i : ι
refine_2 : AEMeasurable (X i) (μ i)
⊢ AEMeasurable (_m := mΩ i) (X i) (Measure.map (Function.eval (β := Ω) i) (Measure.pi (α := Ω) μ))

Tactic:
rw [(measurePreserving_eval μ i).map_eq]

Premises used: MeasureTheory.measurePreserving_eval, MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_11
inst : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst_2 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
i : ι
⊢ AEMeasurable (X i) (μ i)

Tactic:
mX i
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_11
inst : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst_2 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
i : ι
⊢ AEMeasurable (X i) (μ i)

Tactic:
exact mX i
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_11
inst : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst_2 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
i : ι
⊢ AEMeasurable (Function.eval (β := Ω) i) (Measure.pi (α := Ω) μ)

Tactic:
(measurable_pi_apply i).aemeasurable

Premises used: Measurable.aemeasurable, measurable_pi_apply
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_11
inst : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst_2 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
i : ι
⊢ AEMeasurable (Function.eval (β := Ω) i) (Measure.pi (α := Ω) μ)

Tactic:
exact (measurable_pi_apply i).aemeasurable

Premises used: Measurable.aemeasurable, measurable_pi_apply
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ (f i * f j) ⟂ᵢ[μ] f k

Tactic:
Kernel.iIndepFun.indepFun_mul_left hf_indep hf_meas i j k hik hjk

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_left, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) 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 : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hij : i ≠ j
hik : i ≠ k
⊢ f i ⟂ᵢ[μ] f j * f k

Tactic:
Kernel.iIndepFun.indepFun_mul_right hf_indep hf_meas i j k hij hik

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_right, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) μ
i j k : ι
hij : i ≠ j
hik : i ≠ 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 : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ (f i * f j) ⟂ᵢ[μ] f k * f l

Tactic:
Kernel.iIndepFun.indepFun_mul_mul hf_indep hf_meas i j k l hik hil hjk hjl

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_mul, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst : Mul β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (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_meas]
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ (f i / f j) ⟂ᵢ[μ] f k

Tactic:
Kernel.iIndepFun.indepFun_div_left hf_indep hf_meas i j k hik hjk

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_div_left, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) 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 : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hij : i ≠ j
hik : i ≠ k
⊢ f i ⟂ᵢ[μ] f j / f k

Tactic:
Kernel.iIndepFun.indepFun_div_right hf_indep hf_meas i j k hij hik

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_div_right, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) μ
i j k : ι
hij : i ≠ j
hik : i ≠ 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 : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ (f i / f j) ⟂ᵢ[μ] f k / f l

Tactic:
Kernel.iIndepFun.indepFun_div_div hf_indep hf_meas i j k l hik hil hjk hjl

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_div_div, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst : Div β
inst_1 : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (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_meas]
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
⊢ (∏ j ∈ s, f j) ⟂ᵢ[μ] f i

Tactic:
Kernel.iIndepFun.indepFun_finsetProd_of_notMem hf_Indep hf_meas hi

Premises used: ProbabilityTheory.IndepFun, ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMem
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) μ
s : Finset ι
i : ι
hi : i ∉ s
⊢ ∀ (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
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ℕ → Ω → β
hf_Indep : iIndepFun (β := fun (x : ℕ) ↦ β) f μ
hf_meas : ∀ (i : ℕ), Measurable (f i)
n : ℕ
⊢ (∏ j ∈ Finset.range n, f j) ⟂ᵢ[μ] f n

Tactic:
Kernel.iIndepFun.indepFun_prod_range_succ hf_Indep hf_meas n

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_range_succ, ProbabilityTheory.IndepFun
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ℕ → Ω → β
hf_Indep : iIndepFun (β := fun (x : ℕ) ↦ β) f μ
hf_meas : ∀ (i : ℕ), AEMeasurable (f i) μ
n : ℕ
⊢ n ∉ Finset.range n

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
β : Type u_6
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s μ
⊢ iIndepFun (β := fun (n : ι) ↦ β) (fun (n : ι) ↦ (s n).indicator fun (_ω : Ω) ↦ 1) μ

Tactic:
Kernel.iIndepSet.iIndepFun_indicator hs

Premises used: ProbabilityTheory.iIndepFun, ProbabilityTheory.Kernel.iIndepSet.iIndepFun_indicator
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ IsProbabilityMeasure μ

Tactic:
have : IsProbabilityMeasure (μ : Measure Ω) := hindep.isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
intro :
  ∀ (val : Fintype ι),
    Eq (α := ℝ≥0∞) (μ[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (∏ i ∈ s, μ[f i | Y i ⁻¹' t i] : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (μ[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ℝ≥0∞) (∏ i ∈ s, μ[f i | Y i ⁻¹' t i] : ℝ≥0∞)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hms : MeasurableSet.{u_7} (α := Ω) (⋂ (i : ι), Y i ⁻¹' t i)
⊢ μ[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) : ℝ≥0∞)

Tactic:
rw [cond_apply]

Premises used: ProbabilityTheory.cond_apply
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ MeasurableSet.{u_7} (α := Ω) (⋂ (i : ι), Y i ⁻¹' t i)

Tactic:
.iInter fun i ↦ hY i (ht i)

Premises used: MeasurableSet.iInter
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ MeasurableSet.{u_7} (α := Ω) (⋂ (i : ι), Y i ⁻¹' t i)

Tactic:
exact .iInter fun i ↦ hY i (ht i)
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
e_a : Eq.{u_7 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) (⋂ (i : ι), g i)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), Y i ⁻¹' t i))⁻¹ : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), g i) : ℝ≥0∞)

Tactic:
congr
-- Module: Mathlib.Probability.Independence.Basic
Goal:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (Y i ⁻¹' t i) : ℝ≥0∞) (0 : ℝ≥0∞)
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ Eq.{u_7 + 1} (α := Set Ω) ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ i ∈ s, f i)
    ((⋂ (i : ι), Y i ⁻¹' t i) ∩ ⋂ (i : ι), if i ∈ s then f i else univ)

Tactic:
simp only [Set.iInter_ite, Set.iInter_univ, Set.inter_univ]

Premises used: Set.inter_univ, Set.iInter_univ, Set.iInter_ite