-- Mathlib/MeasureTheory/Integral/TorusIntegral.lean
theorem torusIntegral_succAbove
    {f : ℂⁿ⁺¹ → E} {c : ℂⁿ⁺¹} {R : ℝⁿ⁺¹} (hf : TorusIntegrable f c R)
    (i : Fin (n + 1)) :
    (∯ x in T(c, R), f x) =
      ∮ x in C(c i, R i), ∯ y in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth x y)

Proof state:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
θ : ℝ
x✝ : θ ∈ Icc 0 (2 * π)
⊢ ∫ (y : Fin n → ℝ) in Icc 0 fun x => 2 * π,
      (∏ i : Fin (n + 1), ↑(R i) * cexp (↑(e (θ, y) i) * I) * I) • f (torusMap c R (e (θ, y))) =
    deriv (circleMap (c i) (R i)) θ •
      ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth (circleMap (c i) (R i) θ) y)

Tactic:
simp (config := { unfoldPartialApp := true }) only [e, torusIntegral, ← integral_smul,
  deriv_circleMap, i.prod_univ_succAbove _, smul_smul, torusMap, circleMap_zero]

Result:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
θ : ℝ
x✝ : θ ∈ Icc 0 (2 * π)
⊢ (∫ (y : Fin n → ℝ) in Icc 0 fun x => 2 * π,
      (↑(R i) * cexp (↑((MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm (θ, y) i) * I) * I *
          ∏ i_1 : Fin n,
            ↑(R (i.succAbove i_1)) *
                cexp (↑((MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm (θ, y) (i.succAbove i_1)) * I) *
              I) •
        f fun i_1 => c i_1 + ↑(R i_1) * cexp (↑((MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm (θ, y) i_1) * I)) =
    ∫ (a : Fin n → ℝ) in Icc 0 fun x => 2 * π,
      (↑(R i) * cexp (↑θ * I) * I * ∏ i_1 : Fin n, ↑((R ∘ i.succAbove) i_1) * cexp (↑(a i_1) * I) * I) •
        f
          (i.insertNth (circleMap (c i) (R i) θ) fun i_1 =>
            (c ∘ i.succAbove) i_1 + ↑((R ∘ i.succAbove) i_1) * cexp (↑(a i_1) * I))

Proof state:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
θ : ℝ
x✝ : θ ∈ Icc 0 (2 * π)
⊢ (∫ (y : Fin n → ℝ) in Icc 0 fun x => 2 * π,
      (↑(R i) * cexp (↑((MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm (θ, y) i) * I) * I *
          ∏ i_1 : Fin n,
            ↑(R (i.succAbove i_1)) *
                cexp (↑((MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm (θ, y) (i.succAbove i_1)) * I) *
              I) •
        f fun i_1 => c i_1 + ↑(R i_1) * cexp (↑((MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm (θ, y) i_1) * I)) =
    ∫ (a : Fin n → ℝ) in Icc 0 fun x => 2 * π,
      (↑(R i) * cexp (↑θ * I) * I * ∏ i_1 : Fin n, ↑((R ∘ i.succAbove) i_1) * cexp (↑(a i_1) * I) * I) •
        f
          (i.insertNth (circleMap (c i) (R i) θ) fun i_1 =>
            (c ∘ i.succAbove) i_1 + ↑((R ∘ i.succAbove) i_1) * cexp (↑(a i_1) * I))

Tactic:
refine setIntegral_congr_fun measurableSet_Icc fun Θ _ => ?_

Result:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
θ : ℝ
x✝¹ : θ ∈ Icc 0 (2 * π)
Θ : Fin n → ℝ
x✝ : Θ ∈ Icc 0 fun x => 2 * π
⊢ ((↑(R i) * cexp (↑((MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm (θ, Θ) i) * I) * I *
        ∏ i_1 : Fin n,
          ↑(R (i.succAbove i_1)) *
              cexp (↑((MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm (θ, Θ) (i.succAbove i_1)) * I) *
            I) •
      f fun i_1 => c i_1 + ↑(R i_1) * cexp (↑((MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm (θ, Θ) i_1) * I)) =
    (↑(R i) * cexp (↑θ * I) * I * ∏ i_1 : Fin n, ↑((R ∘ i.succAbove) i_1) * cexp (↑(Θ i_1) * I) * I) •
      f
        (i.insertNth (circleMap (c i) (R i) θ) fun i_1 =>
          (c ∘ i.succAbove) i_1 + ↑((R ∘ i.succAbove) i_1) * cexp (↑(Θ i_1) * I))

Proof state:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
⊢ (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) =
    ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth x y)

Tactic:
rw [torusIntegral, ← hem.map_eq, setIntegral_map_equiv, heπ, Measure.volume_eq_prod,
  setIntegral_prod, circleIntegral_def_Icc]

Result:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
⊢ ∫ (x : ℝ) in Icc 0 (2 * π),
      ∫ (y : Fin n → ℝ) in Icc 0 fun x => 2 * π,
        (∏ i : Fin (n + 1), ↑(R i) * cexp (↑(e (x, y) i) * I) * I) • f (torusMap c R (e (x, y))) =
    ∫ (θ : ℝ) in Icc 0 (2 * π),
      deriv (circleMap (c i) (R i)) θ •
        ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth (circleMap (c i) (R i) θ) y)

case hf
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
⊢ IntegrableOn (fun x => (∏ i : Fin (n + 1), ↑(R i) * cexp (↑(e x i) * I) * I) • f (torusMap c R (e x)))
    (Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π) (volume.prod volume)