Theorem: Nat.digitChar_is_digit (One.lean)

State before:
n : ℕ
P : n < 10
⊢ Char.isDigit (digitChar n) = true
Tactic:
revert n
State after:
⊢ ∀ (n : ℕ), n < 10 → Char.isDigit (digitChar n) = true

State before:
⊢ ∀ (n : ℕ), n < 10 → Char.isDigit (digitChar n) = true
Tactic:
decide
State after:
no goals