awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.IdentDistribIndep (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
this : IsFiniteMeasure ν
rw :
  Eq (α := Measure (E × F)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
    (Measure.map (fun (ω' : Ω') ↦ (Z ω', W ω')) ν)
⊢ Eq (α := Measure (E × F)) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) μ) (Measure.map (fun (ω' : Ω') ↦ (Z ω', W ω')) ν)
have rw₁ : Eq (α := Measure (E × F)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
  (Measure.prod (Measure.map Z ν) (Measure.map W ν))
Tactic: rw [hXY.map_prod_eq_prod_map_map hXZ.aemeasurable_fst hYW.aemeasurable_fst,
      hZW.map_prod_eq_prod_map_map hXZ.aemeasurable_snd hYW.aemeasurable_snd,
      hXZ.map_eq, hYW.map_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistribIndep (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
this : IsFiniteMeasure ν
rw :
  Eq (α := Measure (E × F)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
    (Measure.map (fun (ω' : Ω') ↦ (Z ω', W ω')) ν)
rw₁ :
  Eq (α := Measure (E × F)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
    (Measure.prod (Measure.map Z ν) (Measure.map W ν))
⊢ Eq (α := Measure (E × F)) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) μ) (Measure.map (fun (ω' : Ω') ↦ (Z ω', W ω')) ν)
have rw₂ : Eq (α := Measure (E × F)) (Measure.prod (Measure.map Z ν) (Measure.map Y μ))
  (Measure.prod (Measure.map Z ν) (Measure.map W ν))
Tactic: rw [hXY.map_prod_eq_prod_map_map hXZ.aemeasurable_fst hYW.aemeasurable_fst,
      hZW.map_prod_eq_prod_map_map hXZ.aemeasurable_snd hYW.aemeasurable_snd,
      hXZ.map_eq, hYW.map_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistribIndep (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
E : Type u_4
F : Type u_5
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure Ω
ν : Measure Ω'
inst : IsFiniteMeasure μ
X : Ω → E
Y : Ω → F
Z : Ω' → E
W : Ω' → F
hXZ : IdentDistrib X Z μ ν
hYW : IdentDistrib Y W μ ν
hXY : X ⟂ᵢ[μ] Y
hZW : Z ⟂ᵢ[ν] W
this : IsFiniteMeasure ν
rw :
  Eq (α := Measure (E × F)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
    (Measure.map (fun (ω' : Ω') ↦ (Z ω', W ω')) ν)
rw₁ :
  Eq (α := Measure (E × F)) (Measure.prod (Measure.map X μ) (Measure.map Y μ))
    (Measure.prod (Measure.map Z ν) (Measure.map W ν))
rw₂ :
  Eq (α := Measure (E × F)) (Measure.prod (Measure.map Z ν) (Measure.map Y μ))
    (Measure.prod (Measure.map Z ν) (Measure.map W ν))
⊢ Eq (α := Measure (E × F)) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) μ) (Measure.map (fun (ω' : Ω') ↦ (Z ω', W ω')) ν)
have rw₃ : Eq (α := Measure (E × F)) (Measure.prod (Measure.map Z ν) (Measure.map W ν))
  (Measure.prod (Measure.map Z ν) (Measure.map W ν))
Tactic: rw [hXY.map_prod_eq_prod_map_map hXZ.aemeasurable_fst hYW.aemeasurable_fst,
      hZW.map_prod_eq_prod_map_map hXZ.aemeasurable_snd hYW.aemeasurable_snd,
      hXZ.map_eq, hYW.map_eq]
-- Lean 4 proof step from Mathlib.Probability.IdentDistribIndep (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun (β := E) X μ
hY_ind : iIndepFun (β := E) Y ν
⊢ Eq (α := Measure ((x : ι) → E x)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) μ)
    (Measure.map (fun (ω : Ω') (x : ι) ↦ Y x ω) ν)
have this : IsProbabilityMeasure μ
Tactic: have : IsProbabilityMeasure μ := hX_ind.isProbabilityMeasure
-- Lean 4 proof step from Mathlib.Probability.IdentDistribIndep (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun (β := E) X μ
hY_ind : iIndepFun (β := E) Y ν
this : IsProbabilityMeasure μ
⊢ Eq (α := Measure ((x : ι) → E x)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) μ)
    (Measure.map (fun (ω : Ω') (x : ι) ↦ Y x ω) ν)
have this₁ : IsProbabilityMeasure ν
Tactic: have : IsProbabilityMeasure ν := hY_ind.isProbabilityMeasure
-- Lean 4 proof step from Mathlib.Probability.IdentDistribIndep (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun (β := E) X μ
hY_ind : iIndepFun (β := E) Y ν
this_1 : IsProbabilityMeasure μ
this : IsProbabilityMeasure ν
⊢ Eq (α := Measure ((x : ι) → E x)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) μ)
    (Measure.map (fun (ω : Ω') (x : ι) ↦ Y x ω) ν)
have rw : Eq (α := Measure ((x : ι) → E x)) (Measure.infinitePi (X := E) fun (i : ι) ↦ Measure.map (X i) μ)
  (Measure.infinitePi (X := E) fun (i : ι) ↦ Measure.map (Y i) ν)
Tactic: rw [(iIndepFun_iff_map_fun_eq_infinitePi_map₀' (fun i ↦ (h i).aemeasurable_fst)).mp hX_ind,
      (iIndepFun_iff_map_fun_eq_infinitePi_map₀' (fun i ↦ (h i).aemeasurable_snd)).mp hY_ind]
-- Lean 4 proof step from Mathlib.Probability.IdentDistribIndep (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun (β := E) X μ
hY_ind : iIndepFun (β := E) Y ν
this_1 : IsProbabilityMeasure μ
this : IsProbabilityMeasure ν
⊢ Eq (α := Measure ((x : ι) → E x)) (Measure.infinitePi (X := E) fun (i : ι) ↦ Measure.map (X i) μ)
    (Measure.infinitePi (X := E) fun (i : ι) ↦ Measure.map (Y i) ν)
have e_μ : ∀ (i : ι) (s : Set (E i)),
  MeasurableSet s →
    Eq (α := ENNReal) (((Measure.map (X i) μ : Measure (E i)) : (a : Set (E i)) → ENNReal) s : ENNReal)
      (((Measure.map (Y i) ν : Measure (E i)) : (a : Set (E i)) → ENNReal) s : ENNReal)
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Probability.IdentDistribIndep (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun (β := E) X μ
hY_ind : iIndepFun (β := E) Y ν
this_1 : IsProbabilityMeasure μ
this : IsProbabilityMeasure ν
i : ι
s : Set (E i)
h_1 : MeasurableSet s
⊢ Eq (α := ENNReal) (((Measure.map (X i) μ : Measure (E i)) : (a : Set (E i)) → ENNReal) s : ENNReal)
    (((Measure.map (Y i) ν : Measure (E i)) : (a : Set (E i)) → ENNReal) s : ENNReal)
have e_μ : Eq (α := ENNReal) (((Measure.map (Y i) ν : Measure (E i)) : (a : Set (E i)) → ENNReal) s : ENNReal)
  (((Measure.map (Y i) ν : Measure (E i)) : (a : Set (E i)) → ENNReal) s : ENNReal)
Tactic: rw [(h i).map_eq]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ iIndep m μ ↔
    ∀ (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∞)
have simp : (∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s, Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (f i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)) ↔
  ∀ (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∞)
Tactic: simp only [iIndep_iff_iIndepSets, iIndepSets_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
m₁ m₂ _mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ Indep m₁ m₂ μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
have rw : (∀ (t1 t2 : Set Ω),
    Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t1 →
      Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)) ↔
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
Tactic: rw [Indep_iff_IndepSets, IndepSets_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
x : MeasurableSpace Ω
β : Type u_7
γ : Type u_8
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
μ : Measure Ω
⊢ f ⟂ᵢ[μ] g ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
have rw : Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) μ ↔
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
Tactic: rw [IndepFun_iff_Indep, Indep_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
x : MeasurableSpace Ω
β : Type u_7
γ : Type u_8
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
μ : Measure Ω
rw :
  Indep (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
⊢ f ⟂ᵢ[μ] g ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
have rw₁ : (∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)) ↔
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
Tactic: rw [IndepFun_iff_Indep, Indep_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
𝒜 ℬ : Set (Set Ω)
h : ∀ A ∈ 𝒜, IndepSets {A} ℬ μ
⊢ IndepSets 𝒜 ℬ μ
have rw : IndepSets (⋃ x ∈ 𝒜, {x}) ℬ μ
Tactic: rw [← 𝒜.biUnion_of_singleton]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set Ω
⊢ 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∞)
have 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∞)
Tactic: simp_rw [iIndepSets, Kernel.iIndepSets_singleton_iff, ae_dirac_eq, Filter.eventually_pure,
    Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: simp_rw [iIndepSets, Kernel.iIndepSets_singleton_iff, ae_dirac_eq, Filter.eventually_pure,
    Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: simp_rw [iIndepSets, Kernel.iIndepSets_singleton_iff, ae_dirac_eq, Filter.eventually_pure,
    Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: simp_rw [iIndepSets, Kernel.iIndepSets_singleton_iff, ae_dirac_eq, Filter.eventually_pure,
    Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : ι → Set Ω
hf : ∀ (i : ι), MeasurableSet (f i)
⊢ iIndepSet f μ ↔
    ∀ (s : Finset ι),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have 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∞)
Tactic: simp_rw [iIndepSet, Kernel.iIndepSet_iff_meas_biInter hf, ae_dirac_eq, Filter.eventually_pure,
    Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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∞)
⊢ iIndepSet f μ ↔
    ∀ (s : Finset ι),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have 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∞)
Tactic: simp_rw [iIndepSet, Kernel.iIndepSet_iff_meas_biInter hf, ae_dirac_eq, Filter.eventually_pure,
    Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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∞)
⊢ iIndepSet f μ ↔
    ∀ (s : Finset ι),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have 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∞)
Tactic: simp_rw [iIndepSet, Kernel.iIndepSet_iff_meas_biInter hf, ae_dirac_eq, Filter.eventually_pure,
    Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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∞)
⊢ iIndepSet f μ ↔
    ∀ (s : Finset ι),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have 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∞)
Tactic: simp_rw [iIndepSet, Kernel.iIndepSet_iff_meas_biInter hf, ae_dirac_eq, Filter.eventually_pure,
    Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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 μ)
⊢ f ⟂ᵢ[μ] g ↔
    Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ))
have 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 μ))
Tactic: rw [indepFun_iff_measure_inter_preimage_eq_mul]