CH2.tendsto_T_plus_one_mul_exp_atTop_nhds_zero

lemma tendsto_T_plus_one_mul_exp_atTop_nhds_zero {k : ℝ} (hk : k < 0) (C : ℝ) :    Filter.Tendsto (fun (T : ℝ) ↦ C * (T + 1) * Real.exp (k * T)) Filter.atTop (nhds 0) := by  have h_top : Filter.Tendsto (fun T ↦ - k * T) Filter.atTop Filter.atTop := by    apply Filter.tendsto_id.const_mul_atTop (by linarith)  have h_exp_lim := Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero 1 |>.comp h_top  have h_exp_lim0 := Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero 0 |>.comp h_top  simp only [Function.comp_def, pow_one, pow_zero, one_mul, neg_mul, neg_neg] at h_exp_lim h_exp_lim0  have h_Texp : Filter.Tendsto (fun T ↦ T * Real.exp (k * T)) Filter.atTop (nhds 0) := by    convert h_exp_lim.const_mul (-k⁻¹) using 1    · ext T; field_simp [hk.ne]    · simp  have h_add : Filter.Tendsto (fun T ↦ (T + 1) * Real.exp (k * T)) Filter.atTop (nhds 0) := by    simp only [add_mul, one_mul]    convert h_Texp.add h_exp_lim0 using 1    simp  convert h_add.const_mul C using 1  · ext T; ring  · simp