refine ⟨Npos, N_le_t, logt_gt, σ_gt, by linarith [hA.2], ?_⟩
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
⊢ ↑σ + ↑t * I ≠ 1