rw [div_eq_mul_inv, Real.rpow_mul (by positivity), ← Real.exp_mul, ← Real.exp_mul, mul_comm,
  ← mul_assoc, inv_mul_cancel, one_mul]
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t|.log.exp ^ (A / |t|.log) ≤ A.exp
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t|.log ≠ 0