-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Extra.lean
theorem length_utf8EncodeChar (c : Char) : (utf8EncodeChar c).length = c.utf8Size

Proof state:
case inr.inr
c : Char
h✝¹ : ¬c.val ≤ 127
h✝ : ¬c.val ≤ 2047
⊢ (if c.val ≤ 65535 then
        [(c.val >>> 12).toUInt8 &&& 15 ||| 224, (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]
      else
        [(c.val >>> 18).toUInt8 &&& 7 ||| 240, (c.val >>> 12).toUInt8 &&& 63 ||| 128,
          (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]).length =
    if c.val ≤ 65535 then 3 else 4

Tactic:
cases Decidable.em (c.val ≤ 0xffff) <;> simp [*]

Result:
no goals

Proof state:
c : Char
⊢ (utf8EncodeChar c).length = c.utf8Size

Tactic:
simp [Char.utf8Size, utf8EncodeChar]

Result:
c : Char
⊢ (if c.val ≤ 127 then [c.val.toUInt8]
      else
        if c.val ≤ 2047 then [(c.val >>> 6).toUInt8 &&& 31 ||| 192, c.val.toUInt8 &&& 63 ||| 128]
        else
          if c.val ≤ 65535 then
            [(c.val >>> 12).toUInt8 &&& 15 ||| 224, (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]
          else
            [(c.val >>> 18).toUInt8 &&& 7 ||| 240, (c.val >>> 12).toUInt8 &&& 63 ||| 128,
              (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]).length =
    if c.val ≤ 127 then 1 else if c.val ≤ 2047 then 2 else if c.val ≤ 65535 then 3 else 4

Proof state:
c : Char
⊢ (if c.val ≤ 127 then [c.val.toUInt8]
      else
        if c.val ≤ 2047 then [(c.val >>> 6).toUInt8 &&& 31 ||| 192, c.val.toUInt8 &&& 63 ||| 128]
        else
          if c.val ≤ 65535 then
            [(c.val >>> 12).toUInt8 &&& 15 ||| 224, (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]
          else
            [(c.val >>> 18).toUInt8 &&& 7 ||| 240, (c.val >>> 12).toUInt8 &&& 63 ||| 128,
              (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]).length =
    if c.val ≤ 127 then 1 else if c.val ≤ 2047 then 2 else if c.val ≤ 65535 then 3 else 4

Tactic:
cases Decidable.em (c.val ≤ 0x7f) <;> simp [*]

Result:
case inr
c : Char
h✝ : ¬c.val ≤ 127
⊢ (if c.val ≤ 2047 then [(c.val >>> 6).toUInt8 &&& 31 ||| 192, c.val.toUInt8 &&& 63 ||| 128]
      else
        if c.val ≤ 65535 then
          [(c.val >>> 12).toUInt8 &&& 15 ||| 224, (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]
        else
          [(c.val >>> 18).toUInt8 &&& 7 ||| 240, (c.val >>> 12).toUInt8 &&& 63 ||| 128,
            (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]).length =
    if c.val ≤ 2047 then 2 else if c.val ≤ 65535 then 3 else 4

Proof state:
case inr
c : Char
h✝ : ¬c.val ≤ 127
⊢ (if c.val ≤ 2047 then [(c.val >>> 6).toUInt8 &&& 31 ||| 192, c.val.toUInt8 &&& 63 ||| 128]
      else
        if c.val ≤ 65535 then
          [(c.val >>> 12).toUInt8 &&& 15 ||| 224, (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]
        else
          [(c.val >>> 18).toUInt8 &&& 7 ||| 240, (c.val >>> 12).toUInt8 &&& 63 ||| 128,
            (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]).length =
    if c.val ≤ 2047 then 2 else if c.val ≤ 65535 then 3 else 4

Tactic:
cases Decidable.em (c.val ≤ 0x7ff) <;> simp [*]

Result:
case inr.inr
c : Char
h✝¹ : ¬c.val ≤ 127
h✝ : ¬c.val ≤ 2047
⊢ (if c.val ≤ 65535 then
        [(c.val >>> 12).toUInt8 &&& 15 ||| 224, (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]
      else
        [(c.val >>> 18).toUInt8 &&& 7 ||| 240, (c.val >>> 12).toUInt8 &&& 63 ||| 128,
          (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]).length =
    if c.val ≤ 65535 then 3 else 4