internlm/Lean-Github huggingface dataset:
Theorem: List.lastN_eq_reverse_take
Proof state before:
case cons.true.h
α : Type u_1
head : α
tail : List α
ih : ∀ (n : ℕ), drop (length tail - n) tail = reverse (take n (reverse tail))
n : ℕ
h : n ≤ length tail
⊢ n ≤ length tail
Tactic:
. apply h
Proof state after:
no goals
Theorem: Nat.digitChar_sub_zero_eq_self
Proof state before:
n : ℕ
P : n < 10
⊢ Char.toNat (digitChar n) - Char.toNat (Char.ofNat 48) = n
Tactic:
revert n
Proof state after:
⊢ ∀ (n : ℕ), n < 10 → Char.toNat (digitChar n) - Char.toNat (Char.ofNat 48) = n
Theorem: Nat.digitChar_sub_zero_eq_self
Proof state before:
⊢ ∀ (n : ℕ), n < 10 → Char.toNat (digitChar n) - Char.toNat (Char.ofNat 48) = n
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.sub_self_sub_eq_min
Proof state before:
n k : ℕ
⊢ n - (n - k) = Nat.min n k
Tactic:
conv => left; right; rw [Nat.sub_eq_sub_min]
Proof state after:
n k : ℕ
⊢ n - (n - min n k) = Nat.min n k
Theorem: Nat.sub_self_sub_eq_min
Proof state before:
n k : ℕ
⊢ n - (n - min n k) = Nat.min n k
Tactic:
rw [Nat.sub_sub_self]
Proof state after:
n k : ℕ
⊢ min n k ≤ n
Theorem: Nat.sub_self_sub_eq_min
Proof state before:
n k : ℕ
⊢ min n k ≤ n
Tactic:
simp only [min_le_iff, ge_iff_le, le_refl, true_or]
Proof state after:
no goals
Theorem: List.lastN_eq_tail
Proof state before:
α : Type u_1
l : List α
⊢ lastN (length l - 1) l = tail l
Tactic:
unfold List.lastN
Proof state after:
α : Type u_1
l : List α
⊢ drop (length l - (length l - 1)) l = tail l
Theorem: List.lastN_eq_tail
Proof state before:
α : Type u_1
l : List α
⊢ drop (length l - (length l - 1)) l = tail l
Tactic:
rw [Nat.sub_self_sub_eq_min]
Proof state after:
α : Type u_1
l : List α
⊢ drop (Nat.min (length l) 1) l = tail l
Theorem: List.lastN_eq_tail
Proof state before:
α : Type u_1
l : List α
⊢ drop (Nat.min (length l) 1) l = tail l
Tactic:
cases l with
| nil => simp only [drop, tail_nil]
| cons hd tl => 
  have h: Nat.succ (List.length tl) ≥ 1 := by 
    apply Nat.succ_le_succ
    apply Nat.zero_le
  simp only [length_cons, Nat.min_eq_right h, ge_iff_le, drop, tail_cons]
Proof state after:
no goals
Theorem: List.lastN_eq_tail
Proof state before:
case nil
α : Type u_1
⊢ drop (Nat.min (length []) 1) [] = tail []
Tactic:
simp only [drop, tail_nil]
Proof state after:
no goals
Theorem: List.lastN_eq_tail
Proof state before:
case cons
α : Type u_1
hd : α
tl : List α
⊢ drop (Nat.min (length (hd :: tl)) 1) (hd :: tl) = tail (hd :: tl)
Tactic:
have h: Nat.succ (List.length tl) ≥ 1 := by 
  apply Nat.succ_le_succ
  apply Nat.zero_le
Proof state after:
case cons
α : Type u_1
hd : α
tl : List α
h : Nat.succ (length tl) ≥ 1
⊢ drop (Nat.min (length (hd :: tl)) 1) (hd :: tl) = tail (hd :: tl)
Theorem: List.lastN_eq_tail
Proof state before:
case cons
α : Type u_1
hd : α
tl : List α
h : Nat.succ (length tl) ≥ 1
⊢ drop (Nat.min (length (hd :: tl)) 1) (hd :: tl) = tail (hd :: tl)
Tactic:
simp only [length_cons, Nat.min_eq_right h, ge_iff_le, drop, tail_cons]
Proof state after:
no goals
Theorem: List.lastN_eq_tail
Proof state before:
α : Type u_1
hd : α
tl : List α
⊢ Nat.succ (length tl) ≥ 1
Tactic:
apply Nat.succ_le_succ
Proof state after:
case a
α : Type u_1
hd : α
tl : List α
⊢ 0 ≤ length tl
Theorem: List.lastN_eq_tail
Proof state before:
case a
α : Type u_1
hd : α
tl : List α
⊢ 0 ≤ length tl
Tactic:
apply Nat.zero_le
Proof state after:
no goals
Theorem: Nat.toDigits_zero
Proof state before:
b : ℕ
⊢ toDigits b 0 = [Char.ofNat 48]
Tactic:
unfold toDigits toDigitsCore
Proof state after:
b : ℕ
⊢ (let d := digitChar (0 % b);
    let n' := 0 / b;
    if n' = 0 then [d] else toDigitsCore b 0 n' [d]) =
    [Char.ofNat 48]
Theorem: Nat.toDigits_zero
Proof state before:
b : ℕ
⊢ (let d := digitChar (0 % b);
    let n' := 0 / b;
    if n' = 0 then [d] else toDigitsCore b 0 n' [d]) =
    [Char.ofNat 48]
Tactic:
simp only [_root_.zero_le, ge_iff_le, nonpos_iff_eq_zero, Nat.zero_div, zero_mod, ite_true, List.cons.injEq]
Proof state after:
no goals
Theorem: Nat.toDigits_modulo
Proof state before:
b n p i : ℕ
P : i < p
Q : b > 1
⊢ List.getD (List.reverse (toDigits b (n % b ^ p))) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48)
Tactic:
rw [Nat.toDigits_eq_digit_rev, Nat.toDigits_eq_digit_rev]
Proof state after:
b n p i : ℕ
P : i < p
Q : b > 1
⊢ digitChar (digit b (n % b ^ p) i) = digitChar (digit b n i)

case P
b n p i : ℕ
P : i < p
Q : b > 1
⊢ b > 1

case P
b n p i : ℕ
P : i < p
Q : b > 1
⊢ b > 1
Theorem: Nat.toDigits_modulo
Proof state before:
b n p i : ℕ
P : i < p
Q : b > 1
⊢ b > 1
Tactic:
case P => exact Q
Proof state after:
no goals
Theorem: Nat.toDigits_modulo
Proof state before:
b n p i : ℕ
P : i < p
Q : b > 1
⊢ digitChar (digit b (n % b ^ p) i) = digitChar (digit b n i)
Tactic:
congr 1
Proof state after:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
⊢ digit b (n % b ^ p) i = digit b n i
Theorem: Nat.toDigits_modulo
Proof state before:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
⊢ digit b (n % b ^ p) i = digit b n i
Tactic:
unfold digit
Proof state after:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
⊢ n % b ^ p / b ^ i % b = n / b ^ i % b
Theorem: Nat.toDigits_modulo
Proof state before:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
⊢ n % b ^ p / b ^ i % b = n / b ^ i % b
Tactic:
have hpeq := Nat.sub_add_cancel (le_of_lt P)
Proof state after:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ n % b ^ p / b ^ i % b = n / b ^ i % b
Theorem: Nat.toDigits_modulo
Proof state before:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ n % b ^ p / b ^ i % b = n / b ^ i % b
Tactic:
conv => left; left; left; rw [← hpeq, pow_add]
Proof state after:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ n % (b ^ (p - i) * b ^ i) / b ^ i % b = n / b ^ i % b
Theorem: Nat.toDigits_modulo
Proof state before:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ n % (b ^ (p - i) * b ^ i) / b ^ i % b = n / b ^ i % b
Tactic:
rw [Nat.mod_mul_left_div_self, Nat.mod_mod_of_dvd]
Proof state after:
case e_n.h
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ b ∣ b ^ (p - i)
Theorem: Nat.toDigits_modulo
Proof state before:
case e_n.h
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ b ∣ b ^ (p - i)
Tactic:
apply dvd_pow
Proof state after:
case e_n.h.hxy
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ b ∣ b

case e_n.h.x
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ p - i ≠ 0
Theorem: Nat.toDigits_modulo
Proof state before:
case e_n.h.hxy
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ b ∣ b

case e_n.h.x
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ p - i ≠ 0
Tactic:
. apply dvd_refl
Proof state after:
case e_n.h.x
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ p - i ≠ 0
Theorem: Nat.toDigits_modulo
Proof state before:
case e_n.h.x
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ p - i ≠ 0
Tactic:
. simp only [min_le_iff, ge_iff_le, tsub_le_iff_right, le_min_iff, _root_.zero_le, nonpos_iff_eq_zero, ne_eq,
    tsub_eq_zero_iff_le, not_and, not_le, P, implies_true]
Proof state after:
no goals
Theorem: Nat.toDigits_modulo
Proof state before:
b n p i : ℕ
P : i < p
Q : b > 1
⊢ b > 1
Tactic:
exact Q
Proof state after:
no goals
Theorem: List.getD_ext
Proof state before:
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
⊢ a = b
Tactic:
apply List.ext
Proof state after:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
⊢ ∀ (n : ℕ), get? a n = get? b n
Theorem: List.getD_ext
Proof state before:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
⊢ ∀ (n : ℕ), get? a n = get? b n
Tactic:
intro n
Proof state after:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
⊢ get? a n = get? b n
Theorem: List.getD_ext
Proof state before:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
⊢ get? a n = get? b n
Tactic:
have h:= Q n
Proof state after:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : getD a n d = getD b n d
⊢ get? a n = get? b n
Theorem: List.getD_ext
Proof state before:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : getD a n d = getD b n d
⊢ get? a n = get? b n
Tactic:
unfold getD at h
Proof state after:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
⊢ get? a n = get? b n
Theorem: List.getD_ext
Proof state before:
case a
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
⊢ get? a n = get? b n
Tactic:
cases hlt: decide (n < List.length a) with
| true => 
  simp only [decide_eq_true_eq] at hlt
  have hltb: n < length b := by rw [← P]; exact hlt
  simp_all only [zero_le, ge_iff_le, nonpos_iff_eq_zero, hltb, get?_eq_get, Option.getD_some, gt_iff_lt, P] 
| false =>
   simp only [decide_eq_false_iff_not, not_lt] at hlt
   have hltb: n ≥ length b := by rw [← P]; exact hlt
   simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, hlt, List.get?_eq_none.2, hltb]
Proof state after:
no goals
Theorem: List.getD_ext
Proof state before:
case a.true
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : decide (n < length a) = true
⊢ get? a n = get? b n
Tactic:
simp only [decide_eq_true_eq] at hlt
Proof state after:
case a.true
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : n < length a
⊢ get? a n = get? b n
Theorem: List.getD_ext
Proof state before:
case a.true
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : n < length a
⊢ get? a n = get? b n
Tactic:
have hltb: n < length b := by rw [← P]; exact hlt
Proof state after:
case a.true
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : n < length a
hltb : n < length b
⊢ get? a n = get? b n
Theorem: List.getD_ext
Proof state before:
case a.true
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : n < length a
hltb : n < length b
⊢ get? a n = get? b n
Tactic:
simp_all only [zero_le, ge_iff_le, nonpos_iff_eq_zero, hltb, get?_eq_get, Option.getD_some, gt_iff_lt, P]
Proof state after:
no goals
Theorem: List.getD_ext
Proof state before:
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : n < length a
⊢ n < length b
Tactic:
rw [← P]
Proof state after:
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : n < length a
⊢ n < length a
Theorem: List.getD_ext
Proof state before:
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : n < length a
⊢ n < length a
Tactic:
exact hlt
Proof state after:
no goals
Theorem: List.getD_ext
Proof state before:
case a.false
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : decide (n < length a) = false
⊢ get? a n = get? b n
Tactic:
simp only [decide_eq_false_iff_not, not_lt] at hlt
Proof state after:
case a.false
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : length a ≤ n
⊢ get? a n = get? b n
Theorem: List.getD_ext
Proof state before:
case a.false
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : length a ≤ n
⊢ get? a n = get? b n
Tactic:
have hltb: n ≥ length b := by rw [← P]; exact hlt
Proof state after:
case a.false
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : length a ≤ n
hltb : n ≥ length b
⊢ get? a n = get? b n
Theorem: List.getD_ext
Proof state before:
case a.false
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : length a ≤ n
hltb : n ≥ length b
⊢ get? a n = get? b n
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, hlt, List.get?_eq_none.2, hltb]
Proof state after:
no goals
Theorem: List.getD_ext
Proof state before:
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : length a ≤ n
⊢ n ≥ length b
Tactic:
rw [← P]
Proof state after:
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : length a ≤ n
⊢ n ≥ length a
Theorem: List.getD_ext
Proof state before:
α✝ : Type u_1
a b : List α✝
d : α✝
P : length a = length b
Q : ∀ (i : ℕ), getD a i d = getD b i d
n : ℕ
h : Option.getD (get? a n) d = Option.getD (get? b n) d
hlt : length a ≤ n
⊢ n ≥ length a
Tactic:
exact hlt
Proof state after:
no goals
Theorem: List.getD_reverse
Proof state before:
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ getD (reverse l) i d = l[length l - 1 - i]
Tactic:
unfold List.getD
Proof state after:
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ Option.getD (get? (reverse l) i) d = l[length l - 1 - i]
Theorem: List.getD_reverse
Proof state before:
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ Option.getD (get? (reverse l) i) d = l[length l - 1 - i]
Tactic:
rw [List.get?_reverse, List.get?_eq_get]
Proof state after:
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ Option.getD (some (get l { val := length l - 1 - i, isLt := ?m.112638 })) d = l[length l - 1 - i]

i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ length l - 1 - i < length l

case h
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ i < length l
Theorem: List.getD_reverse
Proof state before:
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ Option.getD (some (get l { val := length l - 1 - i, isLt := ?m.112638 })) d = l[length l - 1 - i]

i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ length l - 1 - i < length l

case h
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ i < length l
Tactic:
simp only [tsub_le_iff_right, ge_iff_le, Option.getD_some, getElem_eq_get]
Proof state after:
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ length l - 1 - i < length l

case h
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ i < length l
Theorem: List.getD_reverse
Proof state before:
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ length l - 1 - i < length l

case h
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ i < length l
Tactic:
. exact Nat.sub_one_sub_lt P
Proof state after:
case h
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ i < length l
Theorem: List.getD_reverse
Proof state before:
case h
i : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < length l
⊢ i < length l
Tactic:
. exact P
Proof state after:
no goals
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
a b : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
Q : List.length a ≤ List.length b
⊢ toNatΔ a = toNatΔ b
Tactic:
induction b with
| nil =>
  simp only [List.length_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, List.length_eq_zero] at Q
  simp only [Q]
| cons hd tl ih =>
  cases heq: decide (List.length a = List.length (hd::tl))
  case true => 
    simp only [decide_eq_true_eq] at heq
    have h: a = (hd::tl) := by 
      apply List.getD_ext heq (d:='0')
      intro n
      cases hlt: decide (n < List.length a) with
      | true => 
        simp only [decide_eq_true_eq] at hlt
        have hblt: n < List.length (hd::tl) := by simp_all only [tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, tsub_eq_zero_iff_le, heq]
        simp only [gt_iff_lt, hlt, List.getD_eq_get, List.getElem_eq_get, hblt]
        have Q:= P (List.length a -1 - n)
        conv at Q => right; rw [heq]
        rw [ List.getD_reverse (Nat.sub_one_sub_lt hlt),
          List.getD_reverse (Nat.sub_one_sub_lt hblt)] at Q
        simp only [tsub_le_iff_right, ge_iff_le, Nat.sub_sub_self (Nat.le_pred_of_lt hlt), List.getElem_eq_get,
          Nat.sub_sub_self (Nat.le_pred_of_lt hblt)] at Q
        apply Q
        
      | false => 
        simp only [decide_eq_false_iff_not, not_lt] at hlt
        have hblt: n ≥ List.length (hd::tl) := by simp_all only [tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, tsub_eq_zero_iff_le, heq]
        simp only [List.getD_eq_get?, zero_le, ge_iff_le, nonpos_iff_eq_zero, hlt, List.get?_eq_none.2,
          Option.getD_none, hblt]
    simp only [h]
  case false =>
    simp only [decide_eq_false_iff_not] at heq
    have R := P (List.length tl)
    rw [List.getD_eq_default] at R
    . rw [List.getD_reverse] at R
      . conv => right; unfold toNatΔ toNatAux
        simp only [List.length_cons, Nat.succ_sub_succ_eq_sub, tsub_zero, ge_iff_le, zero_le, nonpos_iff_eq_zero,
          Nat.sub_self, le_refl, tsub_eq_zero_of_le, List.getElem_eq_get, List.get] at R
        rw [String.toNatAux_accumulates, ← toNatΔ, ← R]
        simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_mul, Nat.sub_self, le_refl, tsub_eq_zero_of_le,
          add_zero]
        apply ih
        . intro i
          rw [P, List.reverse_cons]
          cases h: decide ( i < List.length tl) with
          | true =>
            simp only [decide_eq_true_eq] at h
            rw [List.getD_append]
            simp only [List.length_reverse, h]
          | false =>
            simp only [decide_eq_false_iff_not, not_lt] at h
            rw [List.getD_append_right, ←R, List.getD_singleton_default_eq, List.getD_eq_default] <;> 
              simp only [List.length_reverse, ge_iff_le, h]
        . apply Nat.le_of_lt_succ
          apply Nat.lt_of_le_of_ne Q heq
      . simp only [List.length_cons, Nat.lt_succ_self]
    . simp only [List.length_cons] at Q
      simp only [List.length_reverse, ge_iff_le]
      apply Nat.le_of_lt_succ
      apply Nat.lt_of_le_of_ne Q heq
Proof state after:
no goals
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case nil
a : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse []) i (Char.ofNat 48)
Q : List.length a ≤ List.length []
⊢ toNatΔ a = toNatΔ []
Tactic:
simp only [List.length_nil, zero_le, ge_iff_le, nonpos_iff_eq_zero, List.length_eq_zero] at Q
Proof state after:
case nil
a : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse []) i (Char.ofNat 48)
Q : a = []
⊢ toNatΔ a = toNatΔ []
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case nil
a : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse []) i (Char.ofNat 48)
Q : a = []
⊢ toNatΔ a = toNatΔ []
Tactic:
simp only [Q]
Proof state after:
no goals
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case cons
a : List Char
hd : Char
tl : List Char
ih :
  (∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse tl) i (Char.ofNat 48)) →
    List.length a ≤ List.length tl → toNatΔ a = toNatΔ tl
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse (hd :: tl)) i (Char.ofNat 48)
Q : List.length a ≤ List.length (hd :: tl)
⊢ toNatΔ a = toNatΔ (hd :: tl)
Tactic:
cases heq: decide (List.length a = List.length (hd::tl))
Proof state after:
case cons.false
a : List Char
hd : Char
tl : List Char
ih :
  (∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse tl) i (Char.ofNat 48)) →
    List.length a ≤ List.length tl → toNatΔ a = toNatΔ tl
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse (hd :: tl)) i (Char.ofNat 48)
Q : List.length a ≤ List.length (hd :: tl)
heq : decide (List.length a = List.length (hd :: tl)) = false
⊢ toNatΔ a = toNatΔ (hd :: tl)

case cons.true
a : List Char
hd : Char
tl : List Char
ih :
  (∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse tl) i (Char.ofNat 48)) →
    List.length a ≤ List.length tl → toNatΔ a = toNatΔ tl
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse (hd :: tl)) i (Char.ofNat 48)
Q : List.length a ≤ List.length (hd :: tl)
heq : decide (List.length a = List.length (hd :: tl)) = true
⊢ toNatΔ a = toNatΔ (hd :: tl)
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
a : List Char
hd : Char
tl : List Char
ih :
  (∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse tl) i (Char.ofNat 48)) →
    List.length a ≤ List.length tl → toNatΔ a = toNatΔ tl
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse (hd :: tl)) i (Char.ofNat 48)
Q : List.length a ≤ List.length (hd :: tl)
heq : decide (List.length a = List.length (hd :: tl)) = true
⊢ toNatΔ a = toNatΔ (hd :: tl)
Tactic:
case true => 
  simp only [decide_eq_true_eq] at heq
  have h: a = (hd::tl) := by 
    apply List.getD_ext heq (d:='0')
    intro n
    cases hlt: decide (n < List.length a) with
    | true => 
      simp only [decide_eq_true_eq] at hlt
      have hblt: n < List.length (hd::tl) := by simp_all only [tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, tsub_eq_zero_iff_le, heq]
      simp only [gt_iff_lt, hlt, List.getD_eq_get, List.getElem_eq_get, hblt]
      have Q:= P (List.length a -1 - n)
      conv at Q => right; rw [heq]
      rw [ List.getD_reverse (Nat.sub_one_sub_lt hlt),
        List.getD_reverse (Nat.sub_one_sub_lt hblt)] at Q
      simp only [tsub_le_iff_right, ge_iff_le, Nat.sub_sub_self (Nat.le_pred_of_lt hlt), List.getElem_eq_get,
        Nat.sub_sub_self (Nat.le_pred_of_lt hblt)] at Q
      apply Q
      
    | false => 
      simp only [decide_eq_false_iff_not, not_lt] at hlt
      have hblt: n ≥ List.length (hd::tl) := by simp_all only [tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, tsub_eq_zero_iff_le, heq]
      simp only [List.getD_eq_get?, zero_le, ge_iff_le, nonpos_iff_eq_zero, hlt, List.get?_eq_none.2,
        Option.getD_none, hblt]
  simp only [h]
Proof state after:
no goals