calc
  _ = ∫ (y : ℝ) in Ioi 0, (Ψ (y ^ (1 / ε)) / ε) / y := ?_
  _ = ∫ (y : ℝ) in Ioi 0, Ψ y / y := ?_
  _ = 1 := mass_one
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y

case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
Ψ : ℝ → ℝ
xpos : 0 < x
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∫ (y : ℝ) in Ioi 0, Ψ (y ^ (1 / ε)) / ε / y = ∫ (y : ℝ) in Ioi 0, Ψ y / y