Theorem: ASCII.Char.toUnicode_eq_iff_ofUnicode_eq (ASCII/Lemmas.lean)

State before:
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
⊢ ↑c = u ↔ ofUnicode u hu = c
Tactic:
simp only [Char.toUnicode, ofUnicode]
State after:
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { val := c.toByte.toUInt32, valid := ⋯ } = u ↔ { toByte := u.val.toUInt8, valid := ⋯ } = c

State before:
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { val := c.toByte.toUInt32, valid := ⋯ } = u ↔ { toByte := u.val.toUInt8, valid := ⋯ } = c
Tactic:
constructor
State after:
case mp
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { val := c.toByte.toUInt32, valid := ⋯ } = u → { toByte := u.val.toUInt8, valid := ⋯ } = c

case mpr
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { toByte := u.val.toUInt8, valid := ⋯ } = c → { val := c.toByte.toUInt32, valid := ⋯ } = u

State before:
case mp
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { val := c.toByte.toUInt32, valid := ⋯ } = u → { toByte := u.val.toUInt8, valid := ⋯ } = c
Tactic:
intro h
State after:
case mp
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
h : { val := c.toByte.toUInt32, valid := ⋯ } = u
⊢ { toByte := u.val.toUInt8, valid := ⋯ } = c

State before:
case mp
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
h : { val := c.toByte.toUInt32, valid := ⋯ } = u
⊢ { toByte := u.val.toUInt8, valid := ⋯ } = c
Tactic:
cases h
State after:
case mp.refl
c : ASCII.Char
hu : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ } = c

State before:
case mp.refl
c : ASCII.Char
hu : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ } = c
Tactic:
simp [_root_.Char.isASCII, _root_.Char.toNat] at hu
State after:
case mp.refl
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ } = c

State before:
case mp.refl
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ } = c
Tactic:
have hlt : c.toNat < 256 := by apply Nat.lt_trans hu; decide
State after:
case mp.refl
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
hlt : c.toNat < 256
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ } = c

State before:
case mp.refl
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
hlt : c.toNat < 256
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ } = c
Tactic:
ext
State after:
case mp.refl.a.a
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
hlt : c.toNat < 256
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ }.toByte.toNat = c.toByte.toNat

State before:
case mp.refl.a.a
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
hlt : c.toNat < 256
⊢ { toByte := { val := c.toByte.toUInt32, valid := ⋯ }.val.toUInt8, valid := ⋯ }.toByte.toNat = c.toByte.toNat
Tactic:
simp [Nat.mod_eq_of_lt hlt]
State after:
no goals

State before:
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
⊢ c.toNat < 256
Tactic:
apply Nat.lt_trans hu
State after:
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
⊢ 128 < 256

State before:
c : ASCII.Char
hu✝ : { val := c.toByte.toUInt32, valid := ⋯ }.isASCII = true
hu : c.toByte.toNat < 128
⊢ 128 < 256
Tactic:
decide
State after:
no goals

State before:
case mpr
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { toByte := u.val.toUInt8, valid := ⋯ } = c → { val := c.toByte.toUInt32, valid := ⋯ } = u
Tactic:
intro h
State after:
case mpr
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
h : { toByte := u.val.toUInt8, valid := ⋯ } = c
⊢ { val := c.toByte.toUInt32, valid := ⋯ } = u

State before:
case mpr
c : ASCII.Char
u : Unicode.Char
hu : Char.isASCII u = true
h : { toByte := u.val.toUInt8, valid := ⋯ } = c
⊢ { val := c.toByte.toUInt32, valid := ⋯ } = u
Tactic:
cases h
State after:
case mpr.refl
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ } = u

State before:
case mpr.refl
u : Unicode.Char
hu : Char.isASCII u = true
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ } = u
Tactic:
simp [_root_.Char.isASCII, _root_.Char.toNat] at hu
State after:
case mpr.refl
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ } = u

State before:
case mpr.refl
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ } = u
Tactic:
have hlt : u.val.toNat < 256 := by apply Nat.lt_trans hu; decide
State after:
case mpr.refl
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
hlt : u.val.toNat < 256
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ } = u

State before:
case mpr.refl
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
hlt : u.val.toNat < 256
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ } = u
Tactic:
ext
State after:
case mpr.refl.a.a
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
hlt : u.val.toNat < 256
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ }.val.toNat = u.val.toNat

State before:
case mpr.refl.a.a
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
hlt : u.val.toNat < 256
⊢ { val := { toByte := u.val.toUInt8, valid := ⋯ }.toByte.toUInt32, valid := ⋯ }.val.toNat = u.val.toNat
Tactic:
simp [Nat.mod_eq_of_lt hlt]
State after:
no goals

State before:
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
⊢ u.val.toNat < 256
Tactic:
apply Nat.lt_trans hu
State after:
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
⊢ 128 < 256

State before:
u : Unicode.Char
hu✝ : Char.isASCII u = true
hu : u.val.toNat < 128
⊢ 128 < 256
Tactic:
decide
State after:
no goals