awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
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 → 𝕜} (hf : ∀ (i : Fin n), Integrable (f i) (μ i)),
    Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ)
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 → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this_1 :
  MeasurePreserving (α := E 0 × ((j : Fin n) → E (Fin.succAbove 0 j)))
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0)) :
      (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
    (Measure.prod (μ 0)
      (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi (α := E) μ)
this :
  @Integrable.{u_1, u_3} 𝕜 _ _ _ (MeasurableSpace.pi (X := fun (j : Fin n) ↦ E j.succ))
    (fun (x : (j : Fin n) → E j.succ) ↦ ∏ j : Fin n, f j.succ (x j))
    (Measure.pi (α := fun (j : Fin n) ↦ E j.succ) fun (i : Fin n) ↦ μ i.succ)
⊢ @Integrable.{u_1, u_3} 𝕜 _ _ _ Prod.instMeasurableSpace
    (fun (x : E 0 × ((j : Fin n) → E j.succ)) ↦
      f 0
          (({ toFun := fun (f : E 0 × ((i : Fin n) → E i.succ)) ↦ Fin.cons (α := E) f.1 fun (j : Fin n) ↦ f.2 j,
                invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := ⋯,
                right_inv := ⋯ : E 0 × ((i : Fin n) → E i.succ) ≃ ((i : Fin (n + 1)) → E i) } :
              (a : E 0 × ((i : Fin n) → E i.succ)) → (i : Fin (n + 1)) → E i)
            x 0) *
        ∏ i : Fin n,
          f i.succ
            (({ toFun := fun (f : E 0 × ((i : Fin n) → E i.succ)) ↦ Fin.cons (α := E) f.1 fun (j : Fin n) ↦ f.2 j,
                  invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := ⋯,
                  right_inv := ⋯ } :
                (a : E 0 × ((i : Fin n) → E i.succ)) → (i : Fin (n + 1)) → E i)
              x i.succ))
    (Measure.prod (μ 0) (Measure.pi (α := fun (j : Fin n) ↦ E j.succ) fun (j : Fin n) ↦ μ j.succ))

Tactic:
exact Integrable.mul_prod (hf 0) this

Premises used: MeasureTheory.Integrable.mul_prod, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
inst : NormedCommRing 𝕜
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 → 𝕜
hf : ∀ (i : Fin n), Integrable (f i) (μ 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 → 𝕜} (hf : ∀ (i : Fin 0), Integrable (f i) (μ i)),
    Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin 0) → E i) ↦ ∏ i : Fin 0, f i (x i)) (Measure.pi (α := E) μ)
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 → 𝕜} (hf : ∀ (i : Fin n), Integrable (f i) (μ i)),
        Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ))
    {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 → 𝕜}
    (hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)),
    Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin (n + 1)) → E i) ↦ ∏ i : Fin (n + 1), f i (x i))
      (Measure.pi (α := E) μ)
⊢ Integrable.{u_1, u_3} (ε := 𝕜) (fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i)) (Measure.pi (α := E) μ)

Tactic:
induction n with
  | zero => simp only [Finset.univ_eq_empty, Finset.prod_empty, isFiniteMeasure_iff,
      integrable_const_iff, pi_empty_univ, ENNReal.one_lt_top, or_true]
  | succ n n_ih =>
      have := ((measurePreserving_piFinSuccAbove μ 0).symm)
      rw [← this.integrable_comp_emb (MeasurableEquiv.measurableEmbedding _)]
      simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
        Fin.prod_univ_succ, Fin.insertNth_zero]
      simp only [Fin.zero_succAbove, cast_eq, Function.comp_def]
      have : Integrable (fun (x : (j : Fin n) → E (Fin.succ j)) ↦ ∏ j, f (Fin.succ j) (x j))
          (Measure.pi (fun i ↦ μ i.succ)) :=
        n_ih (fun i ↦ hf _)
      exact Integrable.mul_prod (hf 0) this

Premises used: Finset.prod_empty, Fin.zero_succAbove, MeasureTheory.isFiniteMeasure_iff, ENNReal.one_lt_top, Finset.univ_eq_empty, Function.comp_def, Fin.prod_univ_succ, Fin.insertNth_zero, cast_eq, MeasureTheory.integrable_const_iff, Fin.insertNthEquiv, MeasureTheory.Measure.pi_empty_univ, or_true, MeasurableEquiv.piFinSuccAbove_symm_apply
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : NormedCommRing 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hf : ∀ (i : ι), Integrable (f i) (μ i)
e : Fin (card ι) ≃ ι := Equiv.symm (equivFin ι)
simp_rw :
  @Integrable.{u_1, u_3} 𝕜 _ _ _ (MeasurableSpace.pi (X := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)))
    (fun (x : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) ↦
      ∏ x_1 : Fin (card ι), f ((e : (a : Fin (card ι)) → ι) x_1) (x x_1))
    (Measure.pi (α := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)) fun (i' : Fin (card ι)) ↦
      μ ((e : (a : Fin (card ι)) → ι) i'))
⊢ Integrable (ε := 𝕜) (fun (x : (i : ι) → E i) ↦ ∏ i : ι, f i (x i)) (Measure.pi (α := E) μ)

Tactic:
simp_rw [← (measurePreserving_piCongrLeft _ e).integrable_comp_emb
    (MeasurableEquiv.measurableEmbedding _),
    ← e.prod_comp, MeasurableEquiv.coe_piCongrLeft, Function.comp_def,
    Equiv.piCongrLeft_apply_apply]

Premises used: MeasurableEquiv.measurableEmbedding, MeasureTheory.MeasurePreserving.integrable_comp_emb, MeasureTheory.measurePreserving_piCongrLeft, MeasurableEquiv.coe_piCongrLeft, Equiv.prod_comp, Function.comp_def, Equiv.piCongrLeft_apply_apply
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : NormedCommRing 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hf : ∀ (i : ι), Integrable (f i) (μ i)
e : Fin (card ι) ≃ ι := Equiv.symm (equivFin ι)
⊢ @Integrable.{u_1, u_3} 𝕜 _ _ _ (MeasurableSpace.pi (X := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)))
    (fun (x : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) ↦
      ∏ x_1 : Fin (card ι), f ((e : (a : Fin (card ι)) → ι) x_1) (x x_1))
    (Measure.pi (α := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)) fun (i' : Fin (card ι)) ↦
      μ ((e : (a : Fin (card ι)) → ι) i'))

Tactic:
.fin_nat_prod (fun i ↦ hf _)

Premises used: MeasureTheory.Integrable.fin_nat_prod, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : NormedCommRing 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hf : ∀ (i : ι), Integrable (f i) (μ i)
e : Fin (card ι) ≃ ι := Equiv.symm (equivFin ι)
⊢ @Integrable.{u_1, u_3} 𝕜 _ _ _ (MeasurableSpace.pi (X := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)))
    (fun (x : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) ↦
      ∏ x_1 : Fin (card ι), f ((e : (a : Fin (card ι)) → ι) x_1) (x x_1))
    (Measure.pi (α := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)) fun (i' : Fin (card ι)) ↦
      μ ((e : (a : Fin (card ι)) → ι) i'))

Tactic:
exact .fin_nat_prod (fun i ↦ hf _)
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : NormedCommRing 𝕜
E : Type u_3
f : ι → E → 𝕜
mE : MeasurableSpace E
μ : ι → Measure E
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hf : ∀ (i : ι), Integrable (f i) (μ i)
⊢ Integrable (ε := 𝕜) (fun (x : ι → E) ↦ ∏ i : ι, f i (x i)) (Measure.pi (α := fun (a : ι) ↦ E) μ)

Tactic:
Integrable.fintype_prod_dep hf

Premises used: MeasureTheory.Integrable.fintype_prod_dep
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Fin 0 → Type u_3
mE : (i : Fin 0) → MeasurableSpace (E i)
μ : (i : Fin 0) → Measure (E i)
inst_1 : ∀ (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:
simp [measureReal_def]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Integral.Pi
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 :
  Eq.{u_1 + 1} (α := 𝕜)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0)
        (Measure.pi (α := fun (j : Fin n) ↦ E (Fin.succAbove 0 j)) fun (j : Fin n) ↦ μ (Fin.succAbove 0 j)))
      fun (x : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) ↦
      ∏ i : Fin (n + 1),
        f i
          ((MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove E 0) :
              (a : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))) → (j : Fin (n + 1)) → E j)
            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))
⊢ 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:
rw [← ((measurePreserving_piFinSuccAbove μ 0).symm).integral_comp']

Premises used: MeasureTheory.MeasurePreserving.symm, MeasureTheory.measurePreserving_piFinSuccAbove, MeasureTheory.MeasurePreserving.integral_comp', OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Pi
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))
rw₁ 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))
⊢ (@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:
rw [← n_ih, ← integral_prod_mul]

Premises used: MeasureTheory.integral_prod_mul
-- Module: Mathlib.MeasureTheory.Integral.Pi
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 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)
⊢ 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:
rw [Fin.prod_univ_succ]

Premises used: Fin.prod_univ_succ
-- Module: Mathlib.MeasureTheory.Integral.Pi
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)
_₂ :
  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
⊢ 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:
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]

Premises used: MeasureTheory.Measure.prod, MeasureTheory.integral, MeasureTheory.Measure.pi, OfNat.ofNat, Fin
-- Module: Mathlib.MeasureTheory.Integral.Pi
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)
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)
⊢ 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)

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]

Premises used: MeasureTheory.measureReal_def, Fin
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : ℕ
E : Fin n → Type u_3
inst_1 : (i : Fin n) → MeasureSpace (E i)
inst_2 : ∀ (i : Fin n), SigmaFinite.{u_3} (α := E i) (m0 := MeasureSpace.toMeasurableSpace) volume
f : (i : Fin n) → E i → 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : (i : Fin n) → E i) ↦ ∏ i : Fin n, f i (x i))
    (∏ i : Fin n, @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E i) ↦ f i x)

Tactic:
integral_fin_nat_prod_eq_prod _

Premises used: MeasureTheory.integral_fin_nat_prod_eq_prod
-- Module: Mathlib.MeasureTheory.Integral.Pi
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 ι)
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)
⊢ Eq.{u_1 + 1} (α := 𝕜) (∫ (x : (i : ι) → E i), ∏ i : ι, f i (x i) ∂Measure.pi (α := E) μ)
    (∏ i : ι, ∫ (x : E i), f i x ∂μ i)

Tactic:
rw [← (measurePreserving_piCongrLeft _ e).integral_comp']

Premises used: MeasureTheory.measurePreserving_piCongrLeft, MeasureTheory.MeasurePreserving.integral_comp'
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : RCLike 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
inst_2 : (i : ι) → MeasureSpace (E i)
inst_3 : ∀ (i : ι), SigmaFinite.{u_3} (α := E i) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : (i : ι) → E i) ↦ ∏ i : ι, f i (x i))
    (∏ i : ι, @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E i) ↦ f i x)

Tactic:
integral_fintype_prod_eq_prod _

Premises used: MeasureTheory.integral_fintype_prod_eq_prod
-- Module: Mathlib.MeasureTheory.Integral.Pi
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 ι)
rw₂ 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)
⊢ (@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 ι)

Tactic:
rw [integral_fintype_prod_eq_prod, Finset.prod_const, card]

Premises used: MeasureTheory.integral_fintype_prod_eq_prod, Fintype.card, Finset.prod_const
-- Module: Mathlib.MeasureTheory.Integral.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : RCLike 𝕜
E : Type u_3
f : E → 𝕜
inst_2 : MeasureSpace E
inst_3 : SigmaFinite.{u_3} (α := E) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ι → E) ↦ ∏ i : ι, f (x i)) =
    HPow.hPow (α := 𝕜) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : E) ↦ f x) (card ι)

Tactic:
integral_fintype_prod_eq_pow _

Premises used: MeasureTheory.integral_fintype_prod_eq_pow
-- Module: Mathlib.MeasureTheory.Integral.Pi
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)
⊢ Measurable (β := X i) fun (x : (i : ι) → X i) ↦ x i

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.Pi
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)
refine : @Integrable _ _ _ _ (mX i) f (map (fun (x : (i : ι) → X i) ↦ x i) (Measure.pi (α := X) μ))
⊢ Integrable (ε := E) (fun (x : (i : ι) → X i) ↦ f (x i)) (Measure.pi (α := X) μ)

Tactic:
refine Integrable.comp_measurable ?_ (by fun_prop)

Premises used: MeasureTheory.Integrable.comp_measurable
-- Module: Mathlib.MeasureTheory.Integral.Pi
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)
rw :
  Integrable f
    (HSMul.hSMul (α := ENNReal) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (X j)) → ENNReal) Set.univ) (μ i))
⊢ @Integrable _ _ _ _ (mX i) f (map (fun (x : (i : ι) → X i) ↦ x i) (Measure.pi (α := X) μ))

Tactic:
rw [Measure.pi_map_eval]

Premises used: MeasureTheory.Measure.pi_map_eval