rw [← ofReal_one, ← mass_one]
case h.e'_7.h.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
x✝ : ℝ
⊢ 1 = ∫ (x : ℝ) in Ioi 0, ↑(Ψ x / x)
case h.e'_7.h.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
diff : DifferentiableWithinAt ℝ (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) (Ioi 0) 0
this : (fun x => 𝓜 (fun x => ↑(Ψ x)) ↑x - 𝓜 (fun x => ↑(Ψ x)) 0) =O[𝓝[>] 0] fun x => x
x✝ : ℝ
⊢ ↑(∫ (x : ℝ) in Ioi 0, Ψ x / x) = ∫ (x : ℝ) in Ioi 0, ↑(Ψ x / x)