awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
n : ℕ
⊢ Indep (generateFrom {s (n + 1)}) (generateFrom {t : Set Ω | ∃ k ≤ n, s k = t}) μ

Tactic:
Kernel.iIndepSet.indep_generateFrom_le_nat hsm hs n

Premises used: ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le_nat, ProbabilityTheory.Indep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
m1 _mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : SemilatticeSup ι
inst_1 : IsZeroOrProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m1 μ
h_le : ∀ (i : ι), m i ≤ _mΩ
h_le' : m1 ≤ _mΩ
hm : Monotone m
⊢ Indep (⨆ (i : ι), m i) m1 μ

Tactic:
Kernel.indep_iSup_of_monotone h_indep h_le h_le' hm

Premises used: ProbabilityTheory.Kernel.indep_iSup_of_monotone, ProbabilityTheory.Indep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
m1 _mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : SemilatticeInf ι
inst_1 : IsZeroOrProbabilityMeasure μ
h_indep : ∀ (i : ι), Indep (m i) m1 μ
h_le : ∀ (i : ι), m i ≤ _mΩ
h_le' : m1 ≤ _mΩ
hm : Antitone m
⊢ Indep (⨆ (i : ι), m i) m1 μ

Tactic:
Kernel.indep_iSup_of_antitone h_indep h_le h_le' hm

Premises used: ProbabilityTheory.Indep, ProbabilityTheory.Kernel.indep_iSup_of_antitone
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π μ
haS : a ∉ S
⊢ IndepSets (piiUnionInter π (↑S : Set ι)) (π a) μ

Tactic:
Kernel.iIndepSets.piiUnionInter_of_notMem hp_ind haS

Premises used: ProbabilityTheory.IndepSets, ProbabilityTheory.Kernel.iIndepSets.piiUnionInter_of_notMem
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
μ : Measure Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π μ
⊢ ProbabilityTheory.iIndep m μ

Tactic:
Kernel.iIndepSets.iIndep m h_le π h_pi h_generate h_ind

Premises used: ProbabilityTheory.Kernel.iIndepSets.iIndep, ProbabilityTheory.iIndep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
s t : Set Ω
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
⊢ IndepSet s t μ ↔ IndepSets {s} {t} μ

Tactic:
Kernel.indepSet_iff_indepSets_singleton hs_meas ht_meas _ _

Premises used: ProbabilityTheory.IndepSet, ProbabilityTheory.IndepSets, ProbabilityTheory.Kernel.indepSet_iff_indepSets_singleton
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
s t : Set Ω
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
⊢ IndepSet s t μ ↔
    (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
(indepSet_iff_indepSets_singleton hs_meas ht_meas μ).trans indepSets_singleton_iff

Premises used: ProbabilityTheory.indepSets_singleton_iff, Iff.trans, ProbabilityTheory.indepSet_iff_indepSets_singleton
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
s t : Set Ω
μ : Measure Ω
h : IndepSet s t μ
⊢ (μ : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simpa using Kernel.IndepSet.measure_inter_eq_mul _ _ h

Premises used: ProbabilityTheory.Kernel.IndepSet.measure_inter_eq_mul
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
s t : Set Ω
S T : Set (Set Ω)
hs : s ∈ S
ht : t ∈ T
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
h_indep : IndepSets S T μ
⊢ IndepSet s t μ

Tactic:
Kernel.IndepSets.indepSet_of_mem _ _ hs ht hs_meas ht_meas _ _ h_indep

Premises used: ProbabilityTheory.IndepSet, ProbabilityTheory.Kernel.IndepSets.indepSet_of_mem
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
m₁ m₂ _mΩ : MeasurableSpace Ω
μ : Measure Ω
h_indep : Indep m₁ m₂ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ IndepSet s t μ

Tactic:
Kernel.Indep.indepSet_of_measurableSet h_indep hs ht

Premises used: ProbabilityTheory.IndepSet, ProbabilityTheory.Kernel.Indep.indepSet_of_measurableSet
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
m₁ m₂ _mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ Indep m₁ m₂ μ ↔ ∀ (s t : Set Ω), MeasurableSet s → MeasurableSet t → IndepSet s t μ

Tactic:
Kernel.indep_iff_forall_indepSet m₁ m₂ _ _

Premises used: ProbabilityTheory.IndepSet, ProbabilityTheory.Kernel.indep_iff_forall_indepSet, ProbabilityTheory.Indep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : ι → Set Ω
⊢ iIndep (fun (i : ι) ↦ MeasurableSpace.comap (β := Prop) (fun (x : Ω) ↦ x ∈ f i) ⊤) μ ↔ iIndepSet f μ

Tactic:
Kernel.iIndep_comap_mem_iff

Premises used: ProbabilityTheory.iIndepSet, ProbabilityTheory.Kernel.iIndep_comap_mem_iff, ProbabilityTheory.iIndep
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set Ω
simp_rw :
  Kernel.iIndepSets (_mα := PUnit.instMeasurableSpace) (fun (i : ι) ↦ {s i}) (Kernel.const Unit μ) (Measure.dirac ()) ↔
    ∀ (t : Finset ι),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ t, s i) : ℝ≥0∞) (∏ i ∈ t, (μ : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₁ :
  (∀ (S : Finset ι),
      ∀ᵐ (a : Unit) ∂Measure.dirac (),
        Eq (α := ℝ≥0∞)
          ((((Kernel.const Unit μ : (a : Unit) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
          (∏ i ∈ S, (((Kernel.const Unit μ : (a : Unit) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) :
            ℝ≥0∞)) ↔
    ∀ (t : Finset ι),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ t, s i) : ℝ≥0∞) (∏ i ∈ t, (μ : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₂ :
  (∀ (S : Finset ι),
      ∀ᶠ (a : Unit) in pure (),
        Eq (α := ℝ≥0∞)
          ((((Kernel.const Unit μ : (a : Unit) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
          (∏ i ∈ S, (((Kernel.const Unit μ : (a : Unit) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) :
            ℝ≥0∞)) ↔
    ∀ (t : Finset ι),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ t, s i) : ℝ≥0∞) (∏ i ∈ t, (μ : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₃ :
  (∀ (S : Finset ι),
      Eq (α := ℝ≥0∞)
        ((((Kernel.const Unit μ : (a : Unit) → Measure Ω) () : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, s i) : ℝ≥0∞)
        (∏ i ∈ S, (((Kernel.const Unit μ : (a : Unit) → Measure Ω) () : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s i) :
          ℝ≥0∞)) ↔
    ∀ (t : Finset ι),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ t, s i) : ℝ≥0∞) (∏ i ∈ t, (μ : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ iIndepSets (fun (i : ι) ↦ {s i}) μ ↔
    ∀ (t : Finset ι),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ t, s i) : ℝ≥0∞) (∏ i ∈ t, (μ : (a : Set Ω) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
simp_rw [iIndepSets, Kernel.iIndepSets_singleton_iff, ae_dirac_eq, Filter.eventually_pure,
    Kernel.const_apply]

Premises used: MeasureTheory.ae_dirac_eq, Filter.eventually_pure, ProbabilityTheory.Kernel.iIndepSets_singleton_iff, ProbabilityTheory.iIndepSets, ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : ι → Set Ω
h : iIndepSet f μ
s : Finset ι
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
simpa using Kernel.iIndepSet.meas_biInter h s

Premises used: ProbabilityTheory.Kernel.iIndepSet.meas_biInter
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : ι → Set Ω
hf : ∀ (i : ι), MeasurableSet (f i)
⊢ iIndepSet f μ ↔ iIndepSets (fun (i : ι) ↦ {f i}) μ

Tactic:
Kernel.iIndepSet_iff_iIndepSets_singleton hf

Premises used: ProbabilityTheory.iIndepSet, ProbabilityTheory.iIndepSets, ProbabilityTheory.Kernel.iIndepSet_iff_iIndepSets_singleton
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : ι → Set Ω
hf : ∀ (i : ι), MeasurableSet (f i)
simp_rw :
  Kernel.iIndepSet (_mα := PUnit.instMeasurableSpace) f (Kernel.const Unit μ) (Measure.dirac ()) ↔
    ∀ (s : Finset ι),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
simp_rw₁ :
  (∀ (s : Finset ι),
      ∀ᵐ (a : Unit) ∂Measure.dirac (),
        Eq (α := ℝ≥0∞)
          ((((Kernel.const Unit μ : (a : Unit) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
          (∏ i ∈ s, (((Kernel.const Unit μ : (a : Unit) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) :
            ℝ≥0∞)) ↔
    ∀ (s : Finset ι),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
simp_rw₂ :
  (∀ (s : Finset ι),
      ∀ᶠ (a : Unit) in pure (),
        Eq (α := ℝ≥0∞)
          ((((Kernel.const Unit μ : (a : Unit) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
          (∏ i ∈ s, (((Kernel.const Unit μ : (a : Unit) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) :
            ℝ≥0∞)) ↔
    ∀ (s : Finset ι),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
simp_rw₃ :
  (∀ (s : Finset ι),
      Eq (α := ℝ≥0∞)
        ((((Kernel.const Unit μ : (a : Unit) → Measure Ω) () : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
        (∏ i ∈ s, (((Kernel.const Unit μ : (a : Unit) → Measure Ω) () : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) :
          ℝ≥0∞)) ↔
    ∀ (s : Finset ι),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ iIndepSet f μ ↔
    ∀ (s : Finset ι),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
simp_rw [iIndepSet, Kernel.iIndepSet_iff_meas_biInter hf, ae_dirac_eq, Filter.eventually_pure,
    Kernel.const_apply]

Premises used: ProbabilityTheory.Kernel.iIndepSet_iff_meas_biInter, ProbabilityTheory.iIndepSet, MeasureTheory.ae_dirac_eq, Filter.eventually_pure, ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
π : ι → Set (Set Ω)
f : ι → Set Ω
hfπ : ∀ (i : ι), f i ∈ π i
hf : ∀ (i : ι), MeasurableSet (f i)
hπ : iIndepSets π μ
⊢ iIndepSet f μ

Tactic:
Kernel.iIndepSets.iIndepSet_of_mem hfπ hf hπ

Premises used: ProbabilityTheory.iIndepSet, ProbabilityTheory.Kernel.iIndepSets.iIndepSet_of_mem
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
⊢ f ⟂ᵢ[μ] g ↔
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)

Tactic:
simp only [IndepFun, Kernel.indepFun_iff_measure_inter_preimage_eq_mul, ae_dirac_eq,
    Filter.eventually_pure, Kernel.const_apply]

Premises used: ProbabilityTheory.Kernel.indepFun_iff_measure_inter_preimage_eq_mul, MeasureTheory.ae_dirac_eq, Filter.eventually_pure, ProbabilityTheory.IndepFun, ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_10
β : ι → Type u_11
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
⊢ iIndepFun (β := β) f μ ↔
    ∀ (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:
simp only [iIndepFun, Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul, ae_dirac_eq,
    Filter.eventually_pure, Kernel.const_apply]

Premises used: ProbabilityTheory.iIndepFun, MeasureTheory.ae_dirac_eq, Filter.eventually_pure, ProbabilityTheory.Kernel.const_apply, ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
h : ∀ (i : ι), f i =ᶠ[ae μ] g i
⊢ ∀ (i : ι),
    ∀ᵐ (a : Unit) ∂Measure.dirac (),
      f i =ᶠ[ae (F := Measure Ω) ((Kernel.const Unit μ : (a : Unit) → Measure Ω) a : Measure Ω)] g i

Tactic:
simp [h]
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
γ : ι → Type u_11
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h : iIndepFun (β := β) f μ
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
⊢ iIndepFun (β := γ) (fun (i : ι) ↦ g i ∘ f i) μ

Tactic:
h.comp _ hg

Premises used: ProbabilityTheory.iIndepFun, ProbabilityTheory.Kernel.iIndepFun.comp
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
γ : ι → Type u_11
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h : iIndepFun (β := β) f μ
g : (i : ι) → β i → γ i
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ (i : ι), AEMeasurable (_m := mβ i) (g i) (Measure.map (f i) μ)
⊢ ∀ (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
γ : ι → Type u_11
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h : iIndepFun (β := β) f μ
g : (i : ι) → β i → γ i
hf : ∀ (i : ι), AEMeasurable (f i) μ
hg : ∀ (i : ι), AEMeasurable (_m := mβ i) (g i) (Measure.map (f i) μ)
⊢ ∀ (i : ι),
    AEMeasurable (_m := mβ i) (g i)
      (Measure.map (f i)
        (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
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst : IsZeroOrProbabilityMeasure μ
hf : Measurable f
hg : Measurable g
⊢ f ⟂ᵢ[μ] g ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) μ

Tactic:
simp only [IndepFun, IndepSet, Kernel.indepFun_iff_indepSet_preimage hf hg]

Premises used: ProbabilityTheory.IndepSet, ProbabilityTheory.IndepFun, ProbabilityTheory.Kernel.indepFun_iff_indepSet_preimage
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
rw :
  (∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)) ↔
    Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ))
⊢ f ⟂ᵢ[μ] g ↔
    Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ))

Tactic:
rw [indepFun_iff_measure_inter_preimage_eq_mul]

Premises used: ProbabilityTheory.indepFun_iff_measure_inter_preimage_eq_mul
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
rw₁ rw₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [Measure.map_apply_of_aemeasurable hf hs, Measure.map_apply_of_aemeasurable hg ht]

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
⊢ ∀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) : ℝ≥0∞)
        ((Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)

Tactic:
have h₀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) :
      μ (f ⁻¹' s) * μ (g ⁻¹' t) = μ.map f s * μ.map g t ∧
      μ (f ⁻¹' s ∩ g ⁻¹' t) = μ.map (fun ω ↦ (f ω, g ω)) (s ×ˢ t) :=
    ⟨by rw [Measure.map_apply_of_aemeasurable hf hs, Measure.map_apply_of_aemeasurable hg ht],
      (Measure.map_apply_of_aemeasurable (hf.prodMk hg) (hs.prod ht)).symm⟩
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) : ℝ≥0∞)
        ((Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
mp :
  (∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)) →
    Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ))
mpr :
  Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ)) →
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
⊢ (∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)) ↔
    Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ))

Tactic:
constructor
-- Module: Mathlib.Probability.Independence.Basic
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) : ℝ≥0∞)
        ((Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
⊢ (∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)) →
    Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ))

Tactic:
fun h ↦ (Measure.prod_eq fun s t hs ht ↦ ?_).symm

Premises used: MeasureTheory.Measure.prod_eq, Eq.symm