Theorem: Nat.digitChar_sub_zero_eq_self (One.lean)

State before:
n : ℕ
P : n < 10
⊢ Char.toNat (digitChar n) - Char.toNat (Char.ofNat 48) = n
Tactic:
revert n
State after:
⊢ ∀ (n : ℕ), n < 10 → Char.toNat (digitChar n) - Char.toNat (Char.ofNat 48) = n

State before:
⊢ ∀ (n : ℕ), n < 10 → Char.toNat (digitChar n) - Char.toNat (Char.ofNat 48) = n
Tactic:
decide
State after:
no goals