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 ν
⊢ Integrable (ε := ℝ) (fun (p : W × V) ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ)

Tactic:
have : Integrable (fun (p : W × V) ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ) :=
    (hg.norm.mul_prod hf.norm).const_mul _
-- 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 μ)
hf₁ :
  AEStronglyMeasurable (β := G)
    (Function.uncurry fun (ξ : W) (x : V) ↦
      (((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)))
    (ν.prod μ)
hf₂ :
  ∀ᵐ (a : W × V) ∂ν.prod μ,
    norm.{u_6} (E := G)
        (Function.uncurry
          (fun (ξ : W) (x : V) ↦
            (((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)))
          a) ≤
      ‖‖M‖ * (‖g a.1‖ * ‖f a.2‖)‖
⊢ Integrable (ε := G)
    (Function.uncurry fun (ξ : W) (x : V) ↦
      (((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)))
    (ν.prod μ)

Tactic:
apply this.mono

Premises used: MeasureTheory.Integrable.mono
-- 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 μ)
hf₁ :
  AEStronglyMeasurable (β := G)
    (fun (p : W × V) ↦
      (((M : (a : F) → E →SL[σ] G) (g p.1) : E →SL[σ] G) : (a : E) → G)
        (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) p.2 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.1) : 𝕊)
          (f p.2)))
    (ν.prod μ)
⊢ AEStronglyMeasurable (β := G)
    (Function.uncurry fun (ξ : W) (x : V) ↦
      (((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)))
    (ν.prod μ)

Tactic:
change AEStronglyMeasurable (fun p : W × V ↦ (M (g p.1) (e (-(L p.2) p.1) • f p.2))) _

Premises used: Prod.fst, HSMul.hSMul, Prod.snd, DFunLike.coe, Neg.neg, MeasureTheory.AEStronglyMeasurable
-- 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 μ)
⊢ AEStronglyMeasurable (β := E)
    (fun (p : W × V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) p.2 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.1) : 𝕊)
        (f p.2))
    (ν.prod μ)

Tactic:
(Continuous.aestronglyMeasurable ?_).smul hf.1.comp_snd

Premises used: And.left, Continuous.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.smul, MeasureTheory.AEStronglyMeasurable.comp_snd
-- 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 μ)
refine :
  Continuous[instTopologicalSpaceProd, _] fun (p : W × V) ↦
    (e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) p.2 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.1)
⊢ AEStronglyMeasurable (β := E)
    (fun (p : W × V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) p.2 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.1) : 𝕊)
        (f p.2))
    (ν.prod μ)

Tactic:
refine (Continuous.aestronglyMeasurable ?_).smul hf.1.comp_snd

Premises used: And.left, Continuous.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.smul, MeasureTheory.AEStronglyMeasurable.comp_snd
-- 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 μ)
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : W × V) ↦
    (e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) p.2 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.1)

Tactic:
he.comp (hL.comp continuous_swap).neg

Premises used: Continuous.neg, 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 : 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 μ)
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : W × V) ↦
    (e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) p.2 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.1)

Tactic:
exact he.comp (hL.comp continuous_swap).neg

Premises used: Continuous.neg, 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 : 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 μ)
⊢ AEStronglyMeasurable (β := E)
    (fun (p : W × V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) p.2 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.1) : 𝕊)
        (f p.2))
    (ν.prod μ)

Tactic:
have A : AEStronglyMeasurable (fun (p : W × V) ↦ e (-L p.2 p.1) • f p.2) (ν.prod μ) := by
      refine (Continuous.aestronglyMeasurable ?_).smul hf.1.comp_snd
      exact he.comp (hL.comp continuous_swap).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 μ)
A :
  AEStronglyMeasurable (β := E)
    (fun (p : W × V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) p.2 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.1) : 𝕊)
        (f p.2))
    (ν.prod μ)
⊢ AEStronglyMeasurable (β := F × E)
    (fun (p : W × V) ↦
      (g p.1,
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) p.2 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.1) : 𝕊)
          (f p.2)))
    (ν.prod μ)

Tactic:
have A' : AEStronglyMeasurable (fun p ↦ (g p.1, e (-(L p.2) p.1) • f p.2) : W × V → F × E)
      (Measure.prod ν μ) := hg.1.comp_fst.prodMk A
-- 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 μ)
A :
  AEStronglyMeasurable (β := E)
    (fun (p : W × V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) p.2 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.1) : 𝕊)
        (f p.2))
    (ν.prod μ)
A' :
  AEStronglyMeasurable (β := F × E)
    (fun (p : W × V) ↦
      (g p.1,
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) p.2 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.1) : 𝕊)
          (f p.2)))
    (ν.prod μ)
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (q : F × E) ↦
    (((M : (a : F) → E →SL[σ] G) q.1 : E →SL[σ] G) : (a : E) → G) q.2

Tactic:
have hM : Continuous (fun q ↦ M q.1 q.2 : F × E → G) :=
      -- There is no `Continuous.clm_apply` for semilinear continuous maps
      (M.flip.cont.comp continuous_snd).clm_apply continuous_fst
-- 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 μ)
A :
  AEStronglyMeasurable (β := E)
    (fun (p : W × V) ↦
      HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) p.2 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.1) : 𝕊)
        (f p.2))
    (ν.prod μ)
A' :
  AEStronglyMeasurable (β := F × E)
    (fun (p : W × V) ↦
      (g p.1,
        HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) p.2 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.1) : 𝕊)
          (f p.2)))
    (ν.prod μ)
hM :
  Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (q : F × E) ↦
    (((M : (a : F) → E →SL[σ] G) q.1 : E →SL[σ] G) : (a : E) → G) q.2
⊢ AEStronglyMeasurable (β := G)
    (fun (p : W × V) ↦
      (((M : (a : F) → E →SL[σ] G) (g p.1) : E →SL[σ] G) : (a : E) → G)
        (HSMul.hSMul (α := 𝕊) ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) p.2 : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) p.1) : 𝕊)
          (f p.2)))
    (ν.prod μ)

Tactic:
apply hM.comp_aestronglyMeasurable A'

Premises used: Continuous.comp_aestronglyMeasurable
-- 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 μ)
hf₁ :
  ∀ (ξ : W) (x : V),
    norm.{u_6} (E := G)
        (Function.uncurry
          (fun (ξ : W) (x : V) ↦
            (((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)))
          (ξ, x)) ≤
      ‖‖M‖ * (‖g (ξ, x).1‖ * ‖f (ξ, x).2‖)‖
⊢ ∀ᵐ (a : W × V) ∂ν.prod μ,
    norm.{u_6} (E := G)
        (Function.uncurry
          (fun (ξ : W) (x : V) ↦
            (((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)))
          a) ≤
      ‖‖M‖ * (‖g a.1‖ * ‖f a.2‖)‖

Tactic:
filter_upwards 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 : 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
hf₁ :
  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‖
⊢ norm.{u_6} (E := G)
      (Function.uncurry
        (fun (ξ : W) (x : V) ↦
          (((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)))
        (ξ, x)) ≤
    ‖‖M‖ * (‖g (ξ, x).1‖ * ‖f (ξ, x).2‖)‖

Tactic:
simp only [Function.uncurry_apply_pair, norm_mul, norm_norm, ge_iff_le, ← mul_assoc]

Premises used: ge_iff_le, mul_assoc, norm_mul, norm_norm, Function.uncurry_apply_pair