-- 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 * π)
this :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (θ : Fin (n + 1) → ℝ) ↦
      HSMul.hSMul (α := ℂ) (∏ i : Fin (n + 1), (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I) (f (torusMap c R θ)))
    (Icc 0 fun (x : Fin (n + 1)) ↦ 2 * π) volume
hf₁ :
  ∀
    (this :
      IntegrableOn.{0, u_1} (α := ℝ × (Fin n → ℝ)) (ε := E) (mα := Prod.instMeasurableSpace)
        ((fun (θ : Fin (n + 1) → ℝ) ↦
            HSMul.hSMul (α := ℂ) (∏ i : Fin (n + 1), (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I) (f (torusMap c R θ))) ∘
          (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ))
        (preimage (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ)
          (Icc 0 fun (x : Fin (n + 1)) ↦ 2 * π))
        volume),
    IntegrableOn.{0, u_1} (ε := E) (mα := Prod.instMeasurableSpace)
      (fun (x : ℝ × (Fin n → ℝ)) ↦
        HSMul.hSMul (α := ℂ)
          (∏ i : Fin (n + 1), (↑(R i) : ℂ) * cexp ((↑((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) x i) : ℂ) * I) * I)
          (f (torusMap c R ((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) x))))
      (SProd.sprod (β := Set (Fin n → ℝ)) (Icc 0 (2 * π)) (Icc 0 fun (x : Fin n) ↦ 2 * π)) (Measure.prod volume volume)
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := Prod.instMeasurableSpace)
    (fun (x : ℝ × (Fin n → ℝ)) ↦
      HSMul.hSMul (α := ℂ)
        (∏ i : Fin (n + 1), (↑(R i) : ℂ) * cexp ((↑((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) x i) : ℂ) * I) * I)
        (f (torusMap c R ((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) x))))
    (SProd.sprod (β := Set (Fin n → ℝ)) (Icc 0 (2 * π)) (Icc 0 fun (x : Fin n) ↦ 2 * π)) (Measure.prod volume volume)
have hf₂ : ∀
  (this :
    IntegrableOn.{0, u_1} (ε := E) (mα := Prod.instMeasurableSpace)
      ((fun (θ : Fin (n + 1) → ℝ) ↦
          HSMul.hSMul (α := ℂ) (∏ i : Fin (n + 1), (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I) (f (torusMap c R θ))) ∘
        (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ))
      (SProd.sprod (β := Set (Fin n → ℝ)) (Icc 0 (2 * π)) (Icc 0 fun (x : Fin n) ↦ 2 * π)) volume),
  IntegrableOn.{0, u_1} (ε := E) (mα := Prod.instMeasurableSpace)
    (fun (x : ℝ × (Fin n → ℝ)) ↦
      HSMul.hSMul (α := ℂ)
        (∏ i : Fin (n + 1), (↑(R i) : ℂ) * cexp ((↑((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) x i) : ℂ) * I) * I)
        (f (torusMap c R ((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) x))))
    (SProd.sprod (β := Set (Fin n → ℝ)) (Icc 0 (2 * π)) (Icc 0 fun (x : Fin n) ↦ 2 * π)) (Measure.prod volume volume)
Tactic: rwa [← hem.integrableOn_comp_preimage e.measurableEmbedding, heπ] at this
Cleared hypotheses: this