-- Mathlib/MeasureTheory/Integral/Pi.lean
theorem Integrable.fin_nat_prod {n : ℕ} {E : Fin n → Type*}
    [∀ i, MeasureSpace (E i)] [∀ i, SigmaFinite (volume : Measure (E i))]
    {f : (i : Fin n) → E i → 𝕜} (hf : ∀ i, Integrable (f i)) :
    Integrable (fun (x : (i : Fin n) → E i) ↦ ∏ i, f i (x i))

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : ℕ
E : Fin n → Type u_2
inst✝¹ : (i : Fin n) → MeasureSpace (E i)
inst✝ : ∀ (i : Fin n), SigmaFinite volume
f : (i : Fin n) → E i → 𝕜
hf : ∀ (i : Fin n), Integrable (f i) volume
⊢ Integrable (fun x => ∏ i : Fin n, f i (x i)) volume

Tactic:
induction n with
| zero => simp only [Finset.univ_eq_empty, Finset.prod_empty, volume_pi, isFiniteMeasure_iff,
    integrable_const_iff, one_ne_zero, pi_empty_univ, ENNReal.one_lt_top, or_true]
| succ n n_ih =>
    have := ((measurePreserving_piFinSuccAbove (fun i => (volume : Measure (E i))) 0).symm)
    rw [volume_pi, ← 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, Fin.cons_zero, Fin.cons_succ]
    have : Integrable (fun (x : (j : Fin n) → E (Fin.succ j)) ↦ ∏ j, f (Fin.succ j) (x j)) :=
      n_ih (fun i ↦ hf _)
    exact Integrable.prod_mul (hf 0) this

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_2} [inst : (i : Fin n) → MeasureSpace (E i)] [inst_1 : ∀ (i : Fin n), SigmaFinite volume]
    {f : (i : Fin n) → E i → 𝕜},
    (∀ (i : Fin n), Integrable (f i) volume) → Integrable (fun x => ∏ i : Fin n, f i (x i)) volume
E : Fin (n + 1) → Type u_2
inst✝¹ : (i : Fin (n + 1)) → MeasureSpace (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite volume
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) volume
⊢ Integrable (fun x => ∏ i : Fin (n + 1), f i (x i)) volume

Tactic:
have := ((measurePreserving_piFinSuccAbove (fun i => (volume : Measure (E i))) 0).symm)

Result:
case succ
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_2} [inst : (i : Fin n) → MeasureSpace (E i)] [inst_1 : ∀ (i : Fin n), SigmaFinite volume]
    {f : (i : Fin n) → E i → 𝕜},
    (∀ (i : Fin n), Integrable (f i) volume) → Integrable (fun x => ∏ i : Fin n, f i (x i)) volume
E : Fin (n + 1) → Type u_2
inst✝¹ : (i : Fin (n + 1)) → MeasureSpace (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite volume
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) volume
this :
  MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove E 0).symm) (volume.prod (Measure.pi fun j => volume))
    (Measure.pi fun i => volume)
⊢ Integrable (fun x => ∏ i : Fin (n + 1), f i (x i)) volume

Proof state:
case succ
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_2} [inst : (i : Fin n) → MeasureSpace (E i)] [inst_1 : ∀ (i : Fin n), SigmaFinite volume]
    {f : (i : Fin n) → E i → 𝕜},
    (∀ (i : Fin n), Integrable (f i) volume) → Integrable (fun x => ∏ i : Fin n, f i (x i)) volume
E : Fin (n + 1) → Type u_2
inst✝¹ : (i : Fin (n + 1)) → MeasureSpace (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite volume
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) volume
this✝ :
  MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove E 0).symm) (volume.prod (Measure.pi fun j => volume))
    (Measure.pi fun i => volume)
this : Integrable (fun x => ∏ j : Fin n, f j.succ (x j)) volume
⊢ Integrable
    (fun x =>
      f 0
          ({ toFun := fun f => Fin.cons f.1 fun j => f.2 j, invFun := fun f => (f 0, Fin.removeNth 0 f), left_inv := ⋯,
              right_inv := ⋯ }
            x 0) *
        ∏ i : Fin n,
          f i.succ
            ({ toFun := fun f => Fin.cons f.1 fun j => f.2 j, invFun := fun f => (f 0, Fin.removeNth 0 f),
                left_inv := ⋯, right_inv := ⋯ }
              x i.succ))
    (volume.prod (Measure.pi fun j => volume))

Tactic:
exact Integrable.prod_mul (hf 0) this

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_2} [inst : (i : Fin n) → MeasureSpace (E i)] [inst_1 : ∀ (i : Fin n), SigmaFinite volume]
    {f : (i : Fin n) → E i → 𝕜},
    (∀ (i : Fin n), Integrable (f i) volume) → Integrable (fun x => ∏ i : Fin n, f i (x i)) volume
E : Fin (n + 1) → Type u_2
inst✝¹ : (i : Fin (n + 1)) → MeasureSpace (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite volume
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) volume
this :
  MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove E 0).symm) (volume.prod (Measure.pi fun j => volume))
    (Measure.pi fun i => volume)
⊢ Integrable (fun x => ∏ i : Fin (n + 1), f i (x i)) volume

Tactic:
rw [volume_pi, ← this.integrable_comp_emb (MeasurableEquiv.measurableEmbedding _)]

Result:
case succ
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_2} [inst : (i : Fin n) → MeasureSpace (E i)] [inst_1 : ∀ (i : Fin n), SigmaFinite volume]
    {f : (i : Fin n) → E i → 𝕜},
    (∀ (i : Fin n), Integrable (f i) volume) → Integrable (fun x => ∏ i : Fin n, f i (x i)) volume
E : Fin (n + 1) → Type u_2
inst✝¹ : (i : Fin (n + 1)) → MeasureSpace (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite volume
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) volume
this :
  MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove E 0).symm) (volume.prod (Measure.pi fun j => volume))
    (Measure.pi fun i => volume)
⊢ Integrable ((fun x => ∏ i : Fin (n + 1), f i (x i)) ∘ ⇑(MeasurableEquiv.piFinSuccAbove E 0).symm)
    (volume.prod (Measure.pi fun j => volume))

Proof state:
case zero
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Fin 0 → Type u_2
inst✝¹ : (i : Fin 0) → MeasureSpace (E i)
inst✝ : ∀ (i : Fin 0), SigmaFinite volume
f : (i : Fin 0) → E i → 𝕜
hf : ∀ (i : Fin 0), Integrable (f i) volume
⊢ Integrable (fun x => ∏ i : Fin 0, f i (x i)) volume

Tactic:
simp only [Finset.univ_eq_empty, Finset.prod_empty, volume_pi, isFiniteMeasure_iff,
integrable_const_iff, one_ne_zero, pi_empty_univ, ENNReal.one_lt_top, or_true]

Result:
no goals