import Mathlib

instance : Countable Char where
  exists_injective_nat' := by
    use Char.toNat
    intro c₁ c₂ hc
    rw [Char.toNat, Char.toNat, UInt32.toNat_inj] at hc
    exact Char.eq_of_val_eq hc

instance : Countable String := Countable.of_equiv (List Char)
  { toFun := String.mk
    invFun := String.data
    left_inv x := by simp
    right_inv x := by simp }