internlm/Lean-Github huggingface dataset:
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case P
b n i : ℕ
Q : b > 1
⊢ ∀ (i_1 : ℕ),
    List.getD (List.reverse (List.lastN i (Nat.toDigits b n))) i_1 (Char.ofNat 48) =
      List.getD (List.reverse (Nat.toDigits b (n % b ^ i))) i_1 (Char.ofNat 48)
Tactic:
intro ind
Proof state after:
case P
b n i : ℕ
Q : b > 1
ind : ℕ
⊢ List.getD (List.reverse (List.lastN i (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ i))) ind (Char.ofNat 48)
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case P
b n i : ℕ
Q : b > 1
ind : ℕ
⊢ List.getD (List.reverse (List.lastN i (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ i))) ind (Char.ofNat 48)
Tactic:
simp only [ge_iff_le, List.lastN_eq_reverse_take, List.reverse_reverse]
Proof state after:
case P
b n i : ℕ
Q : b > 1
ind : ℕ
⊢ List.getD (List.take i (List.reverse (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ i))) ind (Char.ofNat 48)
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case P
b n i : ℕ
Q : b > 1
ind : ℕ
⊢ List.getD (List.take i (List.reverse (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ i))) ind (Char.ofNat 48)
Tactic:
cases i
Proof state after:
case P.zero
b n : ℕ
Q : b > 1
ind : ℕ
⊢ List.getD (List.take Nat.zero (List.reverse (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ Nat.zero))) ind (Char.ofNat 48)

case P.succ
b n : ℕ
Q : b > 1
ind n✝ : ℕ
⊢ List.getD (List.take (Nat.succ n✝) (List.reverse (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ Nat.succ n✝))) ind (Char.ofNat 48)
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
b n : ℕ
Q : b > 1
ind : ℕ
⊢ List.getD (List.take Nat.zero (List.reverse (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ Nat.zero))) ind (Char.ofNat 48)
Tactic:
case  zero =>
  simp only [List.take, List.length_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, List.getD_eq_default,
Nat.zero_eq, pow_zero, Nat.mod_one, Nat.toDigits_zero, List.reverse_cons, List.reverse_nil, List.nil_append,
List.length_singleton, List.getD_singleton_default_eq]
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
b n : ℕ
Q : b > 1
ind i : ℕ
⊢ List.getD (List.take (Nat.succ i) (List.reverse (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ Nat.succ i))) ind (Char.ofNat 48)
Tactic:
case succ i =>
cases h: decide (ind < Nat.succ i) with
| true =>
  simp only [ge_iff_le, decide_eq_true_eq] at h
  simp only [h, List.getD_take]
  rw [Nat.toDigits_modulo] <;> assumption
| false =>
  simp only [decide_eq_false_iff_not, not_lt] at h
  rw [List.getD_eq_default, List.getD_eq_default]
  . simp only [List.length_reverse, gt_iff_lt, ge_iff_le]
    rw [Nat.toDigits_length_eq_log]
    . calc
      Nat.log b (n % b ^ Nat.succ i) + 1 ≤ Nat.succ i := by
        { 
          apply Nat.succ_le_of_lt
          cases heq: n % b ^ Nat.succ i with
          | zero => simp only [Nat.zero_eq, zero_le, ge_iff_le, nonpos_iff_eq_zero, Nat.log_zero_right, Nat.succ_pos']
          | succ k => 
            rw [← heq]
            apply Nat.log_lt_of_lt_pow
            . simp only [heq, zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, Nat.succ_ne_zero, not_false_iff]
            . apply Nat.mod_lt
              apply Nat.pos_pow_of_pos
              apply Nat.lt_trans Nat.zero_lt_one Q
        }
      _ ≤ ind := h
    . exact Q
  . simp only [List.length_take, List.length_reverse, min_le_iff, ge_iff_le, h, true_or]
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
b n : ℕ
Q : b > 1
ind : ℕ
⊢ List.getD (List.take Nat.zero (List.reverse (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ Nat.zero))) ind (Char.ofNat 48)
Tactic:
simp only [List.take, List.length_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, List.getD_eq_default,
Nat.zero_eq, pow_zero, Nat.mod_one, Nat.toDigits_zero, List.reverse_cons, List.reverse_nil, List.nil_append,
List.length_singleton, List.getD_singleton_default_eq]
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
b n : ℕ
Q : b > 1
ind i : ℕ
⊢ List.getD (List.take (Nat.succ i) (List.reverse (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ Nat.succ i))) ind (Char.ofNat 48)
Tactic:
cases h: decide (ind < Nat.succ i) with
| true =>
  simp only [ge_iff_le, decide_eq_true_eq] at h
  simp only [h, List.getD_take]
  rw [Nat.toDigits_modulo] <;> assumption
| false =>
  simp only [decide_eq_false_iff_not, not_lt] at h
  rw [List.getD_eq_default, List.getD_eq_default]
  . simp only [List.length_reverse, gt_iff_lt, ge_iff_le]
    rw [Nat.toDigits_length_eq_log]
    . calc
      Nat.log b (n % b ^ Nat.succ i) + 1 ≤ Nat.succ i := by
        { 
          apply Nat.succ_le_of_lt
          cases heq: n % b ^ Nat.succ i with
          | zero => simp only [Nat.zero_eq, zero_le, ge_iff_le, nonpos_iff_eq_zero, Nat.log_zero_right, Nat.succ_pos']
          | succ k => 
            rw [← heq]
            apply Nat.log_lt_of_lt_pow
            . simp only [heq, zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, Nat.succ_ne_zero, not_false_iff]
            . apply Nat.mod_lt
              apply Nat.pos_pow_of_pos
              apply Nat.lt_trans Nat.zero_lt_one Q
        }
      _ ≤ ind := h
    . exact Q
  . simp only [List.length_take, List.length_reverse, min_le_iff, ge_iff_le, h, true_or]
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case true
b n : ℕ
Q : b > 1
ind i : ℕ
h : decide (ind < Nat.succ i) = true
⊢ List.getD (List.take (Nat.succ i) (List.reverse (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ Nat.succ i))) ind (Char.ofNat 48)
Tactic:
simp only [ge_iff_le, decide_eq_true_eq] at h
Proof state after:
case true
b n : ℕ
Q : b > 1
ind i : ℕ
h : ind < Nat.succ i
⊢ List.getD (List.take (Nat.succ i) (List.reverse (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ Nat.succ i))) ind (Char.ofNat 48)
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case true
b n : ℕ
Q : b > 1
ind i : ℕ
h : ind < Nat.succ i
⊢ List.getD (List.take (Nat.succ i) (List.reverse (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ Nat.succ i))) ind (Char.ofNat 48)
Tactic:
simp only [h, List.getD_take]
Proof state after:
case true
b n : ℕ
Q : b > 1
ind i : ℕ
h : ind < Nat.succ i
⊢ List.getD (List.reverse (Nat.toDigits b n)) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ Nat.succ i))) ind (Char.ofNat 48)
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case true
b n : ℕ
Q : b > 1
ind i : ℕ
h : ind < Nat.succ i
⊢ List.getD (List.reverse (Nat.toDigits b n)) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ Nat.succ i))) ind (Char.ofNat 48)
Tactic:
rw [Nat.toDigits_modulo] <;> assumption
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case false
b n : ℕ
Q : b > 1
ind i : ℕ
h : decide (ind < Nat.succ i) = false
⊢ List.getD (List.take (Nat.succ i) (List.reverse (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ Nat.succ i))) ind (Char.ofNat 48)
Tactic:
simp only [decide_eq_false_iff_not, not_lt] at h
Proof state after:
case false
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
⊢ List.getD (List.take (Nat.succ i) (List.reverse (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ Nat.succ i))) ind (Char.ofNat 48)
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case false
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
⊢ List.getD (List.take (Nat.succ i) (List.reverse (Nat.toDigits b n))) ind (Char.ofNat 48) =
    List.getD (List.reverse (Nat.toDigits b (n % b ^ Nat.succ i))) ind (Char.ofNat 48)
Tactic:
rw [List.getD_eq_default, List.getD_eq_default]
Proof state after:
case false.hn
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
⊢ List.length (List.reverse (Nat.toDigits b (n % b ^ Nat.succ i))) ≤ ind

case false.hn
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
⊢ List.length (List.take (Nat.succ i) (List.reverse (Nat.toDigits b n))) ≤ ind
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case false.hn
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
⊢ List.length (List.reverse (Nat.toDigits b (n % b ^ Nat.succ i))) ≤ ind

case false.hn
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
⊢ List.length (List.take (Nat.succ i) (List.reverse (Nat.toDigits b n))) ≤ ind
Tactic:
. simp only [List.length_reverse, gt_iff_lt, ge_iff_le]
  rw [Nat.toDigits_length_eq_log]
  . calc
    Nat.log b (n % b ^ Nat.succ i) + 1 ≤ Nat.succ i := by
      { 
        apply Nat.succ_le_of_lt
        cases heq: n % b ^ Nat.succ i with
        | zero => simp only [Nat.zero_eq, zero_le, ge_iff_le, nonpos_iff_eq_zero, Nat.log_zero_right, Nat.succ_pos']
        | succ k => 
          rw [← heq]
          apply Nat.log_lt_of_lt_pow
          . simp only [heq, zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, Nat.succ_ne_zero, not_false_iff]
          . apply Nat.mod_lt
            apply Nat.pos_pow_of_pos
            apply Nat.lt_trans Nat.zero_lt_one Q
      }
    _ ≤ ind := h
  . exact Q
Proof state after:
case false.hn
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
⊢ List.length (List.take (Nat.succ i) (List.reverse (Nat.toDigits b n))) ≤ ind
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case false.hn
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
⊢ List.length (List.take (Nat.succ i) (List.reverse (Nat.toDigits b n))) ≤ ind
Tactic:
. simp only [List.length_take, List.length_reverse, min_le_iff, ge_iff_le, h, true_or]
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
⊢ Nat.log b (n % b ^ Nat.succ i) + 1 ≤ Nat.succ i
Tactic:
apply Nat.succ_le_of_lt
Proof state after:
case h
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
⊢ Nat.log b (n % b ^ Nat.succ i) < Nat.succ i
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case h
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
⊢ Nat.log b (n % b ^ Nat.succ i) < Nat.succ i
Tactic:
cases heq: n % b ^ Nat.succ i with
| zero => simp only [Nat.zero_eq, zero_le, ge_iff_le, nonpos_iff_eq_zero, Nat.log_zero_right, Nat.succ_pos']
| succ k => 
  rw [← heq]
  apply Nat.log_lt_of_lt_pow
  . simp only [heq, zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, Nat.succ_ne_zero, not_false_iff]
  . apply Nat.mod_lt
    apply Nat.pos_pow_of_pos
    apply Nat.lt_trans Nat.zero_lt_one Q
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case h.zero
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
heq : n % b ^ Nat.succ i = Nat.zero
⊢ Nat.log b Nat.zero < Nat.succ i
Tactic:
simp only [Nat.zero_eq, zero_le, ge_iff_le, nonpos_iff_eq_zero, Nat.log_zero_right, Nat.succ_pos']
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case h.succ
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
k : ℕ
heq : n % b ^ Nat.succ i = Nat.succ k
⊢ Nat.log b (Nat.succ k) < Nat.succ i
Tactic:
rw [← heq]
Proof state after:
case h.succ
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
k : ℕ
heq : n % b ^ Nat.succ i = Nat.succ k
⊢ Nat.log b (n % b ^ Nat.succ i) < Nat.succ i
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case h.succ
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
k : ℕ
heq : n % b ^ Nat.succ i = Nat.succ k
⊢ Nat.log b (n % b ^ Nat.succ i) < Nat.succ i
Tactic:
apply Nat.log_lt_of_lt_pow
Proof state after:
case h.succ.hy
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
k : ℕ
heq : n % b ^ Nat.succ i = Nat.succ k
⊢ n % b ^ Nat.succ i ≠ 0

case h.succ.a
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
k : ℕ
heq : n % b ^ Nat.succ i = Nat.succ k
⊢ n % b ^ Nat.succ i < b ^ Nat.succ i
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case h.succ.hy
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
k : ℕ
heq : n % b ^ Nat.succ i = Nat.succ k
⊢ n % b ^ Nat.succ i ≠ 0

case h.succ.a
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
k : ℕ
heq : n % b ^ Nat.succ i = Nat.succ k
⊢ n % b ^ Nat.succ i < b ^ Nat.succ i
Tactic:
. simp only [heq, zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, Nat.succ_ne_zero, not_false_iff]
Proof state after:
case h.succ.a
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
k : ℕ
heq : n % b ^ Nat.succ i = Nat.succ k
⊢ n % b ^ Nat.succ i < b ^ Nat.succ i
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof state before:
case h.succ.a
b n : ℕ
Q : b > 1
ind i : ℕ
h : Nat.succ i ≤ ind
k : ℕ
heq : n % b ^ Nat.succ i = Nat.succ k
⊢ n % b ^ Nat.succ i < b ^ Nat.succ i
Tactic:
. apply Nat.mod_lt
  apply Nat.pos_pow_of_pos
  apply Nat.lt_trans Nat.zero_lt_one Q
Proof state after:
no goals
Theorem: Nat.toDigits_single_digit
Proof state before:
b n : ℕ
P : n < b
⊢ toDigits b n = [digitChar n]
Tactic:
unfold toDigits toDigitsCore
Proof state after:
b n : ℕ
P : n < b
⊢ (let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then [d] else toDigitsCore b (Nat.add n 0) n' [d]) =
    [digitChar n]
Theorem: Nat.toDigits_single_digit
Proof state before:
b n : ℕ
P : n < b
⊢ (let d := digitChar (n % b);
    let n' := n / b;
    if n' = 0 then [d] else toDigitsCore b (Nat.add n 0) n' [d]) =
    [digitChar n]
Tactic:
simp only [_root_.zero_le, ge_iff_le, nonpos_iff_eq_zero, add_eq, add_zero]
Proof state after:
b n : ℕ
P : n < b
⊢ (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b n (n / b) [digitChar (n % b)]) = [digitChar n]
Theorem: Nat.toDigits_single_digit
Proof state before:
b n : ℕ
P : n < b
⊢ (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b n (n / b) [digitChar (n % b)]) = [digitChar n]
Tactic:
split
Proof state after:
case inl
b n : ℕ
P : n < b
h✝ : n / b = 0
⊢ [digitChar (n % b)] = [digitChar n]

case inr
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ toDigitsCore b n (n / b) [digitChar (n % b)] = [digitChar n]
Theorem: Nat.toDigits_single_digit
Proof state before:
case inl
b n : ℕ
P : n < b
h✝ : n / b = 0
⊢ [digitChar (n % b)] = [digitChar n]

case inr
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ toDigitsCore b n (n / b) [digitChar (n % b)] = [digitChar n]
Tactic:
. next => 
  have h:n % b = n := by exact mod_eq_of_lt P
  simp only [h]
Proof state after:
case inr
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ toDigitsCore b n (n / b) [digitChar (n % b)] = [digitChar n]
Theorem: Nat.toDigits_single_digit
Proof state before:
case inr
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ toDigitsCore b n (n / b) [digitChar (n % b)] = [digitChar n]
Tactic:
. next =>
  unfold toDigitsCore
  simp only [_root_.zero_le, ge_iff_le, nonpos_iff_eq_zero]
  split
  . simp only [_root_.zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_mod]
  . split
    . next h _=> exfalso; apply h; exact div_eq_of_lt P
    . next h _=> exfalso; apply h; exact div_eq_of_lt P
Proof state after:
no goals
Theorem: Nat.toDigits_single_digit
Proof state before:
b n : ℕ
P : n < b
h✝ : n / b = 0
⊢ [digitChar (n % b)] = [digitChar n]
Tactic:
have h:n % b = n := by exact mod_eq_of_lt P
Proof state after:
b n : ℕ
P : n < b
h✝ : n / b = 0
h : n % b = n
⊢ [digitChar (n % b)] = [digitChar n]
Theorem: Nat.toDigits_single_digit
Proof state before:
b n : ℕ
P : n < b
h✝ : n / b = 0
h : n % b = n
⊢ [digitChar (n % b)] = [digitChar n]
Tactic:
simp only [h]
Proof state after:
no goals
Theorem: Nat.toDigits_single_digit
Proof state before:
b n : ℕ
P : n < b
h✝ : n / b = 0
⊢ n % b = n
Tactic:
exact mod_eq_of_lt P
Proof state after:
no goals
Theorem: Nat.toDigits_single_digit
Proof state before:
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ toDigitsCore b n (n / b) [digitChar (n % b)] = [digitChar n]
Tactic:
unfold toDigitsCore
Proof state after:
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ (match n, n / b, [digitChar (n % b)] with
    | 0, x, ds => ds
    | succ fuel, n, ds =>
      let d := digitChar (n % b);
      let n' := n / b;
      if n' = 0 then d :: ds else toDigitsCore b fuel n' (d :: ds)) =
    [digitChar n]
Theorem: Nat.toDigits_single_digit
Proof state before:
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ (match n, n / b, [digitChar (n % b)] with
    | 0, x, ds => ds
    | succ fuel, n, ds =>
      let d := digitChar (n % b);
      let n' := n / b;
      if n' = 0 then d :: ds else toDigitsCore b fuel n' (d :: ds)) =
    [digitChar n]
Tactic:
simp only [_root_.zero_le, ge_iff_le, nonpos_iff_eq_zero]
Proof state after:
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ (match n, n / b, [digitChar (n % b)] with
    | 0, x, ds => ds
    | succ fuel, n, ds =>
      if n / b = 0 then digitChar (n % b) :: ds else toDigitsCore b fuel (n / b) (digitChar (n % b) :: ds)) =
    [digitChar n]
Theorem: Nat.toDigits_single_digit
Proof state before:
b n : ℕ
P : n < b
h✝ : ¬n / b = 0
⊢ (match n, n / b, [digitChar (n % b)] with
    | 0, x, ds => ds
    | succ fuel, n, ds =>
      if n / b = 0 then digitChar (n % b) :: ds else toDigitsCore b fuel (n / b) (digitChar (n % b) :: ds)) =
    [digitChar n]
Tactic:
split
Proof state after:
case h_1
b x✝² x✝¹ : ℕ
x✝ : List Char
P : 0 < b
h✝ : ¬0 / b = 0
⊢ [digitChar (0 % b)] = [digitChar 0]

case h_2
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h✝ : ¬succ fuel✝ / b = 0
⊢ (if succ fuel✝ / b / b = 0 then [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]
    else toDigitsCore b fuel✝ (succ fuel✝ / b / b) [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]) =
    [digitChar (succ fuel✝)]
Theorem: Nat.toDigits_single_digit
Proof state before:
case h_1
b x✝² x✝¹ : ℕ
x✝ : List Char
P : 0 < b
h✝ : ¬0 / b = 0
⊢ [digitChar (0 % b)] = [digitChar 0]

case h_2
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h✝ : ¬succ fuel✝ / b = 0
⊢ (if succ fuel✝ / b / b = 0 then [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]
    else toDigitsCore b fuel✝ (succ fuel✝ / b / b) [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]) =
    [digitChar (succ fuel✝)]
Tactic:
. simp only [_root_.zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_mod]
Proof state after:
case h_2
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h✝ : ¬succ fuel✝ / b = 0
⊢ (if succ fuel✝ / b / b = 0 then [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]
    else toDigitsCore b fuel✝ (succ fuel✝ / b / b) [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]) =
    [digitChar (succ fuel✝)]
Theorem: Nat.toDigits_single_digit
Proof state before:
case h_2
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h✝ : ¬succ fuel✝ / b = 0
⊢ (if succ fuel✝ / b / b = 0 then [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]
    else toDigitsCore b fuel✝ (succ fuel✝ / b / b) [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)]) =
    [digitChar (succ fuel✝)]
Tactic:
. split
  . next h _=> exfalso; apply h; exact div_eq_of_lt P
  . next h _=> exfalso; apply h; exact div_eq_of_lt P
Proof state after:
no goals
Theorem: Nat.toDigits_single_digit
Proof state before:
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : succ fuel✝ / b / b = 0
⊢ [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)] = [digitChar (succ fuel✝)]
Tactic:
exfalso
Proof state after:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : succ fuel✝ / b / b = 0
⊢ False
Theorem: Nat.toDigits_single_digit
Proof state before:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : succ fuel✝ / b / b = 0
⊢ False
Tactic:
apply h
Proof state after:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : succ fuel✝ / b / b = 0
⊢ succ fuel✝ / b = 0
Theorem: Nat.toDigits_single_digit
Proof state before:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : succ fuel✝ / b / b = 0
⊢ succ fuel✝ / b = 0
Tactic:
exact div_eq_of_lt P
Proof state after:
no goals
Theorem: Nat.toDigits_single_digit
Proof state before:
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : ¬succ fuel✝ / b / b = 0
⊢ toDigitsCore b fuel✝ (succ fuel✝ / b / b) [digitChar (succ fuel✝ / b % b), digitChar (succ fuel✝ % b)] =
    [digitChar (succ fuel✝)]
Tactic:
exfalso
Proof state after:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : ¬succ fuel✝ / b / b = 0
⊢ False
Theorem: Nat.toDigits_single_digit
Proof state before:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : ¬succ fuel✝ / b / b = 0
⊢ False
Tactic:
apply h
Proof state after:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : ¬succ fuel✝ / b / b = 0
⊢ succ fuel✝ / b = 0
Theorem: Nat.toDigits_single_digit
Proof state before:
case h
b x✝² x✝¹ : ℕ
x✝ : List Char
fuel✝ : ℕ
P : succ fuel✝ < b
h : ¬succ fuel✝ / b = 0
h✝ : ¬succ fuel✝ / b / b = 0
⊢ succ fuel✝ / b = 0
Tactic:
exact div_eq_of_lt P
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
case h
n : ℕ
ih : ∀ (m : ℕ), m < n → toNatΔ (Nat.toDigits 10 m) = m
⊢ toNatΔ (Nat.toDigits 10 n) = n
Tactic:
cases n
Proof state after:
case h.zero
ih : ∀ (m : ℕ), m < Nat.zero → toNatΔ (Nat.toDigits 10 m) = m
⊢ toNatΔ (Nat.toDigits 10 Nat.zero) = Nat.zero

case h.succ
n✝ : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n✝ → toNatΔ (Nat.toDigits 10 m) = m
⊢ toNatΔ (Nat.toDigits 10 (Nat.succ n✝)) = Nat.succ n✝
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
ih : ∀ (m : ℕ), m < Nat.zero → toNatΔ (Nat.toDigits 10 m) = m
⊢ toNatΔ (Nat.toDigits 10 Nat.zero) = Nat.zero
Tactic:
case zero => decide
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
ih : ∀ (m : ℕ), m < Nat.zero → toNatΔ (Nat.toDigits 10 m) = m
⊢ toNatΔ (Nat.toDigits 10 Nat.zero) = Nat.zero
Tactic:
decide
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
⊢ toNatΔ (Nat.toDigits 10 (Nat.succ n)) = Nat.succ n
Tactic:
unfold toNatΔ toNatAux
Proof state after:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
⊢ (match Nat.toDigits 10 (Nat.succ n) with
    | [] => 0
    | head :: tail => toNatAux tail (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48)))) =
    Nat.succ n
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
⊢ (match Nat.toDigits 10 (Nat.succ n) with
    | [] => 0
    | head :: tail => toNatAux tail (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48)))) =
    Nat.succ n
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_mul, tsub_le_iff_right, zero_add]
Proof state after:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
⊢ (match Nat.toDigits 10 (Nat.succ n) with
    | [] => 0
    | head :: tail => toNatAux tail (Char.toNat head - Char.toNat (Char.ofNat 48))) =
    Nat.succ n
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
⊢ (match Nat.toDigits 10 (Nat.succ n) with
    | [] => 0
    | head :: tail => toNatAux tail (Char.toNat head - Char.toNat (Char.ofNat 48))) =
    Nat.succ n
Tactic:
split
Proof state after:
case h_1
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s✝ : List Char
heq✝ : Nat.toDigits 10 (Nat.succ n) = []
⊢ 0 = Nat.succ n

case h_2
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s✝ : List Char
head✝ : Char
tail✝ : List Char
heq✝ : Nat.toDigits 10 (Nat.succ n) = head✝ :: tail✝
⊢ toNatAux tail✝ (Char.toNat head✝ - Char.toNat (Char.ofNat 48)) = Nat.succ n