simpa [Real.exp_neg, Real.exp_log hx] using this
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
l5 : IntegrableOn Ψ (rexp '' Ici (-x.log)) volume
l6 : IntegrableOn (fun x => rexp x • (Ψ ∘ rexp) x) (Ici (-x.log)) volume
this : ∫ (x : ℝ) in Ioi (-x.log), rexp x • (Ψ ∘ rexp) x = ∫ (u : ℝ) in Ioi (rexp (-x.log)), Ψ u
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
no goals