chore: upstream Char lemmas from Mathlib (#4348)

The main purpose here is to add `Char.ofUInt8`, so I can delete the
semantically suspect `UInt8.toLower` etc in Mathlib.

src/Init/Data/Char/Basic.lean

@@ -40,7 +40,7 @@ theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < UInt32.size := by
     apply Nat.lt_trans h₂
     decide
 
-theorem isValidChar_of_isValidChar_Nat (n : Nat) (h : isValidCharNat n) : isValidChar (UInt32.ofNat' n (isValidUInt32 n h)) :=
+theorem isValidChar_of_isValidCharNat (n : Nat) (h : isValidCharNat n) : isValidChar (UInt32.ofNat' n (isValidUInt32 n h)) :=
   match h with
   | Or.inl h        => Or.inl h
   | Or.inr ⟨h₁, h₂⟩ => Or.inr ⟨h₁, h₂⟩
@@ -52,6 +52,13 @@ theorem isValidChar_zero : isValidChar 0 :=
 @[inline] def toNat (c : Char) : Nat :=
   c.val.toNat
 
+/-- Convert a character into a `UInt8`, by truncating (reducing modulo 256) if necessary. -/
+@[inline] def toUInt8 (c : Char) : UInt8 :=
+  c.val.toUInt8
+
+/-- The numbers from 0 to 256 are all valid UTF-8 characters, so we can embed one in the other. -/
+def ofUInt8 (n : UInt8) : Char := ⟨n.toUInt32, .inl (Nat.lt_trans n.1.2 (by decide))⟩
+
 instance : Inhabited Char where
   default := 'A'
 

src/Init/Data/Char/Lemmas.lean

@@ -22,4 +22,13 @@ protected theorem le_total (a b : Char) : a ≤ b ∨ b ≤ a := UInt32.le_total
 protected theorem lt_asymm {a b : Char} (h : a < b) : ¬ b < a := UInt32.lt_asymm h
 protected theorem ne_of_lt {a b : Char} (h : a < b) : a ≠ b := Char.ne_of_val_ne (UInt32.ne_of_lt h)
 
+theorem utf8Size_pos (c : Char) : 0 < c.utf8Size := by
+  simp only [utf8Size]
+  repeat (split; decide)
+  decide
+
+@[simp] theorem ofNat_toNat (c : Char) : Char.ofNat c.toNat = c := by
+  rw [Char.ofNat, dif_pos]
+  rfl
+
 end Char