-- Mathlib/MeasureTheory/Integral/TorusIntegral.lean
theorem torusIntegral_dim1 (f : ℂ¹ → E) (c : ℂ¹) (R : ℝ¹) :
    (∯ x in T(c, R), f x) = ∮ z in C(c 0, R 0), f fun _ => z

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
⊢ torusMap c R = fun θ x => circleMap (c 0) (R 0) (θ 0)

Tactic:
ext θ i : 2

Result:
case h.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
θ : Fin 1 → ℝ
i : Fin 1
⊢ torusMap c R θ i = circleMap (c 0) (R 0) (θ 0)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
H₂ : torusMap c R = fun θ x => circleMap (c 0) (R 0) (θ 0)
⊢ (∯ (x : Fin 1 → ℂ) in T(c, R), f x) = ∮ (z : ℂ) in C(c 0, R 0), f fun x => 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₂]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
H₂ : torusMap c R = fun θ x => circleMap (c 0) (R 0) (θ 0)
⊢ ∫ (x : ℝ) in Icc 0 (2 * π),
      (∏ i : Fin 1, ↑(R i) * cexp (↑((MeasurableEquiv.funUnique (Fin 1) ℝ).symm x i) * I) * I) •
        f ((fun θ x => circleMap (c 0) (R 0) (θ 0)) ((MeasurableEquiv.funUnique (Fin 1) ℝ).symm x)) =
    ∫ (x : ℝ) in Icc 0 (2 * π), deriv (circleMap (c 0) (R 0)) x • f fun x_1 => circleMap (c 0) (R 0) x ∂volume

Proof state:
case h.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
θ : Fin 1 → ℝ
i : Fin 1
⊢ torusMap c R θ i = circleMap (c 0) (R 0) (θ 0)

Tactic:
rw [Subsingleton.elim i 0]

Result:
case h.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
θ : Fin 1 → ℝ
i : Fin 1
⊢ torusMap c R θ 0 = circleMap (c 0) (R 0) (θ 0)

Proof state:
case h.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
θ : Fin 1 → ℝ
i : Fin 1
⊢ torusMap c R θ 0 = circleMap (c 0) (R 0) (θ 0)

Tactic:
rfl

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
⊢ (∯ (x : Fin 1 → ℂ) in T(c, R), f x) = ∮ (z : ℂ) in C(c 0, R 0), f fun x => z

Tactic:
have H₁ : (((MeasurableEquiv.funUnique _ _).symm) ⁻¹' Icc 0 fun _ => 2 * π) = Icc 0 (2 * π) :=
  (OrderIso.funUnique (Fin 1) ℝ).symm.preimage_Icc _ _

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
⊢ (∯ (x : Fin 1 → ℂ) in T(c, R), f x) = ∮ (z : ℂ) in C(c 0, R 0), f fun x => z

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
⊢ (∯ (x : Fin 1 → ℂ) in T(c, R), f x) = ∮ (z : ℂ) in C(c 0, R 0), f fun x => z

Tactic:
have H₂ : torusMap c R = fun θ _ ↦ circleMap (c 0) (R 0) (θ 0) := by
  ext θ i : 2
  rw [Subsingleton.elim i 0]; rfl

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
H₂ : torusMap c R = fun θ x => circleMap (c 0) (R 0) (θ 0)
⊢ (∯ (x : Fin 1 → ℂ) in T(c, R), f x) = ∮ (z : ℂ) in C(c 0, R 0), f fun x => z

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)
H₂ : torusMap c R = fun θ x => circleMap (c 0) (R 0) (θ 0)
⊢ ∫ (x : ℝ) in Icc 0 (2 * π),
      (∏ i : Fin 1, ↑(R i) * cexp (↑((MeasurableEquiv.funUnique (Fin 1) ℝ).symm x i) * I) * I) •
        f ((fun θ x => circleMap (c 0) (R 0) (θ 0)) ((MeasurableEquiv.funUnique (Fin 1) ℝ).symm x)) =
    ∫ (x : ℝ) in Icc 0 (2 * π), deriv (circleMap (c 0) (R 0)) x • f fun x_1 => circleMap (c 0) (R 0) x ∂volume

Tactic:
simp [circleMap_zero]

Result:
no goals