Theorem: String.toNatΔ_inv_NattoDigits_tail (One.lean)

State before:
b n i : ℕ
Q : b > 1
⊢ toNatΔ (List.lastN i (Nat.toDigits b n)) = toNatΔ (Nat.toDigits b (n % b ^ i))
Tactic:
apply String.toNatΔ_eq_of_rev_get_eq
State after:
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)

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
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)

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]
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)

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
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)

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]
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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
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)

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]
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)

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
State after:
no goals

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
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)

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]
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

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
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

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]
State after:
no goals

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
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

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
State after:
no goals

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']
State after:
no goals

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]
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

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
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

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]
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

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
State after:
no goals