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

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 → 𝕜
⊢ ∫ (x : (i : Fin 0) → E i), ∏ i : Fin 0, f i (x i) = ∏ i : Fin 0, ∫ (x : E i), f i x

Tactic:
simp only [volume_pi, Finset.univ_eq_empty, Finset.prod_empty, integral_const,
  pi_empty_univ, ENNReal.one_toReal, smul_eq_mul, mul_one, pow_zero, one_smul]

Result:
no goals

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 → 𝕜
⊢ ∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) = ∏ i : Fin n, ∫ (x : E i), f i x

Tactic:
induction n with
| zero =>
    simp only [volume_pi, Finset.univ_eq_empty, Finset.prod_empty, integral_const,
      pi_empty_univ, ENNReal.one_toReal, smul_eq_mul, mul_one, pow_zero, one_smul]
| 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) := by
        rw [volume_pi, ← ((measurePreserving_piFinSuccAbove
          (fun i => (volume : Measure (E i))) 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, volume_eq_prod,
          volume_pi, Fin.zero_succAbove, cast_eq, Fin.cons_zero]
      _ = (∫ x, f 0 x) * ∏ i : Fin n, ∫ (x : E (Fin.succ i)), f (Fin.succ i) x := by
        rw [← n_ih, ← integral_prod_mul, volume_eq_prod]
      _ = ∏ i, ∫ x, f i x := by rw [Fin.prod_univ_succ]

Result:
no goals

Proof state:
𝕜 : 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 → 𝕜), ∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) = ∏ i : Fin n, ∫ (x : E i), f i x
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 → 𝕜
⊢ ∫ (x : E 0 × ((i : Fin n) → E i.succ)), f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i) =
    (∫ (x : E 0), f 0 x) * ∏ i : Fin n, ∫ (x : E i.succ), f i.succ x

Tactic:
rw [← n_ih, ← integral_prod_mul, volume_eq_prod]

Result:
no goals

Proof state:
𝕜 : 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 → 𝕜), ∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) = ∏ i : Fin n, ∫ (x : E i), f i x
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 → 𝕜
⊢ ∫ (x : (i : Fin (n + 1)) → E i), ∏ i : Fin (n + 1), f i (x i) =
    ∫ (x : E 0 × ((i : Fin n) → E i.succ)), f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i)

Tactic:
rw [volume_pi, ← ((measurePreserving_piFinSuccAbove
  (fun i => (volume : Measure (E i))) 0).symm).integral_comp']

Result:
𝕜 : 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 → 𝕜), ∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) = ∏ i : Fin n, ∫ (x : E i), f i x
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 → 𝕜
⊢ ∫ (x : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))),
      ∏ i : Fin (n + 1), f i ((MeasurableEquiv.piFinSuccAbove E 0).symm x i) ∂volume.prod (Measure.pi fun j => volume) =
    ∫ (x : E 0 × ((i : Fin n) → E i.succ)), f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i)

Proof state:
𝕜 : 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 → 𝕜), ∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) = ∏ i : Fin n, ∫ (x : E i), f i x
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 → 𝕜
⊢ ∫ (x : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))),
      ∏ i : Fin (n + 1), f i ((MeasurableEquiv.piFinSuccAbove E 0).symm x i) ∂volume.prod (Measure.pi fun j => volume) =
    ∫ (x : E 0 × ((i : Fin n) → E i.succ)), f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i)

Tactic:
simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
  Fin.prod_univ_succ, Fin.insertNth_zero, Equiv.coe_fn_mk, Fin.cons_succ, volume_eq_prod,
  volume_pi, Fin.zero_succAbove, cast_eq, Fin.cons_zero]

Result:
no goals

Proof state:
𝕜 : 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 → 𝕜), ∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) = ∏ i : Fin n, ∫ (x : E i), f i x
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 → 𝕜
⊢ (∫ (x : E 0), f 0 x) * ∏ i : Fin n, ∫ (x : E i.succ), f i.succ x = ∏ i : Fin (n + 1), ∫ (x : E i), f i x

Tactic:
rw [Fin.prod_univ_succ]

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 → 𝕜), ∫ (x : (i : Fin n) → E i), ∏ i : Fin n, f i (x i) = ∏ i : Fin n, ∫ (x : E i), f i x
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 → 𝕜
⊢ ∫ (x : (i : Fin (n + 1)) → E i), ∏ i : Fin (n + 1), f i (x i) = ∏ i : Fin (n + 1), ∫ (x : E i), f i x

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) := by
    rw [volume_pi, ← ((measurePreserving_piFinSuccAbove
      (fun i => (volume : Measure (E i))) 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, volume_eq_prod,
      volume_pi, Fin.zero_succAbove, cast_eq, Fin.cons_zero]
  _ = (∫ x, f 0 x) * ∏ i : Fin n, ∫ (x : E (Fin.succ i)), f (Fin.succ i) x := by
    rw [← n_ih, ← integral_prod_mul, volume_eq_prod]
  _ = ∏ i, ∫ x, f i x := by rw [Fin.prod_univ_succ]

Result:
no goals