awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℂ F
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℂ G
inst_12 : TopologicalSpace 𝕜
inst_13 : IsTopologicalRing 𝕜
inst_14 : TopologicalSpace V
inst_15 : BorelSpace V
inst_16 : TopologicalSpace W
inst_17 : MeasurableSpace W
inst_18 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_19 : SigmaFinite μ
inst_20 : SigmaFinite ν
inst_21 : SecondCountableTopology V
inst_22 : CompleteSpace E
inst_23 : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst_12, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
⊢ Eq.{u_6 + 1} (α := G)
    (∫ (x : V),
      ∫ (ξ : W),
        (((M.flip : (a : F) → E →L⋆[ℂ] G) (g ξ) : E →L⋆[ℂ] G) : (a : E) → G)
          (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊)
            (f x)) ∂ν ∂μ)
    (∫ (x : V),
      ∫ (ξ : W),
        (((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
          (HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊) ((((L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g ξ)) ∂ν ∂μ)
have e_f : ∀ (x : V),
  Eq.{u_6 + 1} (α := G)
    (∫ (ξ : W),
      (((M.flip : (a : F) → E →L⋆[ℂ] G) (g ξ) : E →L⋆[ℂ] G) : (a : E) → G)
        (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊)
          (f x)) ∂ν)
    (∫ (ξ : W),
      (((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
        (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) ((((L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊)
          (g ξ)) ∂ν)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℂ F
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℂ G
inst_12 : TopologicalSpace 𝕜
inst_13 : IsTopologicalRing 𝕜
inst_14 : TopologicalSpace V
inst_15 : BorelSpace V
inst_16 : TopologicalSpace W
inst_17 : MeasurableSpace W
inst_18 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_19 : SigmaFinite μ
inst_20 : SigmaFinite ν
inst_21 : SecondCountableTopology V
inst_22 : CompleteSpace E
inst_23 : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst_12, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
x : V
⊢ Eq.{u_6 + 1} (α := G)
    (∫ (ξ : W),
      (((M.flip : (a : F) → E →L⋆[ℂ] G) (g ξ) : E →L⋆[ℂ] G) : (a : E) → G)
        (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊)
          (f x)) ∂ν)
    (∫ (ξ : W),
      (((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
        (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) ((((L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊)
          (g ξ)) ∂ν)
have e_f : ∀ (ξ : W),
  Eq.{u_6 + 1} (α := G)
    ((((M.flip : (a : F) → E →L⋆[ℂ] G) (g ξ) : E →L⋆[ℂ] G) : (a : E) → G)
        (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊)
          (f x)) :
      G)
    ((((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
        (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) ((((L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊)
          (g ξ)) :
      G)
Tactic: congr with ξ
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℂ F
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℂ G
inst_12 : TopologicalSpace 𝕜
inst_13 : IsTopologicalRing 𝕜
inst_14 : TopologicalSpace V
inst_15 : BorelSpace V
inst_16 : TopologicalSpace W
inst_17 : MeasurableSpace W
inst_18 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_19 : SigmaFinite μ
inst_20 : SigmaFinite ν
inst_21 : SecondCountableTopology V
inst_22 : CompleteSpace E
inst_23 : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst_12, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
x : V
ξ : W
⊢ Eq.{u_6 + 1} (α := G)
    ((((M.flip : (a : F) → E →L⋆[ℂ] G) (g ξ) : E →L⋆[ℂ] G) : (a : E) → G)
        (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊)
          (f x)) :
      G)
    ((((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
        (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) ((((L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊)
          (g ξ)) :
      G)
have e_f : Eq.{u_6 + 1} (α := G)
  ((((M.flip : (a : F) → E →L⋆[ℂ] G) (g ξ) : E →L⋆[ℂ] G) : (a : E) → G)
      (HSMul.hSMul (α := 𝕊) (β := ℂ)
          ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊) 1 •
        f x) :
    G)
  ((((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
      (HSMul.hSMul (α := 𝕊) (β := ℂ)
          ((e : (a : 𝕜) → 𝕊) ((((L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) 1 •
        g ξ) :
    G)
Tactic: rw [← smul_one_smul ℂ _ (f x), ← smul_one_smul ℂ _ (g ξ)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℂ F
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℂ G
inst_12 : TopologicalSpace 𝕜
inst_13 : IsTopologicalRing 𝕜
inst_14 : TopologicalSpace V
inst_15 : BorelSpace V
inst_16 : TopologicalSpace W
inst_17 : MeasurableSpace W
inst_18 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_19 : SigmaFinite μ
inst_20 : SigmaFinite ν
inst_21 : SecondCountableTopology V
inst_22 : CompleteSpace E
inst_23 : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst_12, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
⊢ Eq.{u_6 + 1} (α := G)
    (∫ (x : V),
      ∫ (ξ : W),
        (((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
          (HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g ξ)) ∂ν ∂μ)
    (∫ (x : V),
      (((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
        (∫ (ξ : W),
          HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g ξ) ∂ν) ∂μ)
have e_f : ∀ (x : V),
  Eq.{u_6 + 1} (α := G)
    (∫ (ξ : W),
        (((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
          (HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g ξ)) ∂ν :
      G)
    ((((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
        (∫ (ξ : W),
          HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g ξ) ∂ν) :
      G)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℂ F
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℂ G
inst_12 : TopologicalSpace 𝕜
inst_13 : IsTopologicalRing 𝕜
inst_14 : TopologicalSpace V
inst_15 : BorelSpace V
inst_16 : TopologicalSpace W
inst_17 : MeasurableSpace W
inst_18 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_19 : SigmaFinite μ
inst_20 : SigmaFinite ν
inst_21 : SecondCountableTopology V
inst_22 : CompleteSpace E
inst_23 : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst_12, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
x : V
⊢ Eq.{u_6 + 1} (α := G)
    (∫ (ξ : W),
        (((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
          (HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g ξ)) ∂ν :
      G)
    ((((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G)
        (∫ (ξ : W),
          HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) ξ : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g ξ) ∂ν) :
      G)
have e_f : Integrable.{u_5, u_3} (ε := F)
  (fun (x_1 : W) ↦
    HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) x_1 : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊)
      (g x_1))
  ν
Tactic: apply ContinuousLinearMap.integral_comp_comm
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (hypothesis)
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℂ F
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℂ G
inst_12 : TopologicalSpace 𝕜
inst_13 : IsTopologicalRing 𝕜
inst_14 : TopologicalSpace V
inst_15 : BorelSpace V
inst_16 : TopologicalSpace W
inst_17 : MeasurableSpace W
inst_18 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_19 : SigmaFinite μ
inst_20 : SigmaFinite ν
inst_21 : SecondCountableTopology V
inst_22 : CompleteSpace E
inst_23 : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst_12, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
x : V
⊢ Integrable.{u_5, u_3} (ε := F)
    (fun (x_1 : W) ↦
      HSMul.hSMul (α := 𝕊)
        ((e : (a : 𝕜) → 𝕊) (-((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) x_1 : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) x) : 𝕊) (g x_1))
    ν
have hLflip : Continuous[instTopologicalSpaceProd, inst_12] fun (p : W × V) ↦
  ((-(L.flip : (a : W) → V →ₗ[𝕜] 𝕜) p.1 : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) p.2
Tactic: have hLflip : Continuous fun (p : W × V) => (-L.flip p.1) p.2 :=
      (continuous_neg.comp hL).comp continuous_swap
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℂ F
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℂ G
inst_12 : TopologicalSpace 𝕜
inst_13 : IsTopologicalRing 𝕜
inst_14 : TopologicalSpace V
inst_15 : BorelSpace V
inst_16 : TopologicalSpace W
inst_17 : MeasurableSpace W
inst_18 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_19 : SigmaFinite μ
inst_20 : SigmaFinite ν
inst_21 : SecondCountableTopology V
inst_22 : CompleteSpace E
inst_23 : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst_12, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
⊢ Eq.{u_6 + 1} (α := G)
    (∫ (ξ : W), (((M : (a : E) → F →L[ℂ] G) (fourierIntegral e μ L f ξ) : F →L[ℂ] G) : (a : F) → G) (g ξ) ∂ν)
    (∫ (x : V), (((M : (a : E) → F →L[ℂ] G) (f x) : F →L[ℂ] G) : (a : F) → G) (fourierIntegral e ν (-L.flip) g x) ∂μ)
have e₁ : Eq.{u_6 + 1} (α := G)
  (∫ (ξ : W),
    (((M.flip : (a : F) → E →L⋆[ℂ] G) (g ξ) : E →L⋆[ℂ] G) : (a : E) → G)
      (∫ (x : V),
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊)
          (f x) ∂μ) ∂ν)
  (∫ (ξ : W),
    ∫ (x : V),
      (((M.flip : (a : F) → E →L⋆[ℂ] G) (g ξ) : E →L⋆[ℂ] G) : (a : E) → G)
        (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊)
          (f x)) ∂μ ∂ν)
Tactic: calc
  ∫ ξ, M.flip (g ξ) (∫ x, e (-L x ξ) • f x ∂μ) ∂ν
    = ∫ ξ, (∫ x, M.flip (g ξ) (e (-L x ξ) • f x) ∂μ) ∂ν := by
    congr with ξ
    apply (ContinuousLinearMap.integral_comp_commSL RCLike.conj_smul _ _).symm
    exact (fourierIntegral_convergent_iff he hL _).2 hf
  _ = ∫ x, (∫ ξ, M.flip (g ξ) (e (-L x ξ) • f x) ∂ν) ∂μ :=
    integral_fourierIntegral_swap M.flip he hL hf hg
  _ = ∫ x, (∫ ξ, M (f x) (e (L.flip ξ x) • g ξ) ∂ν) ∂μ := by
    congr with x
    congr with ξ
    rw [← smul_one_smul ℂ _ (f x), ← smul_one_smul ℂ _ (g ξ)]
    simp only [map_smulₛₗ, ContinuousLinearMap.flip_apply, LinearMap.flip_apply, RingHom.id_apply,
      Circle.smul_def, smul_eq_mul, mul_one, ← Circle.coe_inv_eq_conj, AddChar.map_neg_eq_inv,
      inv_inv]
  _ = ∫ x, (∫ ξ, M (f x) (e (-(-L.flip ξ) x) • g ξ) ∂ν) ∂μ := by
    simp only [LinearMap.flip_apply, ContinuousLinearMap.map_smul_of_tower, LinearMap.neg_apply,
      neg_neg]
  _ = ∫ x, M (f x) (∫ ξ, e (-(-L.flip ξ) x) • g ξ ∂ν) ∂μ := by
    congr with x
    apply ContinuousLinearMap.integral_comp_comm
    have hLflip : Continuous fun (p : W × V) => (-L.flip p.1) p.2 :=
      (continuous_neg.comp hL).comp continuous_swap
    exact (fourierIntegral_convergent_iff (L := -L.flip) he hLflip x).2 hg
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_7
W : Type u_8
x : MeasurableSpace V
inst_2 : AddCommGroup V
inst_3 : Module ℝ V
inst_4 : AddCommGroup W
inst_5 : Module ℝ W
L : LinearMap.{0, 0, u_7, u_8} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
μ : Measure V
f : V → E
w : W
⊢ fourierIntegral Real.probChar μ L f w =
    ∫ (v : V), Complex.exp (-(↑((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * Complex.I) • f v ∂μ
have simp_rw : Eq.{u_4 + 1} (α := E)
  (∫ (v : V),
    HSMul.hSMul (α := 𝕊)
      ((Real.probChar : (a : ℝ) → 𝕊) (-(((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : 𝕊) (f v) ∂μ)
  (∫ (v : V), Complex.exp (-(↑((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * Complex.I) • f v ∂μ)
Tactic: simp_rw [fourierIntegral, Circle.smul_def, Real.probChar_apply, Complex.ofReal_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_7
W : Type u_8
x : MeasurableSpace V
inst_2 : AddCommGroup V
inst_3 : Module ℝ V
inst_4 : AddCommGroup W
inst_5 : Module ℝ W
L : LinearMap.{0, 0, u_7, u_8} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
μ : Measure V
f : V → E
w : W
simp_rw :
  Eq.{u_4 + 1} (α := E)
    (∫ (v : V),
      HSMul.hSMul (α := 𝕊)
        ((Real.probChar : (a : ℝ) → 𝕊) (-(((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : 𝕊) (f v) ∂μ)
    (∫ (v : V),
      Complex.exp (-(↑((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * Complex.I) • f v ∂μ)
⊢ fourierIntegral Real.probChar μ L f w =
    ∫ (v : V), Complex.exp (-(↑((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * Complex.I) • f v ∂μ
have simp_rw₁ : Eq.{u_4 + 1} (α := E)
  (∫ (v : V),
    HSMul.hSMul (α := ℂ)
      (↑((Real.probChar : (a : ℝ) → 𝕊) (-(((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) (f v) ∂μ)
  (∫ (v : V), Complex.exp (-(↑((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * Complex.I) • f v ∂μ)
Tactic: simp_rw [fourierIntegral, Circle.smul_def, Real.probChar_apply, Complex.ofReal_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_7
W : Type u_8
x : MeasurableSpace V
inst_2 : AddCommGroup V
inst_3 : Module ℝ V
inst_4 : AddCommGroup W
inst_5 : Module ℝ W
L : LinearMap.{0, 0, u_7, u_8} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
μ : Measure V
f : V → E
w : W
simp_rw :
  Eq.{u_4 + 1} (α := E)
    (∫ (v : V),
      HSMul.hSMul (α := 𝕊)
        ((Real.probChar : (a : ℝ) → 𝕊) (-(((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : 𝕊) (f v) ∂μ)
    (∫ (v : V),
      Complex.exp (-(↑((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * Complex.I) • f v ∂μ)
simp_rw₁ :
  Eq.{u_4 + 1} (α := E)
    (∫ (v : V),
      HSMul.hSMul (α := ℂ)
        (↑((Real.probChar : (a : ℝ) → 𝕊) (-(((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) (f v) ∂μ)
    (∫ (v : V),
      Complex.exp (-(↑((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * Complex.I) • f v ∂μ)
⊢ fourierIntegral Real.probChar μ L f w =
    ∫ (v : V), Complex.exp (-(↑((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * Complex.I) • f v ∂μ
have simp_rw₂ : Eq.{u_4 + 1} (α := E)
  (∫ (v : V), Complex.exp ((↑(-(((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * Complex.I) • f v ∂μ)
  (∫ (v : V), Complex.exp (-(↑((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) * Complex.I) • f v ∂μ)
Tactic: simp_rw [fourierIntegral, Circle.smul_def, Real.probChar_apply, Complex.ofReal_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
V : Type u_5
W : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : NormedAddCommGroup W
inst_6 : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedAddCommGroup E
inst_10 : NormedSpace ℂ E
f : V → F →L[ℝ] E
a : F
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : 𝕜) → 𝕊)
hf : Integrable f μ
⊢ Eq.{u_3 + 1} (α := E)
    ((fourierIntegral e μ
            (ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V)
              (F := W) (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L)
            f w :
          (a : F) → E)
        a :
      E)
    (fourierIntegral e μ
        (ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V) (F := W)
          (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L)
        (fun (x : V) ↦ (f x : (a : F) → E) a) w :
      E)
have rw : Eq.{u_3 + 1} (α := E)
  (∫ (x : V),
    (HSMul.hSMul (α := 𝕊)
          ((e : (a : 𝕜) → 𝕊)
              (-((((ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E :=
                              V) (F := W) (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L :
                            V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) :
                          (a : V) → W →ₗ[𝕜] 𝕜)
                        x :
                      W →ₗ[𝕜] 𝕜) :
                    (a : W) → 𝕜)
                  w) :
            𝕊)
          (f x) :
        (a : F) → E)
      a ∂μ)
  (fourierIntegral e μ
    (ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V) (F := W)
      (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L)
    (fun (x : V) ↦ (f x : (a : F) → E) a) w)
Tactic: rw [fourierIntegral, ContinuousLinearMap.integral_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
V : Type u_5
W : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : NormedSpace 𝕜 V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : NormedAddCommGroup W
inst_6 : NormedSpace 𝕜 W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →L[𝕜] W →L[𝕜] 𝕜
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedAddCommGroup E
inst_10 : NormedSpace ℂ E
f : V → F →L[ℝ] E
a : F
w : W
he : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : 𝕜) → 𝕊)
hf : Integrable f μ
rw :
  Eq.{u_3 + 1} (α := E)
    (∫ (x : V),
      (HSMul.hSMul (α := 𝕊)
            ((e : (a : 𝕜) → 𝕊)
                (-((((ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜)
                                (E := V) (F := W) (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L :
                              V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) :
                            (a : V) → W →ₗ[𝕜] 𝕜)
                          x :
                        W →ₗ[𝕜] 𝕜) :
                      (a : W) → 𝕜)
                    w) :
              𝕊)
            (f x) :
          (a : F) → E)
        a ∂μ)
    (fourierIntegral e μ
      (ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V) (F := W)
        (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L)
      (fun (x : V) ↦ (f x : (a : F) → E) a) w)
⊢ Eq.{u_3 + 1} (α := E)
    ((fourierIntegral e μ
            (ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V)
              (F := W) (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L)
            f w :
          (a : F) → E)
        a :
      E)
    (fourierIntegral e μ
        (ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V) (F := W)
          (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L)
        (fun (x : V) ↦ (f x : (a : F) → E) a) w :
      E)
have φ_int : Integrable (ε := F →L[ℝ] E)
  (fun (v : V) ↦
    HSMul.hSMul (α := 𝕊)
      ((e : (a : 𝕜) → 𝕊)
          (-((((ContinuousLinearMap.toLinearMap₁₂.{u_1, u_1, u_1, u_5, u_6, u_1} (R := 𝕜) (𝕜₂ := 𝕜) (𝕜₃ := 𝕜) (E := V)
                          (F := W) (G := 𝕜) (σ₁₃ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) L :
                        V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) :
                      (a : V) → W →ₗ[𝕜] 𝕜)
                    v :
                  W →ₗ[𝕜] 𝕜) :
                (a : W) → 𝕜)
              w) :
        𝕊)
      (f v))
  μ
Tactic: rw [fourierIntegral, ContinuousLinearMap.integral_apply]