Theorem: String.toNatΔ_cons (One.lean)

State before:
head : Char
tail : List Char
⊢ toNatΔ (head :: tail) = (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail + toNatΔ tail
Tactic:
unfold String.toNatΔ
State after:
head : Char
tail : List Char
⊢ toNatAux (head :: tail) 0 = (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail + toNatAux tail 0

State before:
head : Char
tail : List Char
⊢ toNatAux (head :: tail) 0 = (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail + toNatAux tail 0
Tactic:
rw [String.toNatAux, String.toNatAux_accumulates]
State after:
head : Char
tail : List Char
⊢ toNatAux tail 0 + (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail + toNatAux tail 0

State before:
head : Char
tail : List Char
⊢ toNatAux tail 0 + (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48))) * 10 ^ List.length tail =
    (Char.toNat head - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tail + toNatAux tail 0
Tactic:
ring
State after:
no goals