awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
c : Fin n → ℂ
⊢ torusMap c 0 = const (Fin n → ℝ) c

Tactic:
funext fun _ ↦ torusMap_eq_center_iff.2 rfl

Premises used: Iff.mpr, torusMap_eq_center_iff, funext, rfl
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
a : E
c : Fin n → ℂ
R : Fin n → ℝ
⊢ TorusIntegrable.{u_1} (E := E) (fun (x : Fin n → ℂ) ↦ a) c R

Tactic:
simp [TorusIntegrable, measure_Icc_lt_top]

Premises used: TorusIntegrable, measure_Icc_lt_top
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
hf : TorusIntegrable f c R
⊢ TorusIntegrable (-f) c R

Tactic:
hf.neg

Premises used: TorusIntegrable, MeasureTheory.IntegrableOn.neg
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
hf : TorusIntegrable f c R
hg : TorusIntegrable g c R
⊢ TorusIntegrable (f + g) c R

Tactic:
hf.add hg

Premises used: TorusIntegrable, MeasureTheory.IntegrableOn.add
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
hf : TorusIntegrable f c R
hg : TorusIntegrable g c R
⊢ TorusIntegrable (f - g) c R

Tactic:
hf.sub hg

Premises used: MeasureTheory.IntegrableOn.sub, TorusIntegrable
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
rw :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (θ : Fin n → ℝ) ↦ f (const (Fin n → ℝ) c θ)) (Icc 0 fun (x : Fin n) ↦ 2 * π) volume
⊢ TorusIntegrable f c 0

Tactic:
rw [TorusIntegrable, torusMap_zero_radius]

Premises used: torusMap_zero_radius, TorusIntegrable
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (θ : Fin n → ℝ) ↦ f (const (Fin n → ℝ) c θ)) (Icc 0 fun (x : Fin n) ↦ 2 * π) volume

Tactic:
apply torusIntegrable_const (f c) c 0

Premises used: TorusIntegrable.torusIntegrable_const, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst_1 : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (θ : Fin n → ℝ) ↦
      HSMul.hSMul (α := ℂ) (∏ i : Fin n, (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I) (f (torusMap c R θ)))
    (Icc 0 fun (x : Fin n) ↦ 2 * π) volume

Tactic:
(hf.norm.const_mul (∏ i, |R i|)).mono' ?_ ?_

Premises used: Finset.univ, abs, MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mono', MeasureTheory.IntegrableOn, Finset.prod, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst_1 : NormedSpace ℂ E
hf : TorusIntegrable f c R
refine_1 :
  AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (θ : Fin n → ℝ) ↦
      HSMul.hSMul (α := ℂ) (∏ i : Fin n, (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I) (f (torusMap c R θ)))
    (Measure.restrict volume (Icc 0 fun (x : Fin n) ↦ 2 * π))
refine_2 :
  ∀ᵐ (a : Fin n → ℝ) ∂Measure.restrict volume (Icc 0 fun (x : Fin n) ↦ 2 * π),
    ‖HSMul.hSMul (α := ℂ) (∏ i : Fin n, (↑(R i) : ℂ) * cexp ((↑(a i) : ℂ) * I) * I) (f (torusMap c R a))‖ ≤
      (∏ i : Fin n, |R i|) * ‖f (torusMap c R a)‖
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (θ : Fin n → ℝ) ↦
      HSMul.hSMul (α := ℂ) (∏ i : Fin n, (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I) (f (torusMap c R θ)))
    (Icc 0 fun (x : Fin n) ↦ 2 * π) volume

Tactic:
refine (hf.norm.const_mul (∏ i, |R i|)).mono' ?_ ?_

Premises used: Finset.univ, abs, MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mono', Finset.prod, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst_1 : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (θ : Fin n → ℝ) ↦
      HSMul.hSMul (α := ℂ) (∏ i : Fin n, (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I) (f (torusMap c R θ)))
    (Measure.restrict volume (Icc 0 fun (x : Fin n) ↦ 2 * π))

Tactic:
(Continuous.aestronglyMeasurable ?_).smul hf.1

Premises used: And.left, Continuous.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.smul
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst_1 : NormedSpace ℂ E
hf : TorusIntegrable f c R
refine_1 : Continuous (Y := ℂ) fun (θ : Fin n → ℝ) ↦ ∏ i : Fin n, (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I
⊢ AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (θ : Fin n → ℝ) ↦
      HSMul.hSMul (α := ℂ) (∏ i : Fin n, (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I) (f (torusMap c R θ)))
    (Measure.restrict volume (Icc 0 fun (x : Fin n) ↦ 2 * π))

Tactic:
refine (Continuous.aestronglyMeasurable ?_).smul hf.1

Premises used: And.left, Continuous.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.smul
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst_1 : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ Continuous (Y := ℂ) fun (θ : Fin n → ℝ) ↦ ∏ i : Fin n, (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
inst_1 : NormedSpace ℂ E
hf : TorusIntegrable f c R
⊢ ∀ᵐ (a : Fin n → ℝ) ∂Measure.restrict volume (Icc 0 fun (x : Fin n) ↦ 2 * π),
    ‖HSMul.hSMul (α := ℂ) (∏ i : Fin n, (↑(R i) : ℂ) * cexp ((↑(a i) : ℂ) * I) * I) (f (torusMap c R a))‖ ≤
      (∏ i : Fin n, |R i|) * ‖f (torusMap c R a)‖

Tactic:
simp [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
hn : n ≠ 0
f : (Fin n → ℂ) → E
c : Fin n → ℂ
⊢ Eq.{u_1 + 1} (α := E) (∯ (x : Fin n → ℂ) in T(c, 0), f x) 0

Tactic:
simp only [torusIntegral, Pi.zero_apply, ofReal_zero, zero_mul, Fin.prod_const,
    zero_pow hn, zero_smul, integral_zero]

Premises used: MulZeroClass.zero_mul, Pi.zero_apply, Fin.prod_const, Complex.ofReal_zero, zero_smul, torusIntegral, MeasureTheory.integral_zero, zero_pow
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
⊢ Eq.{u_1 + 1} (α := E) (∯ (x : Fin n → ℂ) in T(c, R), -f x) (-∯ (x : Fin n → ℂ) in T(c, R), f x)

Tactic:
simp [torusIntegral, integral_neg]

Premises used: MeasureTheory.integral_neg, torusIntegral
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
hf : TorusIntegrable f c R
hg : TorusIntegrable g c R
⊢ (∯ (x : Fin n → ℂ) in T(c, R), f x + g x) =
    HAdd.hAdd (α := E) (∯ (x : Fin n → ℂ) in T(c, R), f x) (∯ (x : Fin n → ℂ) in T(c, R), g x)

Tactic:
simpa only [torusIntegral, smul_add, Pi.add_apply] using
    integral_add hf.function_integrable hg.function_integrable

Premises used: Pi.add_apply, torusIntegral, TorusIntegrable.function_integrable, MeasureTheory.integral_add, smul_add
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
hf : TorusIntegrable f c R
hg : TorusIntegrable g c R
⊢ (∯ (x : Fin n → ℂ) in T(c, R), f x - g x) =
    HSub.hSub (α := E) (∯ (x : Fin n → ℂ) in T(c, R), f x) (∯ (x : Fin n → ℂ) in T(c, R), g x)

Tactic:
simpa only [sub_eq_add_neg, ← torusIntegral_neg] using torusIntegral_add hf hg.neg

Premises used: torusIntegral_add, sub_eq_add_neg, torusIntegral_neg, TorusIntegrable.neg
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
𝕜 : Type u_2
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass 𝕜 ℂ E
a : 𝕜
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
⊢ (∯ (x : Fin n → ℂ) in T(c, R), a • f x) = HSMul.hSMul (β := E) a (∯ (x : Fin n → ℂ) in T(c, R), f x)

Tactic:
simp only [torusIntegral, integral_smul, ← smul_comm a (_ : ℂ) (_ : E)]

Premises used: MeasureTheory.integral_smul, torusIntegral, SMulCommClass.smul_comm
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
a : ℂ
f : (Fin n → ℂ) → ℂ
c : Fin n → ℂ
R : Fin n → ℝ
⊢ (∯ (x : Fin n → ℂ) in T(c, R), a * f x) = a * ∯ (x : Fin n → ℂ) in T(c, R), f x

Tactic:
torusIntegral_smul a f c R

Premises used: torusIntegral_smul
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
C : ℝ
hf : ∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C
θ : Fin n → ℝ
h : Membership.mem (γ := Set (Fin n → ℝ)) (Icc 0 fun (x : Fin n) ↦ 2 * π) θ
⊢ ‖HSMul.hSMul (α := ℂ) (∏ i : Fin n, (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I) (f (torusMap c R θ))‖ =
    (∏ i : Fin n, |R i|) * ‖f (torusMap c R θ)‖

Tactic:
simp [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
C : ℝ
hf : ∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C
θ : Fin n → ℝ
h : Membership.mem (γ := Set (Fin n → ℝ)) (Icc 0 fun (x : Fin n) ↦ 2 * π) θ
⊢ LE.le (α := ℝ) 0 (∏ i : Fin n, |R i|)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
C : ℝ
hf : ∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C
⊢ (∏ i : Fin n, |R i|) * C *
      ENNReal.toReal ((volume : (a : Set (Fin n → ℝ)) → ENNReal) (Icc 0 fun (x : Fin n) ↦ 2 * π)) =
    ((2 * π) ^ n * ∏ i : Fin n, |R i|) * C

Tactic:
simp only [Pi.zero_def, Real.volume_Icc_pi_toReal fun _ => Real.two_pi_pos.le, sub_zero,
        Fin.prod_const, mul_assoc, mul_comm ((2 * π) ^ (n : ℕ))]

Premises used: Real.pi, HMul.hMul, sub_zero, mul_assoc, Real.volume_Icc_pi_toReal, LT.lt.le, Fin.prod_const, Real.two_pi_pos, Pi.zero_def, HPow.hPow, mul_comm, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : (Fin 0 → ℂ) → E
c : Fin 0 → ℂ
R : Fin 0 → ℝ
⊢ (∯ (x : Fin 0 → ℂ) in T(c, R), f x) = f c

Tactic:
simp only [torusIntegral, Fin.prod_univ_zero, one_smul,
    Subsingleton.elim (fun _ : Fin 0 => 2 * π) 0, Icc_self, Measure.restrict_singleton, volume_pi,
    integral_dirac, Measure.pi_of_empty (fun _ : Fin 0 ↦ volume) 0,
    Measure.dirac_apply_of_mem (mem_singleton _), Subsingleton.elim (torusMap c R 0) c]

Premises used: MeasureTheory.Measure.restrict_singleton, Set.mem_singleton, MeasureTheory.volume_pi, Set.Icc_self, Real.pi, HMul.hMul, MeasureTheory.Measure.pi_of_empty, torusMap, Fin.prod_univ_zero, MeasureTheory.integral_dirac, one_smul, MeasureTheory.Measure.dirac_apply_of_mem, MeasureTheory.MeasureSpace.volume, torusIntegral, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
⊢ preimage (β := Fin 1 → ℝ) (⇑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) : (a : ℝ) → Fin 1 → ℝ)
      (Icc 0 fun (x : Fin 1) ↦ 2 * π) =
    Icc 0 (2 * π)

Tactic:
have H₁ : (((MeasurableEquiv.funUnique _ _).symm) ⁻¹' Icc 0 fun _ => 2 * π) = Icc 0 (2 * π) :=
    (OrderIso.funUnique (Fin 1) ℝ).symm.preimage_Icc _ _
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ :
  preimage (β := Fin 1 → ℝ) (⇑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) : (a : ℝ) → Fin 1 → ℝ)
      (Icc 0 fun (x : Fin 1) ↦ 2 * π) =
    Icc 0 (2 * π)
h : ∀ (θ : Fin 1 → ℝ) (i : Fin 1), torusMap c R θ i = circleMap (c 0) (R 0) (θ 0)
⊢ torusMap c R = fun (θ : Fin 1 → ℝ) (x : Fin 1) ↦ circleMap (c 0) (R 0) (θ 0)

Tactic:
ext θ i : 2
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ :
  preimage (β := Fin 1 → ℝ) (⇑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) : (a : ℝ) → Fin 1 → ℝ)
      (Icc 0 fun (x : Fin 1) ↦ 2 * π) =
    Icc 0 (2 * π)
θ : Fin 1 → ℝ
i : Fin 1
h : torusMap c R θ 0 = circleMap (c 0) (R 0) (θ 0)
⊢ torusMap c R θ i = circleMap (c 0) (R 0) (θ 0)

Tactic:
rw [Subsingleton.elim i 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ :
  preimage (β := Fin 1 → ℝ) (⇑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) : (a : ℝ) → Fin 1 → ℝ)
      (Icc 0 fun (x : Fin 1) ↦ 2 * π) =
    Icc 0 (2 * π)
θ : Fin 1 → ℝ
i : Fin 1
⊢ torusMap c R θ 0 = circleMap (c 0) (R 0) (θ 0)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ :
  preimage (β := Fin 1 → ℝ) (⇑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) : (a : ℝ) → Fin 1 → ℝ)
      (Icc 0 fun (x : Fin 1) ↦ 2 * π) =
    Icc 0 (2 * π)
⊢ torusMap c R = fun (θ : Fin 1 → ℝ) (x : Fin 1) ↦ circleMap (c 0) (R 0) (θ 0)

Tactic:
have H₂ : torusMap c R = fun θ _ ↦ circleMap (c 0) (R 0) (θ 0) := by
    ext θ i : 2
    rw [Subsingleton.elim i 0]; rfl
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ :
  preimage (β := Fin 1 → ℝ) (⇑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) : (a : ℝ) → Fin 1 → ℝ)
      (Icc 0 fun (x : Fin 1) ↦ 2 * π) =
    Icc 0 (2 * π)
H₂ : torusMap c R = fun (θ : Fin 1 → ℝ) (x : Fin 1) ↦ circleMap (c 0) (R 0) (θ 0)
rw :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 (2 * π))) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ)
        (∏ i : Fin 1,
          (↑(R i) : ℂ) *
              cexp
                ((↑((MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ) : (a : ℝ) → Fin 1 → ℝ) x i) : ℂ) * I) *
            I)
        (f
          ((fun (θ : Fin 1 → ℝ) (x : Fin 1) ↦ circleMap (c 0) (R 0) (θ 0))
            ((MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ) : (a : ℝ) → Fin 1 → ℝ) x))))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Icc 0 (2 * π))) fun (x : ℝ) ↦
      deriv (circleMap (c 0) (R 0)) x • f fun (x_1 : Fin 1) ↦ circleMap (c 0) (R 0) x)
⊢ Eq.{u_1 + 1} (α := E) (∯ (x : Fin 1 → ℂ) in T(c, R), f x) (∮ (z : ℂ) in C(c 0, R 0), f fun (x : Fin 1) ↦ z)

Tactic:
rw [torusIntegral, circleIntegral, intervalIntegral.integral_of_le Real.two_pi_pos.le,
    Measure.restrict_congr_set Ioc_ae_eq_Icc,
    ← ((volume_preserving_funUnique (Fin 1) ℝ).symm _).setIntegral_preimage_emb
      (MeasurableEquiv.measurableEmbedding _), H₁, H₂]

Premises used: MeasurableEquiv.measurableEmbedding, Real, MeasureTheory.Measure.restrict_congr_set, MeasureTheory.MeasurePreserving.symm, MeasureTheory.MeasurePreserving.setIntegral_preimage_emb, LT.lt.le, MeasureTheory.Ioc_ae_eq_Icc, Real.two_pi_pos, intervalIntegral.integral_of_le, torusIntegral, circleIntegral, OfNat.ofNat, Fin, MeasureTheory.volume_preserving_funUnique
-- Module: Mathlib.MeasureTheory.Integral.TorusIntegral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ :
  preimage (β := Fin 1 → ℝ) (⇑(MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ)) : (a : ℝ) → Fin 1 → ℝ)
      (Icc 0 fun (x : Fin 1) ↦ 2 * π) =
    Icc 0 (2 * π)
H₂ : torusMap c R = fun (θ : Fin 1 → ℝ) (x : Fin 1) ↦ circleMap (c 0) (R 0) (θ 0)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 (2 * π))) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℂ)
        (∏ i : Fin 1,
          (↑(R i) : ℂ) *
              cexp
                ((↑((MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ) : (a : ℝ) → Fin 1 → ℝ) x i) : ℂ) * I) *
            I)
        (f
          ((fun (θ : Fin 1 → ℝ) (x : Fin 1) ↦ circleMap (c 0) (R 0) (θ 0))
            ((MeasurableEquiv.symm (MeasurableEquiv.funUnique (Fin 1) ℝ) : (a : ℝ) → Fin 1 → ℝ) x))))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Icc 0 (2 * π))) fun (x : ℝ) ↦
      deriv (circleMap (c 0) (R 0)) x • f fun (x_1 : Fin 1) ↦ circleMap (c 0) (R 0) x)

Tactic:
simp [circleMap_zero]

Premises used: circleMap_zero
-- 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)
⊢ MeasurePreserving (α := ℝ × (Fin n → ℝ)) (β := Fin (n + 1) → ℝ) (⇑e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) volume
    volume

Tactic:
have hem : MeasurePreserving e :=
    (volume_preserving_piFinSuccAbove (fun _ : Fin (n + 1) => ℝ) i).symm _
-- 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
⊢ 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 * π)

Tactic:
have heπ : (e ⁻¹' Icc 0 fun _ => 2 * π) = Icc 0 (2 * π) ×ˢ Icc (0 : ℝⁿ) fun _ => 2 * π :=
    ((Fin.insertNthOrderIso (fun _ => ℝ) i).preimage_Icc _ _).trans (Icc_prod_eq _ _)
-- 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 * π)
rw :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 (2 * π))) fun (x : ℝ) ↦
      @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) → ℝ) (x, y) i) : ℂ) * I) * I)
          (f (torusMap c R ((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (x, y)))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 (2 * π))) fun (θ : ℝ) ↦
      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)))
hf₁ :
  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)
⊢ Eq.{u_1 + 1} (α := E) (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x)
    (∮ (x : ℂ) in C(c i, R i),
      ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℂ) x y))

Tactic:
rw [torusIntegral, ← hem.map_eq, setIntegral_map_equiv, heπ, Measure.volume_eq_prod,
    setIntegral_prod, circleIntegral_def_Icc]

Premises used: circleIntegral_def_Icc, MeasureTheory.setIntegral_map_equiv, MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.Measure.volume_eq_prod, torusIntegral, MeasureTheory.setIntegral_prod
-- 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 * π)
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 (2 * π))) fun (x : ℝ) ↦
      @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) → ℝ) (x, y) i) : ℂ) * I) * I)
          (f (torusMap c R ((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (x, y)))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 (2 * π))) fun (θ : ℝ) ↦
      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:
setIntegral_congr_fun measurableSet_Icc fun θ _ => ?_

Premises used: MeasureTheory.setIntegral_congr_fun, measurableSet_Icc