awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (∏ x ∈ Finset.erase Finset.univ i,
      (μ x : (a : Set (α x)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s x))
    (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ)
have h : ∀ (j : ι) (hj : j ∈ Finset.erase Finset.univ i),
  Eq (α := ℝ≥0∞)
    ((μ j : (a : Set (α j)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s j) : ℝ≥0∞)
    ((μ j : (a : Set (α j)) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: refine Finset.prod_congr rfl fun j hj ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((map (eval (β := α) i) (Measure.pi (α := α) μ) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  ((Measure.pi (α := α) μ : (a : Set ((a : ι) → α a)) → ℝ≥0∞) ((fun (f : (a : ι) → α a) ↦ f i) ⁻¹' s) : ℝ≥0∞)
  ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
        (a : Set (α i)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: classical
  rw [Measure.map_apply (measurable_pi_apply i) hs, ← Set.univ_pi_update_univ, Measure.pi_pi,
    Measure.smul_apply, smul_eq_mul, ← Finset.prod_erase_mul _ _ (a := i) (by simp)]
  congrm ?_ * ?_
  swap; · simp
  refine Finset.prod_congr rfl fun j hj ↦ ?_
  simp [Function.update, Finset.ne_of_mem_erase hj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((a : ι) → α a)) → ℝ≥0∞) ((fun (f : (a : ι) → α a) ↦ f i) ⁻¹' s) : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (eval (β := α) i) (Measure.pi (α := α) μ) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞)
  ((Measure.pi (α := α) μ : (a : Set ((a : ι) → α a)) → ℝ≥0∞)
      (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s)) :
    ℝ≥0∞)
  ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
        (a : Set (α i)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: classical
  rw [Measure.map_apply (measurable_pi_apply i) hs, ← Set.univ_pi_update_univ, Measure.pi_pi,
    Measure.smul_apply, smul_eq_mul, ← Finset.prod_erase_mul _ _ (a := i) (by simp)]
  congrm ?_ * ?_
  swap; · simp
  refine Finset.prod_congr rfl fun j hj ↦ ?_
  simp [Function.update, Finset.ne_of_mem_erase hj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((a : ι) → α a)) → ℝ≥0∞) ((fun (f : (a : ι) → α a) ↦ f i) ⁻¹' s) : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((a : ι) → α a)) → ℝ≥0∞)
        (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s)) :
      ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (eval (β := α) i) (Measure.pi (α := α) μ) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞)
  (∏ i_1 : ι, (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i_1) :
    ℝ≥0∞)
  ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
        (a : Set (α i)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: classical
  rw [Measure.map_apply (measurable_pi_apply i) hs, ← Set.univ_pi_update_univ, Measure.pi_pi,
    Measure.smul_apply, smul_eq_mul, ← Finset.prod_erase_mul _ _ (a := i) (by simp)]
  congrm ?_ * ?_
  swap; · simp
  refine Finset.prod_congr rfl fun j hj ↦ ?_
  simp [Function.update, Finset.ne_of_mem_erase hj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((a : ι) → α a)) → ℝ≥0∞) ((fun (f : (a : ι) → α a) ↦ f i) ⁻¹' s) : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((a : ι) → α a)) → ℝ≥0∞)
        (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s)) :
      ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞)
    (∏ i_1 : ι,
        (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i_1) :
      ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (eval (β := α) i) (Measure.pi (α := α) μ) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₃ : ∏ i_1 : ι, (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i_1) =
  HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ)
    ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: classical
  rw [Measure.map_apply (measurable_pi_apply i) hs, ← Set.univ_pi_update_univ, Measure.pi_pi,
    Measure.smul_apply, smul_eq_mul, ← Finset.prod_erase_mul _ _ (a := i) (by simp)]
  congrm ?_ * ?_
  swap; · simp
  refine Finset.prod_congr rfl fun j hj ↦ ?_
  simp [Function.update, Finset.ne_of_mem_erase hj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((a : ι) → α a)) → ℝ≥0∞) ((fun (f : (a : ι) → α a) ↦ f i) ⁻¹' s) : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((a : ι) → α a)) → ℝ≥0∞)
        (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s)) :
      ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞)
    (∏ i_1 : ι,
        (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i_1) :
      ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₃ :
  ∏ i_1 : ι, (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i_1) =
    HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ)
      ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (eval (β := α) i) (Measure.pi (α := α) μ) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₄ : ∏ i_1 : ι, (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i_1) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: classical
  rw [Measure.map_apply (measurable_pi_apply i) hs, ← Set.univ_pi_update_univ, Measure.pi_pi,
    Measure.smul_apply, smul_eq_mul, ← Finset.prod_erase_mul _ _ (a := i) (by simp)]
  congrm ?_ * ?_
  swap; · simp
  refine Finset.prod_congr rfl fun j hj ↦ ?_
  simp [Function.update, Finset.ne_of_mem_erase hj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((a : ι) → α a)) → ℝ≥0∞) ((fun (f : (a : ι) → α a) ↦ f i) ⁻¹' s) : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((a : ι) → α a)) → ℝ≥0∞)
        (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s)) :
      ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞)
    (∏ i_1 : ι,
        (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i_1) :
      ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₃ :
  ∏ i_1 : ι, (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i_1) =
    HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ)
      ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
h₄ :
  ∏ i_1 : ι, (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i_1) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ : ℝ≥0∞)
      ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map (eval (β := α) i) (Measure.pi (α := α) μ) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₅ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
    (∏ x ∈ Finset.erase Finset.univ i,
        (μ x : (a : Set (α x)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s x) :
      ℝ≥0∞)
    ((μ i : (a : Set (α i)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: classical
  rw [Measure.map_apply (measurable_pi_apply i) hs, ← Set.univ_pi_update_univ, Measure.pi_pi,
    Measure.smul_apply, smul_eq_mul, ← Finset.prod_erase_mul _ _ (a := i) (by simp)]
  congrm ?_ * ?_
  swap; · simp
  refine Finset.prod_congr rfl fun j hj ↦ ?_
  simp [Function.update, Finset.ne_of_mem_erase hj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
⊢ Eq (α := Measure ((i : ι) → Y i)) (map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (Measure.pi (α := X) μ))
    (Measure.pi (α := Y) fun (i : ι) ↦ map (f i) (μ i))
have this : ∀ (i : ι), SigmaFinite (μ i)
Tactic: have (i : ι) := (hμ i).of_map _ (hf i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
⊢ Eq (α := Measure ((i : ι) → Y i)) (map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (Measure.pi (α := X) μ))
    (Measure.pi (α := Y) fun (i : ι) ↦ map (f i) (μ i))
have refine : ∀ (s : (i : ι) → Set (Y i)) (hs : ∀ (i : ι), MeasurableSet (s i)),
  Eq (α := ℝ≥0∞)
    ((map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (Measure.pi (α := X) μ) : (a : Set ((i : ι) → Y i)) → ℝ≥0∞)
        (Set.pi (α := Y) univ s) :
      ℝ≥0∞)
    (∏ i : ι, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: refine (pi_eq fun s hs ↦ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞)
    ((map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (Measure.pi (α := X) μ) : (a : Set ((i : ι) → Y i)) → ℝ≥0∞)
        (Set.pi (α := Y) univ s) :
      ℝ≥0∞)
    (∏ i : ι, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
      ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s) :
    ℝ≥0∞)
  (∏ i : ι, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: rw [map_apply_of_aemeasurable _ (.univ_pi hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
rw :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s) :
      ℝ≥0∞)
    (∏ i : ι, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (Measure.pi (α := X) μ) : (a : Set ((i : ι) → Y i)) → ℝ≥0∞)
        (Set.pi (α := Y) univ s) :
      ℝ≥0∞)
    (∏ i : ι, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw₁ : AEMeasurable (β := (i : ι) → Y i) (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (Measure.pi (α := X) μ)
Tactic: rw [map_apply_of_aemeasurable _ (.univ_pi hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s)
    (Set.pi (α := X) univ fun (i : ι) ↦ f i ⁻¹' s i)
have h : ∀ (x : (i : ι) → X i),
  Membership.mem (γ := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s)
      x ↔
    Membership.mem (γ := Set ((i : ι) → X i)) (Set.pi (α := X) univ fun (i : ι) ↦ f i ⁻¹' s i) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s) :
      ℝ≥0∞)
    (∏ i : ι, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have this₁ : Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s)
  (Set.pi (α := X) univ fun (i : ι) ↦ f i ⁻¹' s i)
Tactic: have : (fun (x : Π i, X i) i ↦ f i (x i)) ⁻¹' (Set.univ.pi s) =
      Set.univ.pi (fun i ↦ (f i) ⁻¹' (s i)) := by ext x; simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this_1 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
this :
  Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s)
    (Set.pi (α := X) univ fun (i : ι) ↦ f i ⁻¹' s i)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.pi (α := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s) :
      ℝ≥0∞)
    (∏ i : ι, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' s i))
  (∏ i : ι, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i))
Tactic: rw [this, pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this_1 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
this :
  Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s)
    (Set.pi (α := X) univ fun (i : ι) ↦ f i ⁻¹' s i)
⊢ Eq (α := ℝ≥0∞) (∏ i : ι, (μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' s i))
    (∏ i : ι, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i))
have e_f : ∀ (i : ι),
  Eq (α := ℝ≥0∞) ((μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)
    (((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: congr with i
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
inst : Fintype ι
X : ι → Type u_4
Y : ι → Type u_5
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
inst_1 : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hμ : ∀ (i : ι), SigmaFinite (m0 := inst_1 i) (map (f i) (μ i))
hf : ∀ (i : ι), AEMeasurable (f i) (μ i)
this_1 : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (Y i)
hs : ∀ (i : ι), MeasurableSet (s i)
this :
  Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' Set.pi (α := Y) univ s)
    (Set.pi (α := X) univ fun (i : ι) ↦ f i ⁻¹' s i)
i : ι
⊢ Eq (α := ℝ≥0∞) ((μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)
    (((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have e_f : Eq (α := ℝ≥0∞) ((μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)
  ((μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' s i) : ℝ≥0∞)
Tactic: rw [map_apply_of_aemeasurable (hf i) (hs i)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
⊢ MeasurePreserving (eval (β := α) i) (Measure.pi (α := α) μ) (μ i)
have refine : map (eval (β := α) i) (Measure.pi (α := α) μ) = μ i
Tactic: refine ⟨measurable_pi_apply i, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
⊢ map (eval (β := α) i) (Measure.pi (α := α) μ) = μ i
have rw : ∀ x ∈ Finset.erase Finset.univ i, Eq (α := ℝ≥0∞) ((μ x : (a : Set (α x)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [Measure.pi_map_eval, Finset.prod_eq_one, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
⊢ map (eval (β := α) i) (Measure.pi (α := α) μ) = μ i
have rw : HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) = μ i
Tactic: classical
  rw [Measure.pi_map_eval, Finset.prod_eq_one, one_smul]
  exact fun _ _ ↦ measure_univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
rw : HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) = μ i
⊢ map (eval (β := α) i) (Measure.pi (α := α) μ) = μ i
have rw₁ : HSMul.hSMul (α := ℝ≥0∞) 1 (μ i) = μ i
Tactic: classical
  rw [Measure.pi_map_eval, Finset.prod_eq_one, one_smul]
  exact fun _ _ ↦ measure_univ