Liouville's theorem (bounded entire is constant)

import Mathlib

theorem liouville_thm (f : ℂ → ℂ) (hf : Differentiable ℂ f) (hb : ∃ M, ∀ z, ‖f z‖ ≤ M) : ∃ c, ∀ z, f z = c := by
  apply hf.exists_const_forall_eq_of_bounded
  rw [isBounded_iff_forall_norm_le]
  rcases hb with ⟨M, hM⟩
  use M
  rintro _ ⟨z, rfl⟩
  exact hM z