awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
x : X
hx : x ∈ s
refine_1 : ∀ᶠ (x : X) in 𝓝[s] x, AEStronglyMeasurable (fs x) μ
refine_2 : ∀ᶠ (x : X) in 𝓝[s] x, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
⊢ ContinuousWithinAt.{u_7, u_3} (Y := F) (fun (x : X) ↦ setToFun μ T hT (fs x)) s x
have refine_3 : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s x
Tactic: refine continuousWithinAt_setToFun_of_dominated hT ?_ ?_ bound_integrable ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, AEStronglyMeasurable (fs x) μ
have h : ∀ (a : X),
  Membership.mem (γ := Set X)
    {x : X | x ∈ s → Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ AEStronglyMeasurable (fs x) μ) x} x} a
Tactic: filter_upwards [self_mem_nhdsWithin] with x hx using hfs_meas x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
have h : ∀ (a : X),
  Membership.mem (γ := Set X)
    {x : X | x ∈ s → Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a) x} x} a
Tactic: filter_upwards [self_mem_nhdsWithin] with x hx using h_bound x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᵐ (a : α) ∂μ, ContinuousWithinAt.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s x
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x_1 : α |
      Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s) x}
          x_1 →
        Membership.mem (γ := Set α)
          {x_2 : α | (fun (a : α) ↦ ContinuousWithinAt.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s x) x_2} x_1}
    a
Tactic: filter_upwards [h_cont] with a ha using ha x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
x : X
hx : x ∈ s
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s) x} x_1 →
          Membership.mem (γ := Set α)
            {x_2 : α | (fun (a : α) ↦ ContinuousWithinAt.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s x) x_2} x_1}
      a
⊢ ∀ᵐ (a : α) ∂μ, ContinuousWithinAt.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s x
have h₁ : ∀ (a : α),
  ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s →
    ContinuousWithinAt.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s x
Tactic: filter_upwards [h_cont] with a ha using ha x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.TorusIntegral (goal)
Goal:
n : ℕ
c : Fin n → ℂ
R θ : Fin n → ℝ
⊢ torusMap c R θ - c = torusMap 0 R θ
have h : ∀ (i : Fin n), (torusMap c R θ - c) i = torusMap 0 R θ i
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.TorusIntegral (goal)
Goal:
n : ℕ
E : Type u_1
inst : NormedAddCommGroup E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
⊢ TorusIntegrable f c 0
have 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
Tactic: rw [TorusIntegrable, torusMap_zero_radius]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.TorusIntegral (goal)
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
have 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 * π))
Tactic: refine (hf.norm.const_mul (∏ i, |R i|)).mono' ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.TorusIntegral (goal)
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 * π))
⊢ 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
have 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)‖
Tactic: refine (hf.norm.const_mul (∏ i, |R i|)).mono' ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.TorusIntegral (goal)
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 * π))
have refine_1 : Continuous (Y := ℂ) fun (θ : Fin n → ℝ) ↦ ∏ i : Fin n, (↑(R i) : ℂ) * cexp ((↑(θ i) : ℂ) * I) * I
Tactic: refine (Continuous.aestronglyMeasurable ?_).smul hf.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.TorusIntegral (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
⊢ 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)
have H₁ : 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 _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.TorusIntegral (goal)
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)
have h : ∀ (θ : Fin 1 → ℝ) (i : Fin 1), torusMap c R θ i = circleMap (c 0) (R 0) (θ 0)
Tactic: ext θ i : 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.TorusIntegral (goal)
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 θ i = circleMap (c 0) (R 0) (θ 0)
have h : torusMap c R θ 0 = circleMap (c 0) (R 0) (θ 0)
Tactic: rw [Subsingleton.elim i 0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.TorusIntegral (hypothesis)
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 * π)
⊢ 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)
have H₂ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.TorusIntegral (goal)
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) (∯ (x : Fin 1 → ℂ) in T(c, R), f x) (∮ (z : ℂ) in C(c 0, R 0), f fun (x : Fin 1) ↦ z)
have 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)
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₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.TorusIntegral (hypothesis)
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)
⊢ 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))
have hem : 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 _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.TorusIntegral (hypothesis)
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
⊢ 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))
have 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 * π)
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 _ _)
-- 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 * π)
⊢ 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))
have 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)))
Tactic: rw [torusIntegral, ← hem.map_eq, setIntegral_map_equiv, heπ, Measure.volume_eq_prod,
    setIntegral_prod, circleIntegral_def_Icc]
-- 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 * π)
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)))
⊢ 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))
have 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)
Tactic: rw [torusIntegral, ← hem.map_eq, setIntegral_map_equiv, heπ, Measure.volume_eq_prod,
    setIntegral_prod, circleIntegral_def_Icc]
-- 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 * π)
⊢ 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)))
have refine : ∀ θ ∈ Icc 0 (2 * π),
  (@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) → ℝ) (θ, y) i) : ℂ) * I) * I)
        (f (torusMap c R ((e : (a : ℝ × (Fin n → ℝ)) → Fin (n + 1) → ℝ) (θ, y))))) =
    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: refine setIntegral_congr_fun measurableSet_Icc fun θ _ => ?_
-- 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 ((↑θ : ℂ) * 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))
have e_a : Eq (α := Fin (n + 1) → ℂ)
  (fun (i_1 : Fin (n + 1)) ↦
    c i_1 + (↑(R i_1) : ℂ) * cexp ((↑(i.insertNth (α := fun (x : Fin (n + 1)) ↦ ℝ) θ Θ i_1) : ℂ) * I))
  (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: congr 2