simp only [ne_eq, Nat.cast_eq_zero, n_ne_zero, not_false_eq_true]
case neg.e_a.e_a.refine_3.h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
t : ℝ
n_ne_zero : ¬n = 0
this : (↑X / ↑n * ↑n) ^ (2 + ↑t * I) = (↑X / ↑n) ^ (2 + ↑t * I) * ↑n ^ (2 + ↑t * I)
⊢ ↑n ≠ 0
no goals