c : Char
⊢ UInt32.toNat
        (if c.val ≤ UInt32.ofNatCore 127 Char.utf8Size.proof_1 then UInt32.ofNatCore 1 Char.utf8Size.proof_2
        else
          if c.val ≤ UInt32.ofNatCore 2047 Char.utf8Size.proof_3 then UInt32.ofNatCore 2 Char.utf8Size.proof_4
          else
            if c.val ≤ UInt32.ofNatCore 65535 Char.utf8Size.proof_5 then UInt32.ofNatCore 3 Char.utf8Size.proof_6
            else UInt32.ofNatCore 4 Char.utf8Size.proof_7) =
      1 ∨
    UInt32.toNat
          (if c.val ≤ UInt32.ofNatCore 127 Char.utf8Size.proof_1 then UInt32.ofNatCore 1 Char.utf8Size.proof_2
          else
            if c.val ≤ UInt32.ofNatCore 2047 Char.utf8Size.proof_3 then UInt32.ofNatCore 2 Char.utf8Size.proof_4
            else
              if c.val ≤ UInt32.ofNatCore 65535 Char.utf8Size.proof_5 then UInt32.ofNatCore 3 Char.utf8Size.proof_6
              else UInt32.ofNatCore 4 Char.utf8Size.proof_7) =
        2 ∨
      UInt32.toNat
            (if c.val ≤ UInt32.ofNatCore 127 Char.utf8Size.proof_1 then UInt32.ofNatCore 1 Char.utf8Size.proof_2
            else
              if c.val ≤ UInt32.ofNatCore 2047 Char.utf8Size.proof_3 then UInt32.ofNatCore 2 Char.utf8Size.proof_4
              else
                if c.val ≤ UInt32.ofNatCore 65535 Char.utf8Size.proof_5 then UInt32.ofNatCore 3 Char.utf8Size.proof_6
                else UInt32.ofNatCore 4 Char.utf8Size.proof_7) =
          3 ∨
        UInt32.toNat
            (if c.val ≤ UInt32.ofNatCore 127 Char.utf8Size.proof_1 then UInt32.ofNatCore 1 Char.utf8Size.proof_2
            else
              if c.val ≤ UInt32.ofNatCore 2047 Char.utf8Size.proof_3 then UInt32.ofNatCore 2 Char.utf8Size.proof_4
              else
                if c.val ≤ UInt32.ofNatCore 65535 Char.utf8Size.proof_5 then UInt32.ofNatCore 3 Char.utf8Size.proof_6
                else UInt32.ofNatCore 4 Char.utf8Size.proof_7) =
          4
c : Char
⊢ csize c = 1 ∨ csize c = 2 ∨ csize c = 3 ∨ csize c = 4
simp only [csize, Char.utf8Size]
no goals
c : Char
⊢ UInt32.toNat
        (if c.val ≤ UInt32.ofNatCore 127 Char.utf8Size.proof_1 then UInt32.ofNatCore 1 Char.utf8Size.proof_2
        else
          if c.val ≤ UInt32.ofNatCore 2047 Char.utf8Size.proof_3 then UInt32.ofNatCore 2 Char.utf8Size.proof_4
          else
            if c.val ≤ UInt32.ofNatCore 65535 Char.utf8Size.proof_5 then UInt32.ofNatCore 3 Char.utf8Size.proof_6
            else UInt32.ofNatCore 4 Char.utf8Size.proof_7) =
      1 ∨
    UInt32.toNat
          (if c.val ≤ UInt32.ofNatCore 127 Char.utf8Size.proof_1 then UInt32.ofNatCore 1 Char.utf8Size.proof_2
          else
            if c.val ≤ UInt32.ofNatCore 2047 Char.utf8Size.proof_3 then UInt32.ofNatCore 2 Char.utf8Size.proof_4
            else
              if c.val ≤ UInt32.ofNatCore 65535 Char.utf8Size.proof_5 then UInt32.ofNatCore 3 Char.utf8Size.proof_6
              else UInt32.ofNatCore 4 Char.utf8Size.proof_7) =
        2 ∨
      UInt32.toNat
            (if c.val ≤ UInt32.ofNatCore 127 Char.utf8Size.proof_1 then UInt32.ofNatCore 1 Char.utf8Size.proof_2
            else
              if c.val ≤ UInt32.ofNatCore 2047 Char.utf8Size.proof_3 then UInt32.ofNatCore 2 Char.utf8Size.proof_4
              else
                if c.val ≤ UInt32.ofNatCore 65535 Char.utf8Size.proof_5 then UInt32.ofNatCore 3 Char.utf8Size.proof_6
                else UInt32.ofNatCore 4 Char.utf8Size.proof_7) =
          3 ∨
        UInt32.toNat
            (if c.val ≤ UInt32.ofNatCore 127 Char.utf8Size.proof_1 then UInt32.ofNatCore 1 Char.utf8Size.proof_2
            else
              if c.val ≤ UInt32.ofNatCore 2047 Char.utf8Size.proof_3 then UInt32.ofNatCore 2 Char.utf8Size.proof_4
              else
                if c.val ≤ UInt32.ofNatCore 65535 Char.utf8Size.proof_5 then UInt32.ofNatCore 3 Char.utf8Size.proof_6
                else UInt32.ofNatCore 4 Char.utf8Size.proof_7) =
          4
repeat (first | split | (solve | simp))
no goals
case inr.inr.inr
c : Char
h✝² : ¬c.val ≤ UInt32.ofNatCore 127 Char.utf8Size.proof_1
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 Char.utf8Size.proof_3
h✝ : ¬c.val ≤ UInt32.ofNatCore 65535 Char.utf8Size.proof_5
⊢ UInt32.toNat (UInt32.ofNatCore 4 Char.utf8Size.proof_7) = 1 ∨
    UInt32.toNat (UInt32.ofNatCore 4 Char.utf8Size.proof_7) = 2 ∨
      UInt32.toNat (UInt32.ofNatCore 4 Char.utf8Size.proof_7) = 3 ∨
        UInt32.toNat (UInt32.ofNatCore 4 Char.utf8Size.proof_7) = 4
simp