simp only [Complex.ext_iff, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one,
  sub_self, add_zero, one_re, add_im, mul_im, zero_add, one_im] at t_gt
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
t_gt : ↑σ + ↑t * I = 1
⊢ |t| ≤ 3
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
t_gt : σ = 1 ∧ t = 0
⊢ |t| ≤ 3