-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem integrable_cexp_neg_mul_sq_norm_add (hb : 0 < b.re) (c : ℂ) (w : V) :
    Integrable (fun (v : V) ↦ cexp (-b * ‖v‖^2 + c * ⟪w, v⟫))

Proof state:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ Integrable (fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v))) volume

Tactic:
rw [← e.measurePreserving.integrable_comp_emb e.toHomeomorph.measurableEmbedding]

Result:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ Integrable ((fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v))) ∘ ⇑e) volume

Proof state:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ Integrable ((fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v))) ∘ ⇑e) volume

Tactic:
convert integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace
  hb c (e.symm w) with v

Result:
case h.e'_6.h
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
v : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))
⊢ ((fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v))) ∘ ⇑e) v = cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner (e.symm w) v))

Proof state:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
⊢ Integrable (fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v))) volume

Tactic:
let e := (stdOrthonormalBasis ℝ V).repr.symm

Result:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ Integrable (fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v))) volume

Proof state:
case h.e'_6.h
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
v : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))
⊢ ((fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v))) ∘ ⇑e) v = cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner (e.symm w) v))

Tactic:
simp only [neg_mul, Function.comp_apply, LinearIsometryEquiv.norm_map,
  LinearIsometryEquiv.symm_symm, conj_trivial, ofReal_sum,
  ofReal_mul, LinearIsometryEquiv.inner_map_eq_flip]

Result:
no goals