-- 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 * π)
⊢ 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)))
have refine : ∀ (Θ : Fin n → ℝ),
  Membership.mem (γ := Set (Fin n → ℝ)) (Icc 0 fun (x : Fin n) ↦ 2 * π) Θ →
    (((↑(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) → ℝ)
                        (θ, Θ) 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) → ℝ)
                          (θ, Θ) (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) → ℝ)
                        (θ, Θ) 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 (α := 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 ((↑(Θ i_1) : ℂ) * I))
Tactic: refine setIntegral_congr_fun measurableSet_Icc fun Θ _ => ?_