internlm/Lean-Github huggingface dataset:
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)) = false
⊢ toNatΔ a = toNatΔ (hd :: tl)
Tactic:
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:
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:
simp only [decide_eq_true_eq] at heq
Proof state after:
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 : List.length a = List.length (hd :: tl)
⊢ 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 : List.length a = List.length (hd :: tl)
⊢ toNatΔ a = toNatΔ (hd :: tl)
Tactic:
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]
Proof state after:
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 : List.length a = List.length (hd :: tl)
h : a = hd :: tl
⊢ 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 : List.length a = List.length (hd :: tl)
h : a = hd :: tl
⊢ toNatΔ a = toNatΔ (hd :: tl)
Tactic:
simp only [h]
Proof state after:
no goals
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 : List.length a = List.length (hd :: tl)
⊢ a = hd :: tl
Tactic:
apply List.getD_ext heq (d:='0')
Proof state after:
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 : List.length a = List.length (hd :: tl)
⊢ ∀ (i : ℕ), List.getD a i (Char.ofNat 48) = List.getD (hd :: tl) i (Char.ofNat 48)
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 : List.length a = List.length (hd :: tl)
⊢ ∀ (i : ℕ), List.getD a i (Char.ofNat 48) = List.getD (hd :: tl) i (Char.ofNat 48)
Tactic:
intro n
Proof state after:
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 : List.length a = List.length (hd :: tl)
n : ℕ
⊢ List.getD a n (Char.ofNat 48) = List.getD (hd :: tl) n (Char.ofNat 48)
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 : List.length a = List.length (hd :: tl)
n : ℕ
⊢ List.getD a n (Char.ofNat 48) = List.getD (hd :: tl) n (Char.ofNat 48)
Tactic:
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]
Proof state after:
no goals
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : decide (n < List.length a) = true
⊢ List.getD a n (Char.ofNat 48) = List.getD (hd :: tl) n (Char.ofNat 48)
Tactic:
simp only [decide_eq_true_eq] at hlt
Proof state after:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : n < List.length a
⊢ List.getD a n (Char.ofNat 48) = List.getD (hd :: tl) n (Char.ofNat 48)
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : n < List.length a
⊢ List.getD a n (Char.ofNat 48) = List.getD (hd :: tl) n (Char.ofNat 48)
Tactic:
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]
Proof state after:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : n < List.length a
hblt : n < List.length (hd :: tl)
⊢ List.getD a n (Char.ofNat 48) = List.getD (hd :: tl) n (Char.ofNat 48)
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : n < List.length a
hblt : n < List.length (hd :: tl)
⊢ List.getD a n (Char.ofNat 48) = List.getD (hd :: tl) n (Char.ofNat 48)
Tactic:
simp only [gt_iff_lt, hlt, List.getD_eq_get, List.getElem_eq_get, hblt]
Proof state after:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : n < List.length a
hblt : n < List.length (hd :: tl)
⊢ List.get a { val := n, isLt := (_ : List.length a > n) } =
    List.get (hd :: tl) { val := n, isLt := (_ : List.length (hd :: tl) > n) }
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : n < List.length a
hblt : n < List.length (hd :: tl)
⊢ List.get a { val := n, isLt := (_ : List.length a > n) } =
    List.get (hd :: tl) { val := n, isLt := (_ : List.length (hd :: tl) > n) }
Tactic:
have Q:= P (List.length a -1 - n)
Proof state after:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : n < List.length a
hblt : n < List.length (hd :: tl)
Q :
  List.getD (List.reverse a) (List.length a - 1 - n) (Char.ofNat 48) =
    List.getD (List.reverse (hd :: tl)) (List.length a - 1 - n) (Char.ofNat 48)
⊢ List.get a { val := n, isLt := (_ : List.length a > n) } =
    List.get (hd :: tl) { val := n, isLt := (_ : List.length (hd :: tl) > n) }
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : n < List.length a
hblt : n < List.length (hd :: tl)
Q :
  List.getD (List.reverse a) (List.length a - 1 - n) (Char.ofNat 48) =
    List.getD (List.reverse (hd :: tl)) (List.length a - 1 - n) (Char.ofNat 48)
⊢ List.get a { val := n, isLt := (_ : List.length a > n) } =
    List.get (hd :: tl) { val := n, isLt := (_ : List.length (hd :: tl) > n) }
Tactic:
conv at Q => right; rw [heq]
Proof state after:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : n < List.length a
hblt : n < List.length (hd :: tl)
Q :
  List.getD (List.reverse a) (List.length a - 1 - n) (Char.ofNat 48) =
    List.getD (List.reverse (hd :: tl)) (List.length (hd :: tl) - 1 - n) (Char.ofNat 48)
⊢ List.get a { val := n, isLt := (_ : List.length a > n) } =
    List.get (hd :: tl) { val := n, isLt := (_ : List.length (hd :: tl) > n) }
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : n < List.length a
hblt : n < List.length (hd :: tl)
Q :
  List.getD (List.reverse a) (List.length a - 1 - n) (Char.ofNat 48) =
    List.getD (List.reverse (hd :: tl)) (List.length (hd :: tl) - 1 - n) (Char.ofNat 48)
⊢ List.get a { val := n, isLt := (_ : List.length a > n) } =
    List.get (hd :: tl) { val := n, isLt := (_ : List.length (hd :: tl) > n) }
Tactic:
rw [ List.getD_reverse (Nat.sub_one_sub_lt hlt),
  List.getD_reverse (Nat.sub_one_sub_lt hblt)] at Q
Proof state after:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : n < List.length a
hblt : n < List.length (hd :: tl)
Q :
  a[List.length a - 1 - (List.length a - 1 - n)] =
    (hd :: tl)[List.length (hd :: tl) - 1 - (List.length (hd :: tl) - 1 - n)]
⊢ List.get a { val := n, isLt := (_ : List.length a > n) } =
    List.get (hd :: tl) { val := n, isLt := (_ : List.length (hd :: tl) > n) }
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : n < List.length a
hblt : n < List.length (hd :: tl)
Q :
  a[List.length a - 1 - (List.length a - 1 - n)] =
    (hd :: tl)[List.length (hd :: tl) - 1 - (List.length (hd :: tl) - 1 - n)]
⊢ List.get a { val := n, isLt := (_ : List.length a > n) } =
    List.get (hd :: tl) { val := n, isLt := (_ : List.length (hd :: tl) > n) }
Tactic:
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
Proof state after:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : n < List.length a
hblt : n < List.length (hd :: tl)
Q :
  List.get a { val := n, isLt := (_ : (fun as i => i < List.length as) a n) } =
    List.get (hd :: tl) { val := n, isLt := (_ : (fun as i => i < List.length as) (hd :: tl) n) }
⊢ List.get a { val := n, isLt := (_ : List.length a > n) } =
    List.get (hd :: tl) { val := n, isLt := (_ : List.length (hd :: tl) > n) }
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : n < List.length a
hblt : n < List.length (hd :: tl)
Q :
  List.get a { val := n, isLt := (_ : (fun as i => i < List.length as) a n) } =
    List.get (hd :: tl) { val := n, isLt := (_ : (fun as i => i < List.length as) (hd :: tl) n) }
⊢ List.get a { val := n, isLt := (_ : List.length a > n) } =
    List.get (hd :: tl) { val := n, isLt := (_ : List.length (hd :: tl) > n) }
Tactic:
apply Q
Proof state after:
no goals
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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : n < List.length a
⊢ n < List.length (hd :: tl)
Tactic:
simp_all only [tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, tsub_eq_zero_iff_le, heq]
Proof state after:
no goals
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : decide (n < List.length a) = false
⊢ List.getD a n (Char.ofNat 48) = List.getD (hd :: tl) n (Char.ofNat 48)
Tactic:
simp only [decide_eq_false_iff_not, not_lt] at hlt
Proof state after:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : List.length a ≤ n
⊢ List.getD a n (Char.ofNat 48) = List.getD (hd :: tl) n (Char.ofNat 48)
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : List.length a ≤ n
⊢ List.getD a n (Char.ofNat 48) = List.getD (hd :: tl) n (Char.ofNat 48)
Tactic:
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]
Proof state after:
case 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 : List.length a = List.length (hd :: tl)
n : ℕ
hlt : List.length a ≤ n
hblt : n ≥ List.length (hd :: tl)
⊢ List.getD a n (Char.ofNat 48) = List.getD (hd :: tl) n (Char.ofNat 48)