From bb538e15ad92474ba5f94fcdaccf493d5fd3e35a Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 5 Jun 2024 09:27:47 +1000
Subject: [PATCH] chore: upstream Char lemmas from Mathlib

---
 src/Init/Data/Char/Basic.lean  | 9 ++++++++-
 src/Init/Data/Char/Lemmas.lean | 9 +++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/Char/Basic.lean b/src/Init/Data/Char/Basic.lean
index 4447e2134329..c8a025373fa3 100644
--- a/src/Init/Data/Char/Basic.lean
+++ b/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'
 
diff --git a/src/Init/Data/Char/Lemmas.lean b/src/Init/Data/Char/Lemmas.lean
index 017b9b0c4faa..67d41f973338 100644
--- a/src/Init/Data/Char/Lemmas.lean
+++ b/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