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 Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ β (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → β i) f) μ
⊢ iIndepFun (β := β) f μ
have rw : ∀ (s : Finset ι) {f' : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (f' i)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f' i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f' i) : ℝ≥0∞)
Tactic: rw [iIndepFun_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f_1 : (i : ι) → Ω → β i
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ β (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → β i) f_1) μ
s : Finset ι
f : ι → Set Ω
hs : ∀ i ∈ s, MeasurableSet (f i)
⊢ Eq.{u_1 + 1} (α := Set Ω) (⋂ i ∈ s, f i) (⋂ (i : ↥s), f (↑i : ι))
have h₁ : ∀ (x : Ω), Membership.mem (γ := Set Ω) (⋂ i ∈ s, f i) x ↔ Membership.mem (γ := Set Ω) (⋂ (i : ↥s), f (↑i : ι)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f_1 : (i : ι) → Ω → β i
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ β (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → β i) f_1) μ
s : Finset ι
f : ι → Set Ω
hs : ∀ i ∈ s, MeasurableSet (f i)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have this : Eq.{u_1 + 1} (α := Set Ω) (⋂ i ∈ s, f i) (⋂ (i : ↥s), f (↑i : ι))
Tactic: have : ⋂ i ∈ s, f i = ⋂ i : s, f i := by ext; simp
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f_1 : (i : ι) → Ω → β i
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ β (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → β i) f_1) μ
s : Finset ι
f : ι → Set Ω
hs : ∀ i ∈ s, MeasurableSet (f i)
this : Eq.{u_1 + 1} (α := Set Ω) (⋂ i ∈ s, f i) (⋂ (i : ↥s), f (↑i : ι))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∏ i ∈ s, (μ : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ↥s), f (↑i : ι)) : ℝ≥0∞)
  (∏ i : ↥s, (μ : (a : Set Ω) → ℝ≥0∞) (f (↑i : ι)) : ℝ≥0∞)
Tactic: rw [← Finset.prod_coe_sort, this]
-- 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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h : iIndepFun (β := β) f μ
⊢ Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
have this : IsProbabilityMeasure μ
Tactic: have := h.isProbabilityMeasure
-- 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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h : iIndepFun (β := β) f μ
this : IsProbabilityMeasure μ
⊢ Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
have h₁ : ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
    (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
Tactic: rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h
Cleared hypotheses: h, this
-- 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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
this : IsProbabilityMeasure μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ 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∞)
have left : Eq (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i))
  (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (s i))
Tactic: constructor
-- 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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
this : IsProbabilityMeasure μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
left :
  Eq (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i))
    (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (s i))
⊢ 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∞)
have right : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' s i) : ℝ≥0∞)
  ((Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ : (a : Set ((i : ι) → β i)) → ℝ≥0∞) (Set.pi (α := β) univ s) : ℝ≥0∞)
Tactic: constructor
-- 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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
this : IsProbabilityMeasure μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ 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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
this : IsProbabilityMeasure μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
x : ι
⊢ 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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
this : IsProbabilityMeasure μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ 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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
this : IsProbabilityMeasure μ
s : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ 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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
this : IsProbabilityMeasure μ
⊢ Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
this : IsProbabilityMeasure μ
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) μ)
have refine : ∀ (h' : (i : ι) → Set (β i)) (hm : ∀ (i : ι), MeasurableSet (h' i)),
  Eq (α := ℝ≥0∞)
    ((Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ : (a : Set ((i : ι) → β i)) → ℝ≥0∞) (Set.pi (α := β) univ h') : ℝ≥0∞)
    (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (h' i) : ℝ≥0∞)
Tactic: refine (Measure.pi_eq fun h' hm ↦ ?_).symm
-- 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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
      (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞)
this : IsProbabilityMeasure μ
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' : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (h' i)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ : (a : Set ((i : ι) → β i)) → ℝ≥0∞) (Set.pi (α := β) univ h') : ℝ≥0∞)
    (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (h' i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' h' i) : ℝ≥0∞)
  (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' h' i) : ℝ≥0∞)
Tactic: rw [← (h₀ hm).1, ← (h₀ hm).2]
-- 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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h : iIndepFun (β := β) f μ
⊢ Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
have have : ∀ (this : IsProbabilityMeasure μ),
  Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
Tactic: classical
  have := h.isProbabilityMeasure
  rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h
  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
  refine (Measure.pi_eq fun h' hm ↦ ?_).symm
  rw [← (h₀ hm).1, ← (h₀ hm).2]
  simpa [hm] using h Finset.univ (sets := 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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h : iIndepFun (β := β) f μ
have have₁ have₂ :
  ∀ (this : IsProbabilityMeasure μ),
    Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
⊢ Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
have have₃ : ∀
  (h :
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
        (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞))
  (this : IsProbabilityMeasure μ),
  Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
Tactic: classical
  have := h.isProbabilityMeasure
  rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h
  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
  refine (Measure.pi_eq fun h' hm ↦ ?_).symm
  rw [← (h₀ hm).1, ← (h₀ hm).2]
  simpa [hm] using h Finset.univ (sets := 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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h : iIndepFun (β := β) f μ
have have₁ have₂ :
  ∀ (this : IsProbabilityMeasure μ),
    Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
have₃ :
  ∀
    (h :
      ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
        Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
          (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞))
    (this : IsProbabilityMeasure μ),
    Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
⊢ Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
have have₄ : ∀
  (h :
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ S, f i ⁻¹' sets i) : ℝ≥0∞)
        (∏ i ∈ S, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' sets i) : ℝ≥0∞))
  (this : IsProbabilityMeasure μ)
  (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) μ)
Tactic: classical
  have := h.isProbabilityMeasure
  rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h
  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
  refine (Measure.pi_eq fun h' hm ↦ ?_).symm
  rw [← (h₀ hm).1, ← (h₀ hm).2]
  simpa [hm] using h Finset.univ (sets := 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) μ
⊢ iIndepFun (β := β) f μ ↔
    Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
      (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ)
have refine : Eq (α := Measure ((i : ι) → β i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ)
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) μ) →
  iIndepFun (β := β) f μ
Tactic: refine ⟨iIndepFun.map_fun_eq_pi_map hf, ?_⟩
-- 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: rw [iIndepFun_iff_measure_inter_preimage_eq_mul]
-- 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)) ∧
    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 left : Eq (α := ℝ≥0∞) (∏ i : ι, (μ : (a : Set Ω) → ℝ≥0∞) (f i ⁻¹' s i))
  (∏ i : ι, ((Measure.map (f i) μ : Measure (β i)) : (a : Set (β i)) → ℝ≥0∞) (s i))
Tactic: constructor
-- 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)
left :
  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∞) (∏ 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∞)
have right : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (⋂ (i : ι), f i ⁻¹' s i) : ℝ≥0∞)
  ((Measure.map (fun (ω : Ω) (i : ι) ↦ f i ω) μ : (a : Set ((i : ι) → β i)) → ℝ≥0∞) (Set.pi (α := β) univ s) : ℝ≥0∞)
Tactic: constructor