-- Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
theorem tendsto_integral_exp_smul_cocompact (μ : Measure V) [μ.IsAddHaarMeasure] :
    Tendsto (fun w : V →L[ℝ] ℝ => ∫ v, 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)

Proof state:
case h.e'_3.h.e_f.h.e_a.h.e_6.h.e_a
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this✝¹ : MeasurableSpace V' := borel V'
this✝ : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : (V →L[ℝ] ℝ) ≃L[ℝ] V' →L[ℝ] ℝ := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this : (Measure.map (⇑Aₘ) μ).IsAddHaarMeasure
w : V →L[ℝ] ℝ
v : V
⊢ v = ↑↑A.symm (Aₘ v)

Tactic:
exact (ContinuousLinearEquiv.symm_apply_apply A v).symm

Result:
no goals

Proof state:
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this✝¹ : MeasurableSpace V' := borel V'
this✝ : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)

Tactic:
let Adual : (V →L[ℝ] ℝ) ≃L[ℝ] V' →L[ℝ] ℝ := A.arrowCongrSL (.refl _ _)

Result:
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this✝¹ : MeasurableSpace V' := borel V'
this✝ : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : (V →L[ℝ] ℝ) ≃L[ℝ] V' →L[ℝ] ℝ := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)

Proof state:
case h.e'_3.h
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this✝¹ : MeasurableSpace V' := borel V'
this✝ : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : (V →L[ℝ] ℝ) ≃L[ℝ] V' →L[ℝ] ℝ := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this : (Measure.map (⇑Aₘ) μ).IsAddHaarMeasure
w : V →L[ℝ] ℝ
⊢ ∫ (v : V), 𝐞 (-w v) • f v ∂μ =
    ∫ (x : V), 𝐞 (-(Adual.toHomeomorph.toCocompactMap.toFun w) (Aₘ x)) • (f ∘ ⇑A.symm) (Aₘ x) ∂μ

Tactic:
congr 1 with v : 1

Result:
case h.e'_3.h.e_f.h
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this✝¹ : MeasurableSpace V' := borel V'
this✝ : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : (V →L[ℝ] ℝ) ≃L[ℝ] V' →L[ℝ] ℝ := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this : (Measure.map (⇑Aₘ) μ).IsAddHaarMeasure
w : V →L[ℝ] ℝ
v : V
⊢ 𝐞 (-w v) • f v = 𝐞 (-(Adual.toHomeomorph.toCocompactMap.toFun w) (Aₘ v)) • (f ∘ ⇑A.symm) (Aₘ v)

Proof state:
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this✝¹ : MeasurableSpace V' := borel V'
this✝ : BorelSpace V'
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)

Tactic:
let Aₘ : MeasurableEquiv V V' := A.toHomeomorph.toMeasurableEquiv

Result:
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this✝¹ : MeasurableSpace V' := borel V'
this✝ : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)

Proof state:
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this✝¹ : MeasurableSpace V' := borel V'
this✝ : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : (V →L[ℝ] ℝ) ≃L[ℝ] V' →L[ℝ] ℝ := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this : (Measure.map (⇑Aₘ) μ).IsAddHaarMeasure
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)

Tactic:
convert (tendsto_integral_exp_smul_cocompact_of_inner_product (f ∘ A.symm) (μ.map Aₘ)).comp
  Adual.toHomeomorph.toCocompactMap.cocompact_tendsto' with w

Result:
case h.e'_3.h
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this✝¹ : MeasurableSpace V' := borel V'
this✝ : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : (V →L[ℝ] ℝ) ≃L[ℝ] V' →L[ℝ] ℝ := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this : (Measure.map (⇑Aₘ) μ).IsAddHaarMeasure
w : V →L[ℝ] ℝ
⊢ ∫ (v : V), 𝐞 (-w v) • f v ∂μ =
    ((fun w => ∫ (v : V'), 𝐞 (-w v) • (f ∘ ⇑A.symm) v ∂Measure.map (⇑Aₘ) μ) ∘ Adual.toHomeomorph.toCocompactMap.toFun) w