Theorem: Nat.toDigits_eq_digit (One.lean)

State before:
b n : ℕ
P : b > 1
⊢ ∀ (i : ℕ),
    i < List.length (toDigits b n) →
      List.getD (toDigits b n) i (Char.ofNat 48) = digitChar (digit b n (List.length (toDigits b n) - 1 - i))
Tactic:
intro i h
State after:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.getD (toDigits b n) i (Char.ofNat 48) = digitChar (digit b n (List.length (toDigits b n) - 1 - i))

State before:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.getD (toDigits b n) i (Char.ofNat 48) = digitChar (digit b n (List.length (toDigits b n) - 1 - i))
Tactic:
rw [← Nat.toDigits_eq_digit_rev b n P (List.length (Nat.toDigits b n) - 1 - i)]
State after:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.getD (toDigits b n) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b n)) (List.length (toDigits b n) - 1 - i) (Char.ofNat 48)

State before:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.getD (toDigits b n) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b n)) (List.length (toDigits b n) - 1 - i) (Char.ofNat 48)
Tactic:
rw [ List.getD, List.getD, List.get?_reverse]
State after:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ Option.getD (List.get? (toDigits b n) i) (Char.ofNat 48) =
    Option.getD (List.get? (toDigits b n) (List.length (toDigits b n) - 1 - (List.length (toDigits b n) - 1 - i)))
      (Char.ofNat 48)

case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.length (toDigits b n) - 1 - i < List.length (toDigits b n)

State before:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ Option.getD (List.get? (toDigits b n) i) (Char.ofNat 48) =
    Option.getD (List.get? (toDigits b n) (List.length (toDigits b n) - 1 - (List.length (toDigits b n) - 1 - i)))
      (Char.ofNat 48)

case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.length (toDigits b n) - 1 - i < List.length (toDigits b n)
Tactic:
congr
State after:
case e_a.e_a
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ i = List.length (toDigits b n) - 1 - (List.length (toDigits b n) - 1 - i)

case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.length (toDigits b n) - 1 - i < List.length (toDigits b n)

State before:
case e_a.e_a
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ i = List.length (toDigits b n) - 1 - (List.length (toDigits b n) - 1 - i)

case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.length (toDigits b n) - 1 - i < List.length (toDigits b n)
Tactic:
. have h₂: List.length (toDigits b n) - 1 ≥ (List.length (toDigits b n) - 1 - i) := by simp
  have h₃: List.length (toDigits b n) ≥ 1 := by calc 
    List.length (toDigits b n) > i := h
    _ ≥ 0 := by simp only [ge_iff_le, _root_.zero_le]
  have h₄: i ≤ List.length (toDigits b n) - 1 := by apply Nat.le_pred_of_lt; exact h
  zify [h₂, h₃, h₄]
  apply Int.eq_of_sub_eq_zero
  ring_nf
State after:
case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.length (toDigits b n) - 1 - i < List.length (toDigits b n)

State before:
case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.length (toDigits b n) - 1 - i < List.length (toDigits b n)
Tactic:
. rw [Nat.sub_sub]
  apply Nat.sub_lt_self
  . simp only [add_pos_iff, true_or]
  . rw [Nat.add_comm]
    apply Nat.lt_iff_add_one_le.1 h
State after:
no goals

State before:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
⊢ List.length (toDigits b n) - 1 ≥ List.length (toDigits b n) - 1 - i
Tactic:
simp
State after:
no goals

State before:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
h₂ : List.length (toDigits b n) - 1 ≥ List.length (toDigits b n) - 1 - i
⊢ List.length (toDigits b n) ≥ 1
Tactic:
calc 
List.length (toDigits b n) > i := h
_ ≥ 0 := by simp only [ge_iff_le, _root_.zero_le]
State after:
no goals

State before:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
h₂ : List.length (toDigits b n) - 1 ≥ List.length (toDigits b n) - 1 - i
⊢ i ≥ 0
Tactic:
simp only [ge_iff_le, _root_.zero_le]
State after:
no goals

State before:
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
h₂ : List.length (toDigits b n) - 1 ≥ List.length (toDigits b n) - 1 - i
h₃ : List.length (toDigits b n) ≥ 1
⊢ i ≤ List.length (toDigits b n) - 1
Tactic:
apply Nat.le_pred_of_lt
State after:
case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
h₂ : List.length (toDigits b n) - 1 ≥ List.length (toDigits b n) - 1 - i
h₃ : List.length (toDigits b n) ≥ 1
⊢ i < List.length (toDigits b n)

State before:
case h
b n : ℕ
P : b > 1
i : ℕ
h : i < List.length (toDigits b n)
h₂ : List.length (toDigits b n) - 1 ≥ List.length (toDigits b n) - 1 - i
h₃ : List.length (toDigits b n) ≥ 1
⊢ i < List.length (toDigits b n)
Tactic:
exact h
State after:
no goals