c : Char
⊢ 0 <
    if c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1 then UInt32.ofNatCore 1 utf8Size.proof_2
    else
      if c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3 then UInt32.ofNatCore 2 utf8Size.proof_4
      else
        if c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5 then UInt32.ofNatCore 3 utf8Size.proof_6
        else UInt32.ofNatCore 4 utf8Size.proof_7
c : Char
⊢ 0 < utf8Size c
simp only [utf8Size]
case inr.inr.inr
c : Char
h✝² : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
h✝ : ¬c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5
⊢ 0 < UInt32.ofNatCore 4 utf8Size.proof_7
c : Char
⊢ 0 <
    if c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1 then UInt32.ofNatCore 1 utf8Size.proof_2
    else
      if c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3 then UInt32.ofNatCore 2 utf8Size.proof_4
      else
        if c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5 then UInt32.ofNatCore 3 utf8Size.proof_6
        else UInt32.ofNatCore 4 utf8Size.proof_7
repeat (split; decide)
no goals
case inr.inr.inr
c : Char
h✝² : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
h✝ : ¬c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5
⊢ 0 < UInt32.ofNatCore 4 utf8Size.proof_7
decide
case inr.inr.inr
c : Char
h✝² : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
h✝ : ¬c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5
⊢ 0 < UInt32.ofNatCore 4 utf8Size.proof_7
case inr.inr.inr
c : Char
h✝² : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
h✝ : ¬c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5
⊢ 0 < UInt32.ofNatCore 4 utf8Size.proof_7
(split; decide)
case inr.inr.inr
c : Char
h✝² : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
h✝ : ¬c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5
⊢ 0 < UInt32.ofNatCore 4 utf8Size.proof_7
case inr.inr.inr
c : Char
h✝² : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
h✝ : ¬c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5
⊢ 0 < UInt32.ofNatCore 4 utf8Size.proof_7
split
case inr.inr.inr
c : Char
h✝² : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
h✝ : ¬c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5
⊢ 0 < UInt32.ofNatCore 4 utf8Size.proof_7
case inr.inr.inl
c : Char
h✝² : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
h✝ : c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5
⊢ 0 < UInt32.ofNatCore 3 utf8Size.proof_6

case inr.inr.inr
c : Char
h✝² : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
h✝ : ¬c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5
⊢ 0 < UInt32.ofNatCore 4 utf8Size.proof_7
decide