-- Mathlib/Analysis/Fourier/FourierTransform.lean
theorem integral_bilin_fourierIntegral_eq_flip
    {f : V → E} {g : W → F} (M : E →L[ℂ] F →L[ℂ] G) (he : Continuous e)
    (hL : Continuous fun p : V × W ↦ L p.1 p.2) (hf : Integrable f μ) (hg : Integrable g ν) :
    ∫ ξ, M (fourierIntegral e μ L f ξ) (g ξ) ∂ν =
      ∫ x, M (f x) (fourierIntegral e ν L.flip g x) ∂μ

Proof state:
case hf
𝕜 : Type u_1
inst✝²³ : CommRing 𝕜
V : Type u_2
inst✝²² : AddCommGroup V
inst✝²¹ : Module 𝕜 V
inst✝²⁰ : MeasurableSpace V
W : Type u_3
inst✝¹⁹ : AddCommGroup W
inst✝¹⁸ : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℂ E
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace ℂ F
inst✝¹³ : NormedAddCommGroup G
inst✝¹² : NormedSpace ℂ G
inst✝¹¹ : TopologicalSpace 𝕜
inst✝¹⁰ : IsTopologicalRing 𝕜
inst✝⁹ : TopologicalSpace V
inst✝⁸ : BorelSpace V
inst✝⁷ : TopologicalSpace W
inst✝⁶ : MeasurableSpace W
inst✝⁵ : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst✝⁴ : SigmaFinite μ
inst✝³ : SigmaFinite ν
inst✝² : SecondCountableTopology V
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : V → E
g : W → F
M : E →L[ℂ] F →L[ℂ] G
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
⊢ Integrable (Function.uncurry fun ξ x => (M.flip (g ξ)) (e (-(L x) ξ) • f x)) (ν.prod μ)

Tactic:
have : Integrable (fun (p : W × V) ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ) :=
  (hg.norm.prod_mul hf.norm).const_mul _

Result:
case hf
𝕜 : Type u_1
inst✝²³ : CommRing 𝕜
V : Type u_2
inst✝²² : AddCommGroup V
inst✝²¹ : Module 𝕜 V
inst✝²⁰ : MeasurableSpace V
W : Type u_3
inst✝¹⁹ : AddCommGroup W
inst✝¹⁸ : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℂ E
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace ℂ F
inst✝¹³ : NormedAddCommGroup G
inst✝¹² : NormedSpace ℂ G
inst✝¹¹ : TopologicalSpace 𝕜
inst✝¹⁰ : IsTopologicalRing 𝕜
inst✝⁹ : TopologicalSpace V
inst✝⁸ : BorelSpace V
inst✝⁷ : TopologicalSpace W
inst✝⁶ : MeasurableSpace W
inst✝⁵ : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst✝⁴ : SigmaFinite μ
inst✝³ : SigmaFinite ν
inst✝² : SecondCountableTopology V
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : V → E
g : W → F
M : E →L[ℂ] F →L[ℂ] G
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
this : Integrable (fun p => ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ)
⊢ Integrable (Function.uncurry fun ξ x => (M.flip (g ξ)) (e (-(L x) ξ) • f x)) (ν.prod μ)

Proof state:
𝕜 : Type u_1
inst✝²³ : CommRing 𝕜
V : Type u_2
inst✝²² : AddCommGroup V
inst✝²¹ : Module 𝕜 V
inst✝²⁰ : MeasurableSpace V
W : Type u_3
inst✝¹⁹ : AddCommGroup W
inst✝¹⁸ : Module 𝕜 W
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℂ E
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace ℂ F
inst✝¹³ : NormedAddCommGroup G
inst✝¹² : NormedSpace ℂ G
inst✝¹¹ : TopologicalSpace 𝕜
inst✝¹⁰ : IsTopologicalRing 𝕜
inst✝⁹ : TopologicalSpace V
inst✝⁸ : BorelSpace V
inst✝⁷ : TopologicalSpace W
inst✝⁶ : MeasurableSpace W
inst✝⁵ : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst✝⁴ : SigmaFinite μ
inst✝³ : SigmaFinite ν
inst✝² : SecondCountableTopology V
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : V → E
g : W → F
M : E →L[ℂ] F →L[ℂ] G
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
⊢ ∫ (x : V), ∫ (ξ : W), (M.flip (g ξ)) (e (-(L x) ξ) • f x) ∂ν ∂μ =
    ∫ (x : V), ∫ (ξ : W), (M (f x)) (e (-(L.flip ξ) x) • g ξ) ∂ν ∂μ

Tactic:
simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.map_smul_of_tower,
ContinuousLinearMap.coe_smul', Pi.smul_apply, LinearMap.flip_apply]

Result:
no goals