-- 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:
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 =>
      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:
have : Integrable (fun (x : (j : Fin n) → E (Fin.succ j)) ↦ ∏ j, f (Fin.succ j) (x j)) :=
  n_ih (fun i ↦ hf _)

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)
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))

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)) ∘ ⇑(MeasurableEquiv.piFinSuccAbove E 0).symm)
    (volume.prod (Measure.pi fun j => volume))

Tactic:
simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
  Fin.prod_univ_succ, Fin.insertNth_zero]

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 => f 0 (x 0) * ∏ i : Fin n, f i.succ (x i.succ)) ∘
      ⇑{ toFun := fun f => Fin.cons f.1 fun j => cast ⋯ (f.2 j), invFun := fun f => (f 0, Fin.removeNth 0 f),
          left_inv := ⋯, right_inv := ⋯ })
    (volume.prod (Measure.pi fun j => 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)
⊢ Integrable
    ((fun x => f 0 (x 0) * ∏ i : Fin n, f i.succ (x i.succ)) ∘
      ⇑{ toFun := fun f => Fin.cons f.1 fun j => cast ⋯ (f.2 j), invFun := fun f => (f 0, Fin.removeNth 0 f),
          left_inv := ⋯, right_inv := ⋯ })
    (volume.prod (Measure.pi fun j => volume))

Tactic:
simp only [Fin.zero_succAbove, cast_eq, Function.comp_def, Fin.cons_zero, Fin.cons_succ]

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 =>
      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))