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 ν
pos :
  ∀ (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) ∂μ)
⊢ 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 neg : ∀ (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) ∂μ)
Tactic: by_cases hG : CompleteSpace 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)
    (∫ (ξ : 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)) ∂μ ∂ν)
have e_f : ∀ (ξ : W),
  Eq.{u_6 + 1} (α := G)
    ((((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) ∂μ) :
      G)
    (∫ (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)) ∂μ :
      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
ξ : W
⊢ Eq.{u_6 + 1} (α := G)
    ((((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) ∂μ) :
      G)
    (∫ (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)) ∂μ :
      G)
have apply : Integrable.{u_4, u_2} (ε := E)
  (fun (x : V) ↦
    HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊) (f x))
  μ
Tactic: apply (ContinuousLinearMap.integral_comp_comm _ _).symm
-- 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 (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
⊢ 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 apply : Continuous[instTopologicalSpaceProd, inst_12] fun (p : W × V) ↦
  (((L.flip : (a : W) → V →ₗ[𝕜] 𝕜) p.1 : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) p.2
Tactic: apply (fourierIntegral_convergent_iff he _ _).2 hg
-- 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_comm _ _).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
    simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.map_smul_of_tower,
      ContinuousLinearMap.coe_smul', Pi.smul_apply, LinearMap.flip_apply]
  _ = ∫ x, M (f x) (∫ ξ, e (-L.flip ξ x) • g ξ ∂ν) ∂μ := by
    congr with x
    apply ContinuousLinearMap.integral_comp_comm
    apply (fourierIntegral_convergent_iff he _ _).2 hg
    exact 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 ν
⊢ 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 pos : ∀ (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) ∂μ)
Tactic: by_cases hG : CompleteSpace 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 ν
pos :
  ∀ (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) ∂μ)
⊢ 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 neg : ∀ (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) ∂μ)
Tactic: by_cases hG : CompleteSpace 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)
    (∫ (ξ : 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)) ∂μ ∂ν)
have e_f : ∀ (ξ : W),
  Eq.{u_6 + 1} (α := G)
    ((((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) ∂μ) :
      G)
    (∫ (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)) ∂μ :
      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
ξ : W
⊢ Eq.{u_6 + 1} (α := G)
    ((((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) ∂μ) :
      G)
    (∫ (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)) ∂μ :
      G)
have apply : Integrable.{u_4, u_2} (ε := E)
  (fun (x : V) ↦
    HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊) (f x))
  μ
Tactic: apply (ContinuousLinearMap.integral_comp_commSL RCLike.conj_smul _ _).symm