awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
this :
  Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
    (Measure.map
      (fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) (i : d) ↦
        (↑((↑x : d → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
⊢ Eq (α := Measure (UnitAddTorus d)) (volume : Measure (UnitAddTorus d))
    (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
      (⇑(measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
have simp_rw : Eq.{u_1 + 1} (α := Measure (UnitAddTorus d)) (volume : Measure (UnitAddTorus d))
  (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
    (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
      (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
Tactic: simp_rw [coe_symm_measurableEquivPiIoc, ← this]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
this :
  Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
    (Measure.map
      (fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) (i : d) ↦
        (↑((↑x : d → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
⊢ Eq.{u_1 + 1} (α := Measure (UnitAddTorus d)) (volume : Measure (UnitAddTorus d))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
have h : Eq.{u_1 + 1} (α := Measure (UnitAddTorus d)) (volume : Measure (UnitAddTorus d))
  (Measure.pi (α := fun (i : d) ↦ HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)) fun (i : d) ↦
    volume)
Tactic: convert! (measurePreserving_pi _ _ (fun i => AddCircle.measurePreserving_mk 1 (a i))).map_eq.symm
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
this :
  Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
    (Measure.map
      (fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) (i : d) ↦
        (↑((↑x : d → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
h :
  Eq.{u_1 + 1} (α := Measure (UnitAddTorus d)) (volume : Measure (UnitAddTorus d))
    (Measure.pi (α := fun (i : d) ↦ HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
      fun (i : d) ↦ volume)
⊢ Eq.{u_1 + 1} (α := Measure (UnitAddTorus d)) (volume : Measure (UnitAddTorus d))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
have h₁ : Eq.{u_1 + 1} (α := Measure (d → ℝ))
  (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
    (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
    (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
  (Measure.pi (α := fun (i : d) ↦ ℝ) fun (i : d) ↦ Measure.restrict volume (Ioc (a i) (a i + 1)))
Tactic: convert! (measurePreserving_pi _ _ (fun i => AddCircle.measurePreserving_mk 1 (a i))).map_eq.symm
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
this :
  Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
    (Measure.map
      (fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) (i : d) ↦
        (↑((↑x : d → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
⊢ Eq.{u_1 + 1} (α := Measure (d → ℝ))
    (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
      (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
    (Measure.pi (α := fun (i : d) ↦ ℝ) fun (i : d) ↦ Measure.restrict volume (Ioc (a i) (a i + 1)))
have h : Eq.{u_1 + 1} (α := Measure (d → ℝ))
  (Measure.pi (α := fun (i : d) ↦ ℝ) fun (i : d) ↦ Measure.restrict volume (Ioc (a i) (a i + 1)))
  (Measure.restrict volume {f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)})
Tactic: convert!
    (map_comap_subtype_coe (MeasurableSet.univ_pi' (fun i => measurableSet_Ioc (a := a i))) volume)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
this :
  Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
    (Measure.map
      (fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) (i : d) ↦
        (↑((↑x : d → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
⊢ Eq.{u_1 + 1} (α := Measure (d → ℝ))
    (Measure.pi (α := fun (i : d) ↦ ℝ) fun (i : d) ↦ Measure.restrict volume (Ioc (a i) (a i + 1)))
    (Measure.restrict volume {f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)})
have h : Eq.{u_1 + 1} (α := Set ((i : d) → ℝ)) {f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)}
  (Set.pi (α := fun (i : d) ↦ ℝ) univ fun (i : d) ↦ Ioc (a i) (a i + 1))
Tactic: convert! (Measure.restrict_pi_pi (fun i => volume) (fun i => Ioc (a i) (a i + 1))).symm
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
⊢ ∫⁻ (x : UnitAddTorus d), f x =
    ∫⁻ (x : d → ℝ) in {x : d → ℝ | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)},
      f fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1)
have h : Eq.{u_1 + 1} (α := MeasurableSpace (UnitAddTorus d)) MeasureSpace.toMeasurableSpace
    (MeasurableSpace.pi (X := fun (a : d) ↦ UnitAddCircle)) →
  Eq (α := Measure (UnitAddTorus d)) volume
    (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
      (⇑(measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
Tactic: convert! lintegral_map_equiv (μ := volume.comap Subtype.val) f (measurableEquivPiIoc a).symm
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
h :
  Eq.{u_1 + 1} (α := MeasurableSpace (UnitAddTorus d)) MeasureSpace.toMeasurableSpace
      (MeasurableSpace.pi (X := fun (a : d) ↦ UnitAddCircle)) →
    Eq (α := Measure (UnitAddTorus d)) volume
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (⇑(measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
⊢ ∫⁻ (x : UnitAddTorus d), f x =
    ∫⁻ (x : d → ℝ) in {x : d → ℝ | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)},
      f fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1)
have h₁ : (∫⁻ (x : d → ℝ) in {x : d → ℝ | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)},
    f fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1)) =
  ∫⁻ (a_1 : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }),
    f
      (((measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
        a_1) ∂Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume
Tactic: convert! lintegral_map_equiv (μ := volume.comap Subtype.val) f (measurableEquivPiIoc a).symm
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
⊢ (∫⁻ (x : d → ℝ) in {x : d → ℝ | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)},
      f fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1)) =
    ∫⁻ (a_1 : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }),
      f
        (((measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
          a_1) ∂Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume
have h : ∫⁻ (x : (↑{f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)} : Type u_1)),
    f fun (i : d) ↦
      (↑((↑x : (i : d) → ℝ) i) :
        ℝ ⧸
          AddSubgroup.zmultiples
            1) ∂Measure.comap
      (Subtype.val (p := fun (x : (i : d) → ℝ) ↦
        Membership.mem (γ := Set ((i : d) → ℝ)) {f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)} x))
      (volume : Measure (d → ℝ)) =
  ∫⁻ (a_1 : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }),
    f
      (((measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
        a_1) ∂Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume
Tactic: rw [← lintegral_subtype_comap (MeasurableSet.univ_pi' (fun i => measurableSet_Ioc))]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : UnitAddTorus d → E
a : d → ℝ
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦ f x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume {x : d → ℝ | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)}) fun (x : d → ℝ) ↦
      f fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
have h : Eq.{u_1 + 1} (α := MeasurableSpace (UnitAddTorus d)) MeasureSpace.toMeasurableSpace
    (MeasurableSpace.pi (X := fun (a : d) ↦ UnitAddCircle)) →
  Eq (α := Measure (UnitAddTorus d)) volume
    (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
      (⇑(measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
Tactic: convert! integral_map_equiv (μ := volume.comap Subtype.val) (measurableEquivPiIoc a).symm f
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : UnitAddTorus d → E
a : d → ℝ
h :
  Eq.{u_1 + 1} (α := MeasurableSpace (UnitAddTorus d)) MeasureSpace.toMeasurableSpace
      (MeasurableSpace.pi (X := fun (a : d) ↦ UnitAddCircle)) →
    Eq (α := Measure (UnitAddTorus d)) volume
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (⇑(measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦ f x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume {x : d → ℝ | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)}) fun (x : d → ℝ) ↦
      f fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
have h₁ : Eq.{u_3 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
    (Measure.restrict volume {x : d → ℝ | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)}) fun (x : d → ℝ) ↦
    f fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
  (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
    (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)
    fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) ↦
    f
      (((measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
        x))
Tactic: convert! integral_map_equiv (μ := volume.comap Subtype.val) (measurableEquivPiIoc a).symm f
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : UnitAddTorus d → E
a : d → ℝ
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume {x : d → ℝ | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)}) fun (x : d → ℝ) ↦
      f fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)
      fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) ↦
      f
        (((measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
          x))
have h : Eq.{u_3 + 1} (α := E)
  (@integral _ _ _ _
    (Subtype.instMeasurableSpace (p := fun (x : (i : d) → ℝ) ↦
      Membership.mem (γ := Set ((i : d) → ℝ)) {f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)} x))
    (Measure.comap
      (Subtype.val (p := fun (x : (i : d) → ℝ) ↦
        Membership.mem (γ := Set ((i : d) → ℝ)) {f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)} x))
      (volume : Measure (d → ℝ)))
    fun (x : (↑{f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)} : Type u_1)) ↦
    f fun (i : d) ↦ (↑((↑x : (i : d) → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1))
  (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
    (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)
    fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) ↦
    f
      (((measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
        x))
Tactic: rw [← integral_subtype_comap (MeasurableSet.univ_pi' (fun i => measurableSet_Ioc))]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
⊢ Orthonormal.{0, u_1, u_1} ℂ (E := ↥(Lp ℂ 2 volume)) (mFourierLp 2)
have rw : ∀ (i j : d → ℤ), inner ℂ (E := ↥(Lp ℂ 2 volume)) (mFourierLp 2 i) (mFourierLp 2 j) = if i = j then 1 else 0
Tactic: rw [orthonormal_iff_ite]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
m n : d → ℤ
⊢ inner ℂ (E := ↥(Lp ℂ 2 volume)) (mFourierLp 2 m) (mFourierLp 2 n) = if m = n then 1 else 0
have simp : Eq (α := ℂ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦
    (mFourier (n + -m) : (a : UnitAddTorus d) → ℂ) x)
  (if m = n then 1 else 0)
Tactic: simp only [ContinuousMap.inner_toLp, ← mFourier_neg, ← mFourier_add]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
m n : d → ℤ
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦
      (mFourier (n + -m) : (a : UnitAddTorus d) → ℂ) x)
    (if m = n then 1 else 0)
have pos : ∀ (h : m = n),
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦
      (mFourier (n + -m) : (a : UnitAddTorus d) → ℂ) x)
    1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
m n : d → ℤ
pos :
  ∀ (h : m = n),
    Eq (α := ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦
        (mFourier (n + -m) : (a : UnitAddTorus d) → ℂ) x)
      1
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦
      (mFourier (n + -m) : (a : UnitAddTorus d) → ℂ) x)
    (if m = n then 1 else 0)
have neg : ∀ (h : ¬m = n),
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦
      (mFourier (n + -m) : (a : UnitAddTorus d) → ℂ) x)
    0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
m n : d → ℤ
h : ¬m = n
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦
      (mFourier (n + -m) : (a : UnitAddTorus d) → ℂ) x)
    0
have neg : Eq (α := ℂ)
  (∏ i : d,
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddCircle) ↦
      (fourier ((n + -m) i) : (a : AddCircle 1) → ℂ) x)
  0
Tactic: rw [mFourier, ContinuousMap.coe_mk, MeasureTheory.integral_fintype_prod_volume_eq_prod]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
m n : d → ℤ
h : ¬m = n
⊢ Eq (α := ℂ)
    (∏ i : d,
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddCircle) ↦
        (fourier ((n + -m) i) : (a : AddCircle 1) → ℂ) x)
    0
have neg : ∀ (i : d) (hi : m i ≠ n i),
  Eq (α := ℂ)
    (∏ i : d,
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddCircle) ↦
        (fourier ((n + -m) i) : (a : AddCircle 1) → ℂ) x)
    0
Tactic: obtain ⟨i, hi⟩ := Function.ne_iff.mp h
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
m n : d → ℤ
h : ¬m = n
i : d
hi : m i ≠ n i
⊢ Eq (α := ℂ)
    (∏ i : d,
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddCircle) ↦
        (fourier ((n + -m) i) : (a : AddCircle 1) → ℂ) x)
    0
have neg : Eq (α := ℂ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddCircle) ↦
    (fourier ((n + -m) i) : (a : AddCircle 1) → ℂ) x)
  0
Tactic: apply Finset.prod_eq_zero (Finset.mem_univ i)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ (↑((HilbertBasis.repr mFourierBasis : (a : ↥(Lp ℂ 2 volume)) → ↥(lp (fun (x : d → ℤ) ↦ ℂ) 2)) f) :
        (i : d → ℤ) → (fun (x : d → ℤ) ↦ ℂ) i)
      i =
    mFourierCoeff (↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i
have trans : Eq (α := (fun (x : d → ℤ) ↦ ℂ) i)
  ((↑((HilbertBasis.repr mFourierBasis : (a : ↥(Lp ℂ 2 volume)) → ↥(lp (fun (x : d → ℤ) ↦ ℂ) 2)) f) :
      (i : d → ℤ) → (fun (x : d → ℤ) ↦ ℂ) i)
    i)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
    HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t))
Tactic: trans ∫ t, conj (mFourierLp 2 i t) * f t
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
trans :
  Eq (α := (fun (x : d → ℤ) ↦ ℂ) i)
    ((↑((HilbertBasis.repr mFourierBasis : (a : ↥(Lp ℂ 2 volume)) → ↥(lp (fun (x : d → ℤ) ↦ ℂ) 2)) f) :
        (i : d → ℤ) → (fun (x : d → ℤ) ↦ ℂ) i)
      i)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) :
          ℂ)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t))
⊢ (↑((HilbertBasis.repr mFourierBasis : (a : ↥(Lp ℂ 2 volume)) → ↥(lp (fun (x : d → ℤ) ↦ ℂ) 2)) f) :
        (i : d → ℤ) → (fun (x : d → ℤ) ↦ ℂ) i)
      i =
    mFourierCoeff (↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i
have trans₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
    HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t)) =
  mFourierCoeff (↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i
Tactic: trans ∫ t, conj (mFourierLp 2 i t) * f t
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ Eq (α := (fun (x : d → ℤ) ↦ ℂ) i)
    ((↑((HilbertBasis.repr mFourierBasis : (a : ↥(Lp ℂ 2 volume)) → ↥(lp (fun (x : d → ℤ) ↦ ℂ) 2)) f) :
        (i : d → ℤ) → (fun (x : d → ℤ) ↦ ℂ) i)
      i)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) :
          ℂ)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t))
have rw : Eq (α := (fun (x : d → ℤ) ↦ ℂ) i)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : UnitAddTorus d) ↦
    inner ℂ ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
    HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t))
Tactic: rw [mFourierBasis.repr_apply_apply f i, MeasureTheory.L2.inner_def, coe_mFourierBasis]