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

State before:
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toNat = n ↔ ofNatAux n hn = c
Tactic:
simp only [toNat, ofNatAux]
State after:
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toByte.toNat = n ↔ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c

State before:
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toByte.toNat = n ↔ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c
Tactic:
constructor
State after:
case mp
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toByte.toNat = n → { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c

case mpr
c : ASCII.Char
n : Nat
hn : n < 128
⊢ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c → c.toByte.toNat = n

State before:
case mp
c : ASCII.Char
n : Nat
hn : n < 128
⊢ c.toByte.toNat = n → { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c
Tactic:
intro h
State after:
case mp
c : ASCII.Char
n : Nat
hn : n < 128
h : c.toByte.toNat = n
⊢ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c

State before:
case mp
c : ASCII.Char
n : Nat
hn : n < 128
h : c.toByte.toNat = n
⊢ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c
Tactic:
cases h
State after:
case mp.refl
c : ASCII.Char
hn : c.toByte.toNat < 128
⊢ { toByte := { val := ⟨c.toByte.toNat, ⋯⟩ }, valid := hn } = c

State before:
case mp.refl
c : ASCII.Char
hn : c.toByte.toNat < 128
⊢ { toByte := { val := ⟨c.toByte.toNat, ⋯⟩ }, valid := hn } = c
Tactic:
ext
State after:
case mp.refl.a.a
c : ASCII.Char
hn : c.toByte.toNat < 128
⊢ { toByte := { val := ⟨c.toByte.toNat, ⋯⟩ }, valid := hn }.toByte.toNat = c.toByte.toNat

State before:
case mp.refl.a.a
c : ASCII.Char
hn : c.toByte.toNat < 128
⊢ { toByte := { val := ⟨c.toByte.toNat, ⋯⟩ }, valid := hn }.toByte.toNat = c.toByte.toNat
Tactic:
simp only [dif_pos c.toNat_lt, UInt8.toNat]
State after:
no goals

State before:
case mpr
c : ASCII.Char
n : Nat
hn : n < 128
⊢ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c → c.toByte.toNat = n
Tactic:
intro h
State after:
case mpr
c : ASCII.Char
n : Nat
hn : n < 128
h : { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c
⊢ c.toByte.toNat = n

State before:
case mpr
c : ASCII.Char
n : Nat
hn : n < 128
h : { toByte := { val := ⟨n, ⋯⟩ }, valid := hn } = c
⊢ c.toByte.toNat = n
Tactic:
cases h
State after:
case mpr.refl
n : Nat
hn : n < 128
⊢ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn }.toByte.toNat = n

State before:
case mpr.refl
n : Nat
hn : n < 128
⊢ { toByte := { val := ⟨n, ⋯⟩ }, valid := hn }.toByte.toNat = n
Tactic:
simp only [dif_pos hn, ofNatAux, UInt8.toNat]
State after:
no goals