Complex.Hadamard.EntireOfOrderAtMost.comp_add_const

theorem comp_add_const {ρ : ℝ} {f : ℂ → ℂ} (h : EntireOfOrderAtMost ρ f)    (hρ : 0 ≤ ρ) (c : ℂ) :    EntireOfOrderAtMost ρ (fun z : ℂ => f (z + c)) := by  refine ⟨h.differentiable.comp (differentiable_id.add (differentiable_const c)), ?_⟩  intro ε hε  rcases h.exists_bound hε with ⟨C, hC, hCbound⟩  let A : ℝ := 1 + ‖c‖  let C' : ℝ := C * A ^ (ρ + ε)  have hApos : 0 < A := by    dsimp [A]    positivity  have hτnonneg : 0 ≤ ρ + ε := by linarith  refine ⟨C', mul_pos hC (Real.rpow_pos_of_pos hApos _), ?_⟩  intro z  have hbase :      1 + ‖z + c‖ ≤ A * (1 + ‖z‖) := by    dsimp [A]    have hnorm : ‖z + c‖ ≤ ‖z‖ + ‖c‖ := norm_add_le z c    nlinarith [norm_nonneg z, norm_nonneg c]  have hpow :      (1 + ‖z + c‖) ^ (ρ + ε) ≤ (A * (1 + ‖z‖)) ^ (ρ + ε) := by    exact Real.rpow_le_rpow (by positivity) hbase hτnonneg  calc    ‖f (z + c)‖ ≤ Real.exp (C * (1 + ‖z + c‖) ^ (ρ + ε)) := hCbound (z + c)    _ ≤ Real.exp (C' * (1 + ‖z‖) ^ (ρ + ε)) := by      refine Real.exp_le_exp.2 ?_      calc        C * (1 + ‖z + c‖) ^ (ρ + ε) ≤ C * (A * (1 + ‖z‖)) ^ (ρ + ε) := by          exact mul_le_mul_of_nonneg_left hpow hC.le        _ = C' * (1 + ‖z‖) ^ (ρ + ε) := by          rw [Real.mul_rpow (le_of_lt hApos) (by positivity : 0 ≤ 1 + ‖z‖)]          ring