awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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
apply :
  Continuous[instTopologicalSpaceProd, inst_12] fun (p : W × V) ↦
    (((L.flip : (a : W) → V →ₗ[𝕜] 𝕜) p.1 : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) p.2
⊢ 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 (fourierIntegral_convergent_iff he _ _).2 hg

Premises used: Iff.mpr, VectorFourier.fourierIntegral_convergent_iff
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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
⊢ Continuous[instTopologicalSpaceProd, inst_12] fun (p : W × V) ↦
    (((L.flip : (a : W) → V →ₗ[𝕜] 𝕜) p.1 : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) p.2

Tactic:
hL.comp continuous_swap

Premises used: Continuous.comp, continuous_swap
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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
⊢ Continuous[instTopologicalSpaceProd, inst_12] fun (p : W × V) ↦
    (((L.flip : (a : W) → V →ₗ[𝕜] 𝕜) p.1 : V →ₗ[𝕜] 𝕜) : (a : V) → 𝕜) p.2

Tactic:
exact hL.comp continuous_swap

Premises used: Continuous.comp, continuous_swap
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℂ F
inst_8 : TopologicalSpace 𝕜
inst_9 : IsTopologicalRing 𝕜
inst_10 : TopologicalSpace V
inst_11 : BorelSpace V
inst_12 : TopologicalSpace W
inst_13 : MeasurableSpace W
inst_14 : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst_15 : SigmaFinite μ
inst_16 : SigmaFinite ν
inst_17 : SecondCountableTopology V
inst_18 : CompleteSpace F
f : V → ℂ
g : W → F
he : Continuous[inst_8, _] (⇑e : (a : 𝕜) → 𝕊)
hL :
  Continuous[instTopologicalSpaceProd, inst_8] fun (p : V × W) ↦
    (((L : (a : V) → W →ₗ[𝕜] 𝕜) p.1 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.2
hf : Integrable f μ
hg : Integrable g ν
⊢ Eq.{u_5 + 1} (α := F) (∫ (ξ : W), fourierIntegral e μ L f ξ • g ξ ∂ν)
    (∫ (x : V), f x • fourierIntegral e ν L.flip g x ∂μ)

Tactic:
integral_bilin_fourierIntegral_eq_flip (ContinuousLinearMap.lsmul ℂ ℂ) he hL hf hg

Premises used: VectorFourier.integral_bilin_fourierIntegral_eq_flip, Complex, ContinuousLinearMap.lsmul
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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) ∂μ)
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) ∂μ)
⊢ 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

Premises used: CompleteSpace
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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) ∂μ)

Tactic:
simp [integral, hG]

Premises used: MeasureTheory.integral
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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
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)
⊢ 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:
congr with ξ
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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
apply :
  Integrable.{u_4, u_2} (ε := E)
    (fun (x : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊) (f x))
    μ
⊢ 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:
apply (ContinuousLinearMap.integral_comp_commSL RCLike.conj_smul _ _).symm

Premises used: ContinuousLinearMap.integral_comp_commSL, Eq.symm, RCLike.conj_smul
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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
⊢ Integrable.{u_4, u_2} (ε := E)
    (fun (x : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊) (f x))
    μ

Tactic:
(fourierIntegral_convergent_iff he hL _).2 hf

Premises used: Iff.mpr, VectorFourier.fourierIntegral_convergent_iff
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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
⊢ Integrable.{u_4, u_2} (ε := E)
    (fun (x : V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊) (f x))
    μ

Tactic:
exact (fourierIntegral_convergent_iff he hL _).2 hf

Premises used: Iff.mpr, VectorFourier.fourierIntegral_convergent_iff
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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),
      ∫ (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)) ∂μ ∂ν)
    (∫ (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)) ∂ν ∂μ)

Tactic:
integral_fourierIntegral_swap M.flip he hL hf hg

Premises used: VectorFourier.integral_fourierIntegral_swap, ContinuousLinearMap.flip
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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
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 ξ)) ∂ν)
⊢ 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 ξ)) ∂ν ∂μ)

Tactic:
congr with x
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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
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)
⊢ 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 ξ
-- Module: Mathlib.Analysis.Fourier.FourierTransform
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
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)
⊢ 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:
rw [← smul_one_smul ℂ _ (f x), ← smul_one_smul ℂ _ (g ξ)]

Premises used: smul_one_smul, Complex