-- 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 → 𝕜
simp_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))) ↦
      ∏ x_1 : Fin (n + 1),
        f x_1
          ((Fin.insertNthEquiv E 0 : (a : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) → (i : Fin (n + 1)) → E i) x
            x_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))
simp_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))) ↦
      ∏ x_1 : Fin (n + 1),
        f x_1
          (({ toFun := fun (f : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) ↦ Fin.insertNth (α := E) 0 f.1 f.2,
                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 (Fin.succAbove 0 i))) → (i : Fin (n + 1)) → E i)
            x x_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))
simp_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))) ↦
      f 0
          (({ toFun := fun (f : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) ↦ Fin.insertNth (α := E) 0 f.1 f.2,
                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 (Fin.succAbove 0 i)) ≃ ((i : Fin (n + 1)) → E i) } :
              (a : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) → (i : Fin (n + 1)) → E i)
            x 0) *
        ∏ i : Fin n,
          f i.succ
            (({ toFun := fun (f : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) ↦ Fin.insertNth (α := E) 0 f.1 f.2,
                  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 (Fin.succAbove 0 i))) → (i : Fin (n + 1)) → E i)
              x i.succ))
    (@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))
simp_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))) ↦
      f 0
          (({
                toFun := fun (f : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) ↦
                  Fin.cons (α := E) f.1 fun (j : Fin n) ↦ cast ⋯ (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 (Fin.succAbove 0 i)) ≃ ((i : Fin (n + 1)) → E i) } :
              (a : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) → (i : Fin (n + 1)) → E i)
            x 0) *
        ∏ x_1 : Fin n,
          f x_1.succ
            (({
                  toFun := fun (f : E 0 × ((i : Fin n) → E (Fin.succAbove 0 i))) ↦
                    Fin.cons (α := E) f.1 fun (j : Fin n) ↦ cast ⋯ (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 (Fin.succAbove 0 i))) → (i : Fin (n + 1)) → E i)
              x x_1.succ))
    (@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))
simp_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))) ↦
      f 0 (Fin.cons (α := E) x.1 (fun (j : Fin n) ↦ cast ⋯ (x.2 j)) 0) *
        ∏ x_1 : Fin n, f x_1.succ (Fin.cons (α := E) x.1 (fun (j : Fin n) ↦ cast ⋯ (x.2 j)) x_1.succ))
    (@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))
simp_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))) ↦
      f 0 (Fin.cons (α := E) x.1 (fun (j : Fin n) ↦ cast ⋯ (x.2 j)) 0) * ∏ x_1 : Fin n, f x_1.succ (cast ⋯ (x.2 x_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))
simp_rw₆ :
  Eq.{u_1 + 1} (α := 𝕜)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0) (Measure.pi (α := fun (j : Fin n) ↦ E j.succ) fun (j : Fin n) ↦ μ j.succ))
      fun (x : E 0 × ((j : Fin n) → E j.succ)) ↦
      f 0 (Fin.cons (α := E) x.1 (fun (j : Fin n) ↦ cast ⋯ (x.2 j)) 0) * ∏ x_1 : Fin n, f x_1.succ (cast ⋯ (x.2 x_1)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (j : Fin n) ↦ μ j.succ))
      fun (x : E 0 × ((i : Fin n) → E i.succ)) ↦ f 0 x.1 * ∏ i : Fin n, f i.succ (x.2 i))
simp_rw₇ :
  Eq.{u_1 + 1} (α := 𝕜)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0) (Measure.pi (α := fun (j : Fin n) ↦ E j.succ) fun (j : Fin n) ↦ μ j.succ))
      fun (x : E 0 × ((j : Fin n) → E j.succ)) ↦
      f 0 (Fin.cons (α := E) x.1 (fun (j : Fin n) ↦ x.2 j) 0) * ∏ x_1 : Fin n, f x_1.succ (x.2 x_1))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.prod (μ 0) (Measure.pi (α := fun (i : Fin n) ↦ E i.succ) fun (j : Fin n) ↦ μ j.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} (α := 𝕜)
    (@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))

Tactic:
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]

Premises used: Fin.cons_succ, Fin.zero_succAbove, Fin.prod_univ_succ, Fin.insertNth_zero, cast_eq, Equiv.coe_fn_mk, Fin.insertNthEquiv, Fin.cons_zero, MeasurableEquiv.piFinSuccAbove_symm_apply