-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : 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.symm (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) ↦ ℝ) i)
hem :
  MeasurePreserving (α := ℝ × (Fin n → ℝ)) (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) volume
    volume
heπ :
  preimage (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (Icc 0 fun (x : Fin (n + 1)) ↦ 2 * π) =
    SProd.sprod (β := Set (Fin n → ℝ)) (Icc 0 (2 * π)) (Icc 0 fun (x : Fin n) ↦ 2 * π)
θ : ℝ
h : θ ∈ Icc 0 (2 * π)
simp :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 fun (x : Fin n) ↦ 2 * π))
      fun (y : Fin n → ℝ) ↦
      ((↑(R i) : ℂ) *
              cexp
                ((↑(((MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) ↦ ℝ) i) :
                            ℝ × ((j : Fin n) → ℝ) ≃ᵐ ((j : Fin (n + 1)) → ℝ)) :
                          (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ)
                        (θ, y) i) :
                    ℂ) *
                  I) *
            I *
          ∏ i_1 : Fin n,
            (↑(R (i.succAbove i_1)) : ℂ) *
                cexp
                  ((↑(((MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) ↦ ℝ) i) :
                              ℝ × ((j : Fin n) → ℝ) ≃ᵐ ((j : Fin (n + 1)) → ℝ)) :
                            (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ)
                          (θ, y) (i.succAbove i_1)) :
                      ℂ) *
                    I) *
              I) •
        f fun (i_1 : Fin (n + 1)) ↦
          c i_1 +
            (↑(R i_1) : ℂ) *
              cexp
                ((↑(((MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) ↦ ℝ) i) :
                            ℝ × ((j : Fin n) → ℝ) ≃ᵐ ((j : Fin (n + 1)) → ℝ)) :
                          (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ)
                        (θ, y) i_1) :
                    ℂ) *
                  I))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 fun (x : Fin n) ↦ 2 * π))
      fun (a : Fin n → ℝ) ↦
      ((↑(R i) : ℂ) * cexp ((↑θ : ℂ) * I) * I *
          ∏ i_1 : Fin n, (↑((R ∘ i.succAbove) i_1) : ℂ) * cexp ((↑(a i_1) : ℂ) * I) * I) •
        f
          (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℂ) (circleMap (c i) (R i) θ) fun (i_1 : Fin n) ↦
            (c ∘ i.succAbove) i_1 + (↑((R ∘ i.succAbove) i_1) : ℂ) * cexp ((↑(a i_1) : ℂ) * I)))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 fun (x : Fin n) ↦ 2 * π))
      fun (y : Fin n → ℝ) ↦
      HSMul.hSMul (α := ℂ)
        (∏ i : Fin (n + 1),
          (↑(R i) : ℂ) * cexp ((↑((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (θ, y) i) : ℂ) * I) * I)
        (f (torusMap c R ((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (θ, y))))) =
    HSMul.hSMul (β := E) (deriv (circleMap (c i) (R i)) θ)
      (∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove),
        f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℂ) (circleMap (c i) (R i) θ) y))

Tactic:
simp +unfoldPartialApp only [e, torusIntegral, ← integral_smul,
      deriv_circleMap, i.prod_univ_succAbove _, smul_smul, torusMap, circleMap_zero]

Premises used: MeasureTheory.integral_smul, Fin.prod_univ_succAbove, torusMap, smul_smul, circleMap_zero, deriv_circleMap, torusIntegral