simp only [div_right_comm _ c _, integral_div c, div_self <| ne_of_gt hΨpos]
case h.refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∫ (x : ℝ) in Ici 0, Ψ x / c / x = 1
no goals