-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.TorusIntegral (goal)
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 * π)
⊢ (@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))
have 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)))
Tactic: simp +unfoldPartialApp only [e, torusIntegral, ← integral_smul,
      deriv_circleMap, i.prod_univ_succAbove _, smul_smul, torusMap, circleMap_zero]