-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
lemma _root_.MeasureTheory.AEStronglyMeasurable.fourierSMulRight
    [SecondCountableTopologyEither V (W →L[ℝ] ℝ)] [MeasurableSpace V] [BorelSpace V]
    {L : V →L[ℝ] W →L[ℝ] ℝ} {f : V → E} {μ : Measure V}
    (hf : AEStronglyMeasurable f μ) :
    AEStronglyMeasurable (fun v ↦ fourierSMulRight L f v) μ

Proof state:
case hf
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : SecondCountableTopologyEither V (W →L[ℝ] ℝ)
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
μ : Measure V
hf : AEStronglyMeasurable f μ
aux0 : Continuous fun p => p.1.smulRight p.2
aux1 : AEStronglyMeasurable (fun v => (L v, f v)) μ
⊢ AEStronglyMeasurable (fun x => (L x).smulRight (f x)) μ

Tactic:
exact (aux0.comp_aestronglyMeasurable aux1 :)

Result:
no goals

Proof state:
case hf
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : SecondCountableTopologyEither V (W →L[ℝ] ℝ)
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
μ : Measure V
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x => (L x).smulRight (f x)) μ

Tactic:
have aux0 : Continuous fun p : (W →L[ℝ] ℝ) × E ↦ p.1.smulRight p.2 :=
  (ContinuousLinearMap.smulRightL ℝ W E).continuous₂

Result:
case hf
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : SecondCountableTopologyEither V (W →L[ℝ] ℝ)
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
μ : Measure V
hf : AEStronglyMeasurable f μ
aux0 : Continuous fun p => p.1.smulRight p.2
⊢ AEStronglyMeasurable (fun x => (L x).smulRight (f x)) μ

Proof state:
case hf
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : SecondCountableTopologyEither V (W →L[ℝ] ℝ)
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
μ : Measure V
hf : AEStronglyMeasurable f μ
aux0 : Continuous fun p => p.1.smulRight p.2
⊢ AEStronglyMeasurable (fun x => (L x).smulRight (f x)) μ

Tactic:
have aux1 : AEStronglyMeasurable (fun v ↦ (L v, f v)) μ :=
  L.continuous.aestronglyMeasurable.prod_mk hf

Result:
case hf
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : SecondCountableTopologyEither V (W →L[ℝ] ℝ)
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
μ : Measure V
hf : AEStronglyMeasurable f μ
aux0 : Continuous fun p => p.1.smulRight p.2
aux1 : AEStronglyMeasurable (fun v => (L v, f v)) μ
⊢ AEStronglyMeasurable (fun x => (L x).smulRight (f x)) μ

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : SecondCountableTopologyEither V (W →L[ℝ] ℝ)
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
μ : Measure V
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun v => VectorFourier.fourierSMulRight L f v) μ

Tactic:
apply AEStronglyMeasurable.const_smul'

Result:
case hf
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
inst✝² : SecondCountableTopologyEither V (W →L[ℝ] ℝ)
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
μ : Measure V
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x => (L x).smulRight (f x)) μ