Tanh const mul has Temperate Growth

lemma tanh_const_mul_hasTemperateGrowth (κ : ℝ) :    Function.HasTemperateGrowth (fun x => Real.tanh (κ * x)) := by  constructor  · have h : (fun x => Real.tanh (κ * x)) = (Real.tanh ∘ (fun x => κ * x)) :=      rfl    have h' : ContDiff ℝ ∞ (fun x => κ * x) := by      have h'': (fun x : ℝ => κ * x) = fun x => κ • x := rfl      rw [contDiff_infty, h'']      intro n      apply contDiff_const_smul    rw [h]    apply ContDiff.comp contDiff_top_tanh h'  · intro n    obtain ⟨D, hD⟩ := iteratedDeriv_tanh_bounded n    use 0    use D * (|κ| ^ n)    intro x    rw [tanh_const_mul_iteratedDeriv_norm_eq_iteratedFDeriv_norm, iteratedDeriv_tanh_const_mul]    field_simp    rw [abs_mul, abs_pow, mul_comm, mul_comm, mul_comm D (|κ| ^ n)]    apply mul_le_mul_of_nonneg_left    apply hD    simp only [abs_nonneg, pow_nonneg]