simp only [ne_eq, div_eq_zero_iff, one_ne_zero, εpos.ne', or_self, not_false_eq_true]
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ 1 / ε ≠ 0
no goals