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 : RingHomIsometric σ
f : V → E
g : W → F
M : F →L[ℂ] E →SL[σ] 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 ν
this : Integrable (ε := ℝ) (fun (p : W × V) ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ)
ξ : W
x : V
⊢ norm.{u_6} (E := G)
      ((((M : (a : F) → E →SL[σ] G) (g ξ) : E →SL[σ] G) : (a : E) → G)
          (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊)
            (f x)) :
        G) ≤
    ‖M‖ * ‖g ξ‖ *
      ‖HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊)
          (f x)‖

Tactic:
M.le_opNorm₂ (g ξ) (e (-L x ξ) • f x)

Premises used: ContinuousLinearMap.le_opNorm₂, HSMul.hSMul, DFunLike.coe, Neg.neg
-- 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 : RingHomIsometric σ
f : V → E
g : W → F
M : F →L[ℂ] E →SL[σ] 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 ν
this : Integrable (ε := ℝ) (fun (p : W × V) ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ)
ξ : W
x : V
h : ‖‖M‖‖ * ‖g ξ‖ = ‖M‖ * ‖g ξ‖
h₁ :
  ‖f x‖ =
    ‖HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊) (f x)‖
⊢ norm.{u_6} (E := G)
      ((((M : (a : F) → E →SL[σ] G) (g ξ) : E →SL[σ] G) : (a : E) → G)
          (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) x : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) ξ) : 𝕊)
            (f x)) :
        G) ≤
    ‖‖M‖‖ * ‖g ξ‖ * ‖f x‖

Tactic:
convert! M.le_opNorm₂ (g ξ) (e (-L x ξ) • f x) using 2

Premises used: ContinuousLinearMap.le_opNorm₂, HSMul.hSMul, DFunLike.coe, Neg.neg
-- 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 : RingHomIsometric σ
f : V → E
g : W → F
M : F →L[ℂ] E →SL[σ] 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 ν
this : Integrable (ε := ℝ) (fun (p : W × V) ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ)
ξ : W
x : V
h : 0 ≤ ‖M‖ ∨ g ξ = 0
⊢ ‖‖M‖‖ * ‖g ξ‖ = ‖M‖ * ‖g ξ‖

Tactic:
simp
-- 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_comm _ _).symm

Premises used: Eq.symm, ContinuousLinearMap.integral_comp_comm
-- 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
⊢ 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:
simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.map_smul_of_tower,
      ContinuousLinearMap.coe_smul', Pi.smul_apply, LinearMap.flip_apply]

Premises used: ContinuousLinearMap.coe_smul', ContinuousLinearMap.map_smul_of_tower, ContinuousLinearMap.flip_apply, LinearMap.flip_apply, Pi.smul_apply
-- 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 : (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)
⊢ 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 ξ) ∂ν) ∂μ)

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 :
  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))
    ν
⊢ 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:
apply ContinuousLinearMap.integral_comp_comm

Premises used: ContinuousLinearMap.integral_comp_comm