exact_mod_cast (by omega : n ≤ N)
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
n : ℕ
hn : n < N + 1
⊢ ↑n ≤ ↑N
no goals