-- 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 * π)
Θ : Fin n → ℝ
h_1 : 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))
have simp : (((↑(R i) : ℂ) * cexp ((↑θ : ℂ) * I) * I * ∏ x : Fin n, (↑(R (i.succAbove x)) : ℂ) * cexp ((↑(Θ x) : ℂ) * I) * I) •
    f fun (i_1 : Fin (n + 1)) ↦
      c i_1 + (↑(R i_1) : ℂ) * cexp ((↑(i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) θ Θ i_1) : ℂ) * I)) =
  ((↑(R i) : ℂ) * cexp ((↑θ : ℂ) * I) * I * ∏ x : Fin n, (↑(R (i.succAbove x)) : ℂ) * cexp ((↑(Θ x) : ℂ) * 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: simp only [MeasurableEquiv.piFinSuccAbove_symm_apply, i.insertNth_apply_same,
      i.insertNth_apply_succAbove, (· ∘ ·), Fin.insertNthEquiv, Equiv.coe_fn_mk]