congr
case h.e'_3.e_f.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
y : ℝ
⊢ Ψ (y ^ (1 / ε)) / ε / y = (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y
case h.e'_3.e_f.h.e_a.e_a.e_a.e_a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
this :
  ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (fun y => Ψ ((x / y) ^ (1 / ε)) / ε) y / ↑y
y : ℝ
⊢ y = x / (x / y)