FKS2.t_mul_exp_neg_one_thousandth_le_five_hundred

lemma t_mul_exp_neg_one_thousandth_le_five_hundred    (t : ℝ) (_ht : t ≥ 1000) :    t * exp (-(1 / 1000 : ℝ) * t) ≤ 500 := by  have htwo : 2 * (t / 1000) ≤ exp (t / 1000) := Real.two_mul_le_exp  have ht_le : t ≤ 500 * exp (t / 1000) := by    have hmul := mul_le_mul_of_nonneg_left htwo (by norm_num : (0 : ℝ) ≤ 500)    have hmul' : 500 * (2 * (t / 1000)) ≤ 500 * exp (t / 1000) := by      simpa [mul_assoc, mul_left_comm, mul_comm] using hmul    calc      t = 500 * (2 * (t / 1000)) := by        ring_nf      _ ≤ 500 * exp (t / 1000) := hmul'  have hdiv : t / exp (t / 1000) ≤ 500 := (div_le_iff₀ (Real.exp_pos _)).2 ht_le  have hdiv' : t * (exp (t / 1000))⁻¹ ≤ 500 := by    simpa [div_eq_mul_inv] using hdiv  have hexp_inv : exp (-(1 / 1000 : ℝ) * t) = (exp (t / 1000))⁻¹ := by    rw [show (-(1 / 1000 : ℝ) * t) = -(t / 1000) by ring_nf, Real.exp_neg]  calc    t * exp (-(1 / 1000 : ℝ) * t) = t * (exp (t / 1000))⁻¹ := by      rw [hexp_inv]    _ ≤ 500 := hdiv'