Theorem: Nat.toDigits_digits (One.lean)

State before:
b n : ℕ
P : b ≤ 10
Q : b > 1
⊢ (List.all (toDigits b n) Char.isDigit == true) = true
Tactic:
let h:  ∀ c, c ∈ Nat.toDigitsCore b (n+1) n [] → Char.isDigit c = true ∨ c ∈ [] := by
  intro c
  apply Nat.toDigitsCore_digits  _ _ P Q
State after:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true ∨ c ∈ [] :=
  fun c => toDigitsCore_digits b n P Q
⊢ (List.all (toDigits b n) Char.isDigit == true) = true

State before:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true ∨ c ∈ [] :=
  fun c => toDigitsCore_digits b n P Q
⊢ (List.all (toDigits b n) Char.isDigit == true) = true
Tactic:
simp
State after:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true ∨ c ∈ [] :=
  fun c => toDigitsCore_digits b n P Q
⊢ ∀ (x : Char), x ∈ toDigits b n → Char.isDigit x = true

State before:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true ∨ c ∈ [] :=
  fun c => toDigitsCore_digits b n P Q
⊢ ∀ (x : Char), x ∈ toDigits b n → Char.isDigit x = true
Tactic:
simp at h
State after:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true
⊢ ∀ (x : Char), x ∈ toDigits b n → Char.isDigit x = true

State before:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true
⊢ ∀ (x : Char), x ∈ toDigits b n → Char.isDigit x = true
Tactic:
unfold Nat.toDigits
State after:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true
⊢ ∀ (x : Char), x ∈ toDigitsCore b (n + 1) n [] → Char.isDigit x = true

State before:
b n : ℕ
P : b ≤ 10
Q : b > 1
h : ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true
⊢ ∀ (x : Char), x ∈ toDigitsCore b (n + 1) n [] → Char.isDigit x = true
Tactic:
apply h
State after:
no goals

State before:
b n : ℕ
P : b ≤ 10
Q : b > 1
⊢ ∀ (c : Char), c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true ∨ c ∈ []
Tactic:
intro c
State after:
b n : ℕ
P : b ≤ 10
Q : b > 1
c : Char
⊢ c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true ∨ c ∈ []

State before:
b n : ℕ
P : b ≤ 10
Q : b > 1
c : Char
⊢ c ∈ toDigitsCore b (n + 1) n [] → Char.isDigit c = true ∨ c ∈ []
Tactic:
apply Nat.toDigitsCore_digits  _ _ P Q
State after:
no goals