awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) ∂Measure.pi (α := E) μ)
      (∏ i : Fin n, ∫ (x : E i), f i x ∂μ i)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
rw :
  (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
      fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i)) =
    HMul.hMul (α := 𝕜) (∫ (x : E 0), f 0 x ∂μ 0)
      (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : Fin n) ↦ E i.succ))
        (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ) fun (x : (i : Fin n) → E i.succ) ↦
        ∏ i : Fin n, f i.succ (x i))
⊢ (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
      fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i)) =
    HMul.hMul (α := 𝕜) (∫ (x : E 0), f 0 x ∂μ 0) (∏ i : Fin n, ∫ (x : E i.succ), f i.succ x ∂μ i.succ)
have rw₁ : Eq.{u_1 + 1} (α := 𝕜)
  (@integral _ _ _ _ Prod.instMeasurableSpace
    (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
    fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i))
  (@integral _ _ _ _ Prod.instMeasurableSpace
    (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
    fun (z : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 z.1 * ∏ i : Fin n, f i.succ (z.2 i))
Tactic: rw [← n_ih, ← integral_prod_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) ∂Measure.pi (α := E) μ)
      (∏ i : Fin n, ∫ (x : E i), f i x ∂μ i)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
⊢ HMul.hMul (α := 𝕜) (∫ (x : E 0), f 0 x ∂μ 0) (∏ i : Fin n, ∫ (x : E i.succ), f i.succ x ∂μ i.succ) =
    ∏ i : Fin (n + 1), ∫ (x : E i), f i x ∂μ i
have rw : HMul.hMul (α := 𝕜) (∫ (x : E 0), f 0 x ∂μ 0) (∏ i : Fin n, ∫ (x : E i.succ), f i.succ x ∂μ i.succ) =
  HMul.hMul (α := 𝕜) (∫ (x : E 0), f 0 x ∂μ 0) (∏ i : Fin n, ∫ (x : E i.succ), f i.succ x ∂μ i.succ)
Tactic: rw [Fin.prod_univ_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) ∂Measure.pi (α := E) μ)
      (∏ i : Fin n, ∫ (x : E i), f i x ∂μ i)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin (n + 1)) → E i), ∏ i : Fin (n + 1), f i (x i) ∂Measure.pi (α := E) μ)
    (∏ i : Fin (n + 1), ∫ (x : E i), f i x ∂μ i)
have _ : Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin (n + 1)) → E i), ∏ i : Fin (n + 1), f i (x i) ∂Measure.pi (α := E) μ)
  (@integral _ _ _ _ Prod.instMeasurableSpace
    (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
    fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i))
Tactic: calc
        _ = ∫ x : E 0 × ((i : Fin n) → E (Fin.succ i)),
            f 0 x.1 * ∏ i : Fin n, f (Fin.succ i) (x.2 i)
            ∂((μ 0).prod (Measure.pi (fun i ↦ μ i.succ))) := by
          rw [← ((measurePreserving_piFinSuccAbove μ 0).symm).integral_comp']
          simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
            Fin.prod_univ_succ, Fin.insertNth_zero, Equiv.coe_fn_mk, Fin.cons_succ,
            Fin.zero_succAbove, cast_eq, Fin.cons_zero]
        _ = (∫ x, f 0 x ∂μ 0)
            * ∏ i : Fin n, ∫ (x : E (Fin.succ i)), f (Fin.succ i) x ∂(μ i.succ) := by
          rw [← n_ih, ← integral_prod_mul]
        _ = ∏ i, ∫ x, f i x ∂(μ i) := by rw [Fin.prod_univ_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) ∂Measure.pi (α := E) μ)
      (∏ i : Fin n, ∫ (x : E i), f i x ∂μ i)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
_ :
  Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin (n + 1)) → E i), ∏ i : Fin (n + 1), f i (x i) ∂Measure.pi (α := E) μ)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
      fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i))
⊢ Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin (n + 1)) → E i), ∏ i : Fin (n + 1), f i (x i) ∂Measure.pi (α := E) μ)
    (∏ i : Fin (n + 1), ∫ (x : E i), f i x ∂μ i)
have _₁ : (@integral _ _ _ _ Prod.instMeasurableSpace
    (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
    fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i)) =
  HMul.hMul (α := 𝕜) (∫ (x : E 0), f 0 x ∂μ 0) (∏ i : Fin n, ∫ (x : E i.succ), f i.succ x ∂μ i.succ)
Tactic: calc
        _ = ∫ x : E 0 × ((i : Fin n) → E (Fin.succ i)),
            f 0 x.1 * ∏ i : Fin n, f (Fin.succ i) (x.2 i)
            ∂((μ 0).prod (Measure.pi (fun i ↦ μ i.succ))) := by
          rw [← ((measurePreserving_piFinSuccAbove μ 0).symm).integral_comp']
          simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
            Fin.prod_univ_succ, Fin.insertNth_zero, Equiv.coe_fn_mk, Fin.cons_succ,
            Fin.zero_succAbove, cast_eq, Fin.cons_zero]
        _ = (∫ x, f 0 x ∂μ 0)
            * ∏ i : Fin n, ∫ (x : E (Fin.succ i)), f (Fin.succ i) x ∂(μ i.succ) := by
          rw [← n_ih, ← integral_prod_mul]
        _ = ∏ i, ∫ x, f i x ∂(μ i) := by rw [Fin.prod_univ_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) ∂Measure.pi (α := E) μ)
      (∏ i : Fin n, ∫ (x : E i), f i x ∂μ i)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst_1 : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
_ :
  Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin (n + 1)) → E i), ∏ i : Fin (n + 1), f i (x i) ∂Measure.pi (α := E) μ)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
      fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i))
_₁ :
  (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (i : Fin n) ↦ μ i.succ))
      fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i)) =
    HMul.hMul (α := 𝕜) (∫ (x : E 0), f 0 x ∂μ 0) (∏ i : Fin n, ∫ (x : E i.succ), f i.succ x ∂μ i.succ)
⊢ Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin (n + 1)) → E i), ∏ i : Fin (n + 1), f i (x i) ∂Measure.pi (α := E) μ)
    (∏ i : Fin (n + 1), ∫ (x : E i), f i x ∂μ i)
have _₂ : HMul.hMul (α := 𝕜) (∫ (x : E 0), f 0 x ∂μ 0) (∏ i : Fin n, ∫ (x : E i.succ), f i.succ x ∂μ i.succ) =
  ∏ i : Fin (n + 1), ∫ (x : E i), f i x ∂μ i
Tactic: calc
        _ = ∫ x : E 0 × ((i : Fin n) → E (Fin.succ i)),
            f 0 x.1 * ∏ i : Fin n, f (Fin.succ i) (x.2 i)
            ∂((μ 0).prod (Measure.pi (fun i ↦ μ i.succ))) := by
          rw [← ((measurePreserving_piFinSuccAbove μ 0).symm).integral_comp']
          simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
            Fin.prod_univ_succ, Fin.insertNth_zero, Equiv.coe_fn_mk, Fin.cons_succ,
            Fin.zero_succAbove, cast_eq, Fin.cons_zero]
        _ = (∫ x, f 0 x ∂μ 0)
            * ∏ i : Fin n, ∫ (x : E (Fin.succ i)), f (Fin.succ i) x ∂(μ i.succ) := by
          rw [← n_ih, ← integral_prod_mul]
        _ = ∏ i, ∫ x, f i x ∂(μ i) := by rw [Fin.prod_univ_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : ℕ
E : Fin n → Type u_3
mE : (i : Fin n) → MeasurableSpace (E i)
μ : (i : Fin n) → Measure (E i)
inst_1 : ∀ (i : Fin n), SigmaFinite (μ i)
f : (i : Fin n) → E i → 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) ∂Measure.pi (α := E) μ)
    (∏ i : Fin n, ∫ (x : E i), f i x ∂μ i)
have zero : ∀ {E : Fin 0 → Type u_3} {mE : (i : Fin 0) → MeasurableSpace (E i)} {μ : (i : Fin 0) → Measure (E i)}
  [∀ (i : Fin 0), SigmaFinite (μ i)] (f : (i : Fin 0) → E i → 𝕜),
  Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin 0) → E i), ∏ i : Fin 0, f i (x i) ∂Measure.pi (α := E) μ)
    (∏ i : Fin 0, ∫ (x : E i), f i x ∂μ i)
Tactic: induction n with
  | zero => simp [measureReal_def]
  | succ n n_ih =>
      calc
        _ = ∫ x : E 0 × ((i : Fin n) → E (Fin.succ i)),
            f 0 x.1 * ∏ i : Fin n, f (Fin.succ i) (x.2 i)
            ∂((μ 0).prod (Measure.pi (fun i ↦ μ i.succ))) := by
          rw [← ((measurePreserving_piFinSuccAbove μ 0).symm).integral_comp']
          simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
            Fin.prod_univ_succ, Fin.insertNth_zero, Equiv.coe_fn_mk, Fin.cons_succ,
            Fin.zero_succAbove, cast_eq, Fin.cons_zero]
        _ = (∫ x, f 0 x ∂μ 0)
            * ∏ i : Fin n, ∫ (x : E (Fin.succ i)), f (Fin.succ i) x ∂(μ i.succ) := by
          rw [← n_ih, ← integral_prod_mul]
        _ = ∏ i, ∫ x, f i x ∂(μ i) := by rw [Fin.prod_univ_succ]
Cleared hypotheses: n, E, mE, μ, inst_1, f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : ℕ
E : Fin n → Type u_3
mE : (i : Fin n) → MeasurableSpace (E i)
μ : (i : Fin n) → Measure (E i)
inst_1 : ∀ (i : Fin n), SigmaFinite (μ i)
f : (i : Fin n) → E i → 𝕜
zero :
  ∀ {E : Fin 0 → Type u_3} {mE : (i : Fin 0) → MeasurableSpace (E i)} {μ : (i : Fin 0) → Measure (E i)}
    [∀ (i : Fin 0), SigmaFinite (μ i)] (f : (i : Fin 0) → E i → 𝕜),
    Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin 0) → E i), ∏ i : Fin 0, f i (x i) ∂Measure.pi (α := E) μ)
      (∏ i : Fin 0, ∫ (x : E i), f i x ∂μ i)
⊢ Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) ∂Measure.pi (α := E) μ)
    (∏ i : Fin n, ∫ (x : E i), f i x ∂μ i)
have succ : ∀ (n : ℕ)
  (n_ih :
    ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
      [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
      Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) ∂Measure.pi (α := E) μ)
        (∏ i : Fin n, ∫ (x : E i), f i x ∂μ i))
  {E : Fin (n + 1) → Type u_3} {mE : (i : Fin (n + 1)) → MeasurableSpace (E i)} {μ : (i : Fin (n + 1)) → Measure (E i)}
  [∀ (i : Fin (n + 1)), SigmaFinite (μ i)] (f : (i : Fin (n + 1)) → E i → 𝕜),
  Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : Fin (n + 1)) → E i), ∏ i : Fin (n + 1), f i (x i) ∂Measure.pi (α := E) μ)
    (∏ i : Fin (n + 1), ∫ (x : E i), f i x ∂μ i)
Tactic: induction n with
  | zero => simp [measureReal_def]
  | succ n n_ih =>
      calc
        _ = ∫ x : E 0 × ((i : Fin n) → E (Fin.succ i)),
            f 0 x.1 * ∏ i : Fin n, f (Fin.succ i) (x.2 i)
            ∂((μ 0).prod (Measure.pi (fun i ↦ μ i.succ))) := by
          rw [← ((measurePreserving_piFinSuccAbove μ 0).symm).integral_comp']
          simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
            Fin.prod_univ_succ, Fin.insertNth_zero, Equiv.coe_fn_mk, Fin.cons_succ,
            Fin.zero_succAbove, cast_eq, Fin.cons_zero]
        _ = (∫ x, f 0 x ∂μ 0)
            * ∏ i : Fin n, ∫ (x : E (Fin.succ i)), f (Fin.succ i) x ∂(μ i.succ) := by
          rw [← n_ih, ← integral_prod_mul]
        _ = ∏ i, ∫ x, f i x ∂(μ i) := by rw [Fin.prod_univ_succ]
Cleared hypotheses: n, E, mE, μ, inst_1, f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : RCLike 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
e : Fin (card ι) ≃ ι := Equiv.symm (equivFin ι)
⊢ Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : ι) → E i), ∏ i : ι, f i (x i) ∂Measure.pi (α := E) μ)
    (∏ i : ι, ∫ (x : E i), f i x ∂μ i)
have rw : Eq.{u_1 + 1} (α := 𝕜)
  (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)))
    (Measure.pi (α := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)) fun (i' : Fin (card ι)) ↦
      μ ((e : (a : Fin (card ι)) → ι) i'))
    fun (x : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) ↦
    ∏ i : ι,
      f i
        ((MeasurableEquiv.piCongrLeft E e :
            (a : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) → (a : ι) → E a)
          x i))
  (∏ i : ι, ∫ (x : E i), f i x ∂μ i)
Tactic: rw [← (measurePreserving_piCongrLeft _ e).integral_comp']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : RCLike 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
e : Fin (card ι) ≃ ι := Equiv.symm (equivFin ι)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)))
      (Measure.pi (α := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)) fun (i' : Fin (card ι)) ↦
        μ ((e : (a : Fin (card ι)) → ι) i'))
      fun (x : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) ↦
      ∏ i : ι,
        f i
          ((MeasurableEquiv.piCongrLeft E e :
              (a : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) → (a : ι) → E a)
            x i))
    (∏ i : ι, ∫ (x : E i), f i x ∂μ i)
have simp_rw : Eq.{u_1 + 1} (α := 𝕜)
  (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)))
    (Measure.pi (α := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)) fun (i' : Fin (card ι)) ↦
      μ ((e : (a : Fin (card ι)) → ι) i'))
    fun (x : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) ↦
    ∏ i : Fin (card ι),
      f ((e : (a : Fin (card ι)) → ι) i)
        ((MeasurableEquiv.piCongrLeft E e :
            (a : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) → (a : ι) → E a)
          x ((e : (a : Fin (card ι)) → ι) i)))
  (∏ i : Fin (card ι),
    ∫ (x : E ((e : (a : Fin (card ι)) → ι) i)),
      f ((e : (a : Fin (card ι)) → ι) i) x ∂μ ((e : (a : Fin (card ι)) → ι) i))
Tactic: simp_rw [← e.prod_comp, MeasurableEquiv.coe_piCongrLeft, Equiv.piCongrLeft_apply_apply,
    MeasureTheory.integral_fin_nat_prod_eq_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : RCLike 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
e : Fin (card ι) ≃ ι := Equiv.symm (equivFin ι)
simp_rw :
  Eq.{u_1 + 1} (α := 𝕜)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)))
      (Measure.pi (α := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)) fun (i' : Fin (card ι)) ↦
        μ ((e : (a : Fin (card ι)) → ι) i'))
      fun (x : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) ↦
      ∏ i : Fin (card ι),
        f ((e : (a : Fin (card ι)) → ι) i)
          ((MeasurableEquiv.piCongrLeft E e :
              (a : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) → (a : ι) → E a)
            x ((e : (a : Fin (card ι)) → ι) i)))
    (∏ i : Fin (card ι),
      ∫ (x : E ((e : (a : Fin (card ι)) → ι) i)),
        f ((e : (a : Fin (card ι)) → ι) i) x ∂μ ((e : (a : Fin (card ι)) → ι) i))
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)))
      (Measure.pi (α := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)) fun (i' : Fin (card ι)) ↦
        μ ((e : (a : Fin (card ι)) → ι) i'))
      fun (x : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) ↦
      ∏ i : ι,
        f i
          ((MeasurableEquiv.piCongrLeft E e :
              (a : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) → (a : ι) → E a)
            x i))
    (∏ i : ι, ∫ (x : E i), f i x ∂μ i)
have simp_rw₁ : Eq.{u_1 + 1} (α := 𝕜)
  (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)))
    (Measure.pi (α := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)) fun (i' : Fin (card ι)) ↦
      μ ((e : (a : Fin (card ι)) → ι) i'))
    fun (x : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) ↦
    ∏ x_1 : Fin (card ι),
      f ((e : (a : Fin (card ι)) → ι) x_1)
        ((Equiv.piCongrLeft E e : (a : (a : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) a)) → (b : ι) → E b) x
          ((e : (a : Fin (card ι)) → ι) x_1)))
  (∏ i : Fin (card ι),
    ∫ (x : E ((e : (a : Fin (card ι)) → ι) i)),
      f ((e : (a : Fin (card ι)) → ι) i) x ∂μ ((e : (a : Fin (card ι)) → ι) i))
Tactic: simp_rw [← e.prod_comp, MeasurableEquiv.coe_piCongrLeft, Equiv.piCongrLeft_apply_apply,
    MeasureTheory.integral_fin_nat_prod_eq_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : RCLike 𝕜
E : Type u_3
f : E → 𝕜
mE : MeasurableSpace E
μ : Measure E
inst_2 : SigmaFinite μ
⊢ (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (x : ι) ↦ E)) (Measure.pi (α := fun (x : ι) ↦ E) fun (x : ι) ↦ μ)
      fun (x : ι → E) ↦ ∏ i : ι, f (x i)) =
    HPow.hPow (α := 𝕜) (∫ (x : E), f x ∂μ) (card ι)
have rw : ∏ i : ι, ∫ (x : E), f x ∂μ = HPow.hPow (α := 𝕜) (∫ (x : E), f x ∂μ) (card ι)
Tactic: rw [integral_fintype_prod_eq_prod, Finset.prod_const, card]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : RCLike 𝕜
E : Type u_3
f : E → 𝕜
mE : MeasurableSpace E
μ : Measure E
inst_2 : SigmaFinite μ
rw : ∏ i : ι, ∫ (x : E), f x ∂μ = HPow.hPow (α := 𝕜) (∫ (x : E), f x ∂μ) (card ι)
⊢ (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (x : ι) ↦ E)) (Measure.pi (α := fun (x : ι) ↦ E) fun (x : ι) ↦ μ)
      fun (x : ι → E) ↦ ∏ i : ι, f (x i)) =
    HPow.hPow (α := 𝕜) (∫ (x : E), f x ∂μ) (card ι)
have rw₁ : HPow.hPow (α := 𝕜) (∫ (x : E), f x ∂μ) (Finset.card.{u_2} (α := ι) Finset.univ) =
  HPow.hPow (α := 𝕜) (∫ (x : E), f x ∂μ) (card ι)
Tactic: rw [integral_fintype_prod_eq_prod, Finset.prod_const, card]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : RCLike 𝕜
E : Type u_3
f : E → 𝕜
mE : MeasurableSpace E
μ : Measure E
inst_2 : SigmaFinite μ
rw : ∏ i : ι, ∫ (x : E), f x ∂μ = HPow.hPow (α := 𝕜) (∫ (x : E), f x ∂μ) (card ι)
rw₁ :
  HPow.hPow (α := 𝕜) (∫ (x : E), f x ∂μ) (Finset.card.{u_2} (α := ι) Finset.univ) =
    HPow.hPow (α := 𝕜) (∫ (x : E), f x ∂μ) (card ι)
⊢ (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (x : ι) ↦ E)) (Measure.pi (α := fun (x : ι) ↦ E) fun (x : ι) ↦ μ)
      fun (x : ι → E) ↦ ∏ i : ι, f (x i)) =
    HPow.hPow (α := 𝕜) (∫ (x : E), f x ∂μ) (card ι)
have rw₂ : HPow.hPow (α := 𝕜) (∫ (x : E), f x ∂μ) (Finset.card.{u_2} (α := ι) Finset.univ) =
  HPow.hPow (α := 𝕜) (∫ (x : E), f x ∂μ) (Finset.card.{u_2} (α := ι) Finset.univ)
Tactic: rw [integral_fintype_prod_eq_prod, Finset.prod_const, card]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
ι : Type u_2
inst : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : ∀ (i : ι), IsFiniteMeasure (μ i)
i : ι
f : X i → E
hf : Integrable f (μ i)
⊢ Integrable (ε := E) (fun (x : (i : ι) → X i) ↦ f (x i)) (Measure.pi (α := X) μ)
have refine : @Integrable _ _ _ _ (mX i) f (map (fun (x : (i : ι) → X i) ↦ x i) (Measure.pi (α := X) μ))
Tactic: refine Integrable.comp_measurable ?_ (by fun_prop)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
ι : Type u_2
inst : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : ∀ (i : ι), IsFiniteMeasure (μ i)
i : ι
f : X i → E
hf : Integrable f (μ i)
⊢ @Integrable _ _ _ _ (mX i) f (map (fun (x : (i : ι) → X i) ↦ x i) (Measure.pi (α := X) μ))
have rw : Integrable f
  (HSMul.hSMul (α := ENNReal) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (X j)) → ENNReal) Set.univ) (μ i))
Tactic: rw [Measure.pi_map_eval]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
ι : Type u_2
inst : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : ∀ (i : ι), IsFiniteMeasure (μ i)
i : ι
f : X i → E
hf : Integrable f (μ i)
⊢ @Integrable _ _ _ _ (mX i) f (map (fun (x : (i : ι) → X i) ↦ x i) (Measure.pi (α := X) μ))
have rw : Integrable f
  (HSMul.hSMul (α := ENNReal) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (X j)) → ENNReal) Set.univ) (μ i))
Tactic: classical
  rw [Measure.pi_map_eval]
  exact hf.smul_measure <| ENNReal.prod_ne_top (by finiteness)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
ι : Type u_2
inst : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
f : X i → E
hf : AEStronglyMeasurable f (μ i)
⊢ Eq.{u_4 + 1} (α := E) (∫ (x : (i : ι) → X i), f (x i) ∂Measure.pi (α := X) μ) (∫ (x : X i), f x ∂μ i)
have hφ : AEMeasurable (Function.eval (β := X) i) (Measure.pi (α := X) μ)
Tactic: rw [← (measurePreserving_eval μ i).map_eq, integral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
ι : Type u_2
inst : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
f : X i → E
hf : AEStronglyMeasurable f (μ i)
hφ : AEMeasurable (Function.eval (β := X) i) (Measure.pi (α := X) μ)
⊢ Eq.{u_4 + 1} (α := E) (∫ (x : (i : ι) → X i), f (x i) ∂Measure.pi (α := X) μ) (∫ (x : X i), f x ∂μ i)
have hfm : AEStronglyMeasurable (m₀ := mX i) f (map (Function.eval (β := X) i) (Measure.pi (α := X) μ))
Tactic: rw [← (measurePreserving_eval μ i).map_eq, integral_map]