[GOAL]
c : Char
⊢ 0 < utf8Size c
[PROOFSTEP]
simp only [utf8Size]
[GOAL]
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
[PROOFSTEP]
repeat (split; decide)
[GOAL]
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
[PROOFSTEP]
split
[GOAL]
case inl
c : Char
h✝ : c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
⊢ 0 < UInt32.ofNatCore 1 utf8Size.proof_2
case inr
c : Char
h✝ : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
⊢ 0 <
    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
[PROOFSTEP]
decide
[GOAL]
case inr
c : Char
h✝ : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
⊢ 0 <
    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
[PROOFSTEP]
split
[GOAL]
case inr.inl
c : Char
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝ : c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
⊢ 0 < UInt32.ofNatCore 2 utf8Size.proof_4
case inr.inr
c : Char
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
⊢ 0 <
    if c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5 then UInt32.ofNatCore 3 utf8Size.proof_6
    else UInt32.ofNatCore 4 utf8Size.proof_7
[PROOFSTEP]
decide
[GOAL]
case inr.inr
c : Char
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
⊢ 0 <
    if c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5 then UInt32.ofNatCore 3 utf8Size.proof_6
    else UInt32.ofNatCore 4 utf8Size.proof_7
[PROOFSTEP]
split
[GOAL]
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
[PROOFSTEP]
decide
[GOAL]
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
[PROOFSTEP]
split
[GOAL]
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
[PROOFSTEP]
decide
[GOAL]
c : Char
h : isValidCharNat (toNat c)
⊢ ofNat (toNat c) = c
[PROOFSTEP]
rw [Char.ofNat, dif_pos h]
[GOAL]
c : Char
h : isValidCharNat (toNat c)
⊢ ofNatAux (toNat c) h = c
[PROOFSTEP]
rfl
