awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i))
    (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (s i))
have 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∞)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
x : ι
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x) : ℝ≥0∞)
    (((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) (s x) : ℝ≥0∞)
have left : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x) : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x) : ℝ≥0∞)
Tactic: rw [Measure.map_apply_of_aemeasurable (hf x) (hm x)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (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∞)
have 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∞)
Tactic: rw [Measure.map_apply_of_aemeasurable (aemeasurable_pi_lambda _ fun x ↦ hf x)
        (.univ_pi hm)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ 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∞)
have 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
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
⊢ Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ) →
    ∀ (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∞)
have h₀ : ∀ {s : (i : ι) → Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)),
  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: have h₀ {s : ∀ i, Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)) :
      ∏ i : ι, μ (f i ⁻¹' s i) = ∏ i : ι, μ.map (f i) (s i) ∧
      μ (⋂ i : ι, (f i ⁻¹' s i)) = μ.map (fun ω i ↦ f i ω) (univ.pi s) := by
    constructor
    · congr with x
      rw [Measure.map_apply_of_aemeasurable (hf x) (hm x)]
    · rw [Measure.map_apply_of_aemeasurable (aemeasurable_pi_lambda _ fun x ↦ hf x)
        (.univ_pi hm)]
      congr with x
      simp
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
h₀ :
  ∀ {s : (i : ι) → Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)),
    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∞)
h :
  Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
S : Finset ι
s : (i : ι) → Set (β i)
hs : ∀ i ∈ S, MeasurableSet (s i)
i : ι
⊢ MeasurableSet (if i ∈ S then s i else univ)
have pos : ∀ (hiS : i ∈ S), MeasurableSet (s i)
Tactic: split_ifs with hiS
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
h₀ :
  ∀ {s : (i : ι) → Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)),
    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∞)
h :
  Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
S : Finset ι
s : (i : ι) → Set (β i)
hs : ∀ i ∈ S, MeasurableSet (s i)
i : ι
pos : ∀ (hiS : i ∈ S), MeasurableSet (s i)
⊢ MeasurableSet (if i ∈ S then s i else univ)
have neg : ∀ (hiS : i ∉ S), MeasurableSet.{u_11} (α := β i) univ
Tactic: split_ifs with hiS
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
h₀ :
  ∀ {s : (i : ι) → Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)),
    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∞)
h :
  Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
S : Finset ι
s : (i : ι) → Set (β i)
hs : ∀ i ∈ S, MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' s i) : ℝ≥0∞)
    (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' if i ∈ S then s i else univ))
    (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (if i ∈ S then s i else univ)) ∧
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' if i ∈ S then s i else univ) : ℝ≥0∞)
    ((Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ : (a : Set ((i : ι) → β i)) → ℝ≥0∞)
        (Set.pi (α := β) univ fun (i : ι) ↦ if i ∈ S then s i else univ) :
      ℝ≥0∞)
Tactic: specialize h₀ (s := fun i ↦ if i ∈ S then s i else univ)
    fun i ↦ by beta_reduce; split_ifs with hiS <;> simp [hiS, hs]
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
S : Finset ι
s : (i : ι) → Set (β i)
hs : ∀ i ∈ S, MeasurableSet (s i)
h₀ :
  Eq (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' if i ∈ S then s i else univ))
      (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (if i ∈ S then s i else univ)) ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' if i ∈ S then s i else univ) : ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ : (a : Set ((i : ι) → β i)) → ℝ≥0∞)
          (Set.pi (α := β) univ fun (i : ι) ↦ if i ∈ S then s i else univ) :
        ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' s i) : ℝ≥0∞)
    (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)
have h₁ : ∏ x ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x) =
    HMul.hMul (α := ℝ≥0∞) (∏ x ∈ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) (s x))
      (∏ x : ι with x ∉ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) univ) ∧
  (μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' s i) =
    HMul.hMul (α := ℝ≥0∞) (∏ x ∈ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) (s x))
      (∏ x : ι with x ∉ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) univ)
Tactic: simp only [apply_ite, preimage_univ, measure_univ, Finset.prod_ite_mem, Finset.univ_inter,
    Finset.prod_ite, Finset.filter_univ_mem, iInter_ite, iInter_univ, inter_univ, h,
    Measure.pi_pi] at h₀
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
S : Finset ι
s : (i : ι) → Set (β i)
hs : ∀ i ∈ S, MeasurableSet (s i)
h₀ :
  ∏ x ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x) =
      HMul.hMul (α := ℝ≥0∞) (∏ x ∈ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) (s x))
        (∏ x : ι with x ∉ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) univ) ∧
    (μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' s i) =
      HMul.hMul (α := ℝ≥0∞) (∏ x ∈ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) (s x))
        (∏ x : ι with x ∉ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) univ)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' s i) : ℝ≥0∞)
    (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)
have rw : HMul.hMul (α := ℝ≥0∞) (∏ x ∈ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) (s x))
    (∏ x : ι with x ∉ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) univ) =
  ∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i)
Tactic: rw [h₀.2, ← h₀.1]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
S : Finset ι
s : (i : ι) → Set (β i)
hs : ∀ i ∈ S, MeasurableSet (s i)
h₀ :
  ∏ x ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x) =
      HMul.hMul (α := ℝ≥0∞) (∏ x ∈ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) (s x))
        (∏ x : ι with x ∉ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) univ) ∧
    (μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' s i) =
      HMul.hMul (α := ℝ≥0∞) (∏ x ∈ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) (s x))
        (∏ x : ι with x ∉ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) univ)
rw :
  HMul.hMul (α := ℝ≥0∞) (∏ x ∈ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) (s x))
      (∏ x : ι with x ∉ S, ((Measure.map (f x) μ : Measure (β x)) : (a : Set (β x)) → ℝ≥0∞) univ) =
    ∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' s i) : ℝ≥0∞)
    (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (∏ x ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f x ⁻¹' s x)) (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i))
Tactic: rw [h₀.2, ← h₀.1]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
⊢ Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ) →
    iIndepFun (β := β) f μ
have rw : Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ) →
  ∀ (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: classical
  rw [iIndepFun_iff_measure_inter_preimage_eq_mul]
  have h₀ {s : ∀ i, Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)) :
      ∏ i : ι, μ (f i ⁻¹' s i) = ∏ i : ι, μ.map (f i) (s i) ∧
      μ (⋂ i : ι, (f i ⁻¹' s i)) = μ.map (fun ω i ↦ f i ω) (univ.pi s) := by
    constructor
    · congr with x
      rw [Measure.map_apply_of_aemeasurable (hf x) (hm x)]
    · rw [Measure.map_apply_of_aemeasurable (aemeasurable_pi_lambda _ fun x ↦ hf x)
        (.univ_pi hm)]
      congr with x
      simp
  intro h S s hs
  specialize h₀ (s := fun i ↦ if i ∈ S then s i else univ)
    fun i ↦ by beta_reduce; split_ifs with hiS <;> simp [hiS, hs]
  simp only [apply_ite, preimage_univ, measure_univ, Finset.prod_ite_mem, Finset.univ_inter,
    Finset.prod_ite, Finset.filter_univ_mem, iInter_ite, iInter_univ, inter_univ, h,
    Measure.pi_pi] at h₀
  rw [h₀.2, ← h₀.1]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst_1 : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
rw rw₁ rw₂ :
  Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ) →
    ∀ (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∞)
⊢ Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ) →
    iIndepFun (β := β) f μ
have rw₃ : ∀
  (h₀ :
    ∀ {s : (i : ι) → Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)),
      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∞)),
  Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ) →
    ∀ (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: classical
  rw [iIndepFun_iff_measure_inter_preimage_eq_mul]
  have h₀ {s : ∀ i, Set (β i)} (hm : ∀ (i : ι), MeasurableSet (s i)) :
      ∏ i : ι, μ (f i ⁻¹' s i) = ∏ i : ι, μ.map (f i) (s i) ∧
      μ (⋂ i : ι, (f i ⁻¹' s i)) = μ.map (fun ω i ↦ f i ω) (univ.pi s) := by
    constructor
    · congr with x
      rw [Measure.map_apply_of_aemeasurable (hf x) (hm x)]
    · rw [Measure.map_apply_of_aemeasurable (aemeasurable_pi_lambda _ fun x ↦ hf x)
        (.univ_pi hm)]
      congr with x
      simp
  intro h S s hs
  specialize h₀ (s := fun i ↦ if i ∈ S then s i else univ)
    fun i ↦ by beta_reduce; split_ifs with hiS <;> simp [hiS, hs]
  simp only [apply_ite, preimage_univ, measure_univ, Finset.prod_ite_mem, Finset.univ_inter,
    Finset.prod_ite, Finset.filter_univ_mem, iInter_ite, iInter_univ, inter_univ, h,
    Measure.pi_pi] at h₀
  rw [h₀.2, ← h₀.1]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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 (α := Ω) μ)
have refine_1 : ∀ (i : ι), AEMeasurable (β := 𝓧 i) (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ)
Tactic: refine iIndepFun_iff_map_fun_eq_pi_map ?_ |>.2 ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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 (α := Ω) μ)
⊢ iIndepFun (β := 𝓧) (fun (i : ι) (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ)
have 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 (α := Ω) μ))
Tactic: refine iIndepFun_iff_map_fun_eq_pi_map ?_ |>.2 ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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)
⊢ 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 (α := Ω) μ))
have 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 (α := Ω) μ))
Tactic: rw [Measure.pi_map_pi mX]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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)
⊢ 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 (α := Ω) μ))
have 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 (α := Ω) μ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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)
⊢ Eq (α := (i : ι) → Measure (𝓧 i)) (fun (i : ι) ↦ Measure.map (X i) (μ i)) fun (i : ι) ↦
    Measure.map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ)
have refine_2 : ∀ (i : ι),
  Eq (α := Measure (𝓧 i)) (Measure.map (X i) (μ i))
    (Measure.map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ))
Tactic: ext i : 1
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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 : ι
⊢ Eq (α := Measure (𝓧 i)) (Measure.map (X i) (μ i))
    (Measure.map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ))
have refine_2 : AEMeasurable (_m := mΩ i) (X i) (Measure.map (Function.eval (β := Ω) i) (Measure.pi (α := Ω) μ))
Tactic: rw [← (measurePreserving_eval μ i).map_eq, AEMeasurable.map_map_of_aemeasurable,
    Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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 (α := Ω) μ))
⊢ Eq (α := Measure (𝓧 i)) (Measure.map (X i) (μ i))
    (Measure.map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (Measure.pi (α := Ω) μ))
have refine_2₁ : AEMeasurable (Function.eval (β := Ω) i) (Measure.pi (α := Ω) μ)
Tactic: rw [← (measurePreserving_eval μ i).map_eq, AEMeasurable.map_map_of_aemeasurable,
    Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
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 (_m := mΩ i) (X i) (Measure.map (Function.eval (β := Ω) i) (Measure.pi (α := Ω) μ))
have refine_2 : AEMeasurable (X i) (μ i)
Tactic: rw [(measurePreserving_eval μ i).map_eq]