-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
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))
⊢ 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))
have 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 sorry (f.2 j),
              invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := sorry,
              right_inv := sorry : 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 sorry (f.2 j),
                invFun := fun (f : (i : Fin (n + 1)) → E i) ↦ (f 0, Fin.removeNth (α := E) 0 f), left_inv := sorry,
                right_inv := sorry } :
              (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))
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]