internlm/Lean-Github huggingface dataset:
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
hblt : n ≥ List.length (hd :: tl)
⊢ List.getD a n (Char.ofNat 48) = List.getD (hd :: tl) n (Char.ofNat 48)
Tactic:
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:
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
⊢ 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:
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:
simp only [decide_eq_false_iff_not] 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 R := P (List.length tl)
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)
R :
  List.getD (List.reverse a) (List.length tl) (Char.ofNat 48) =
    List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
⊢ 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)
R :
  List.getD (List.reverse a) (List.length tl) (Char.ofNat 48) =
    List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
⊢ toNatΔ a = toNatΔ (hd :: tl)
Tactic:
rw [List.getD_eq_default] at R
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)
R : Char.ofNat 48 = List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
⊢ toNatΔ a = toNatΔ (hd :: tl)

case hn
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)
R :
  List.getD (List.reverse a) (List.length tl) (Char.ofNat 48) =
    List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
⊢ List.length (List.reverse a) ≤ List.length 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)
R : Char.ofNat 48 = List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
⊢ toNatΔ a = toNatΔ (hd :: tl)

case hn
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)
R :
  List.getD (List.reverse a) (List.length tl) (Char.ofNat 48) =
    List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
⊢ List.length (List.reverse a) ≤ List.length tl
Tactic:
. 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]
Proof state after:
case hn
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)
R :
  List.getD (List.reverse a) (List.length tl) (Char.ofNat 48) =
    List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
⊢ List.length (List.reverse a) ≤ List.length tl
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case hn
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)
R :
  List.getD (List.reverse a) (List.length tl) (Char.ofNat 48) =
    List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
⊢ List.length (List.reverse a) ≤ List.length tl
Tactic:
. 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 P.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)
R✝ : Char.ofNat 48 = List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
R : Char.ofNat 48 = hd
i : ℕ
h : decide (i < List.length tl) = true
⊢ List.getD (List.reverse tl ++ [hd]) i (Char.ofNat 48) = List.getD (List.reverse tl) i (Char.ofNat 48)
Tactic:
simp only [decide_eq_true_eq] at h
Proof state after:
case P.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)
R✝ : Char.ofNat 48 = List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
R : Char.ofNat 48 = hd
i : ℕ
h : i < List.length tl
⊢ List.getD (List.reverse tl ++ [hd]) i (Char.ofNat 48) = List.getD (List.reverse tl) i (Char.ofNat 48)
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case P.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)
R✝ : Char.ofNat 48 = List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
R : Char.ofNat 48 = hd
i : ℕ
h : i < List.length tl
⊢ List.getD (List.reverse tl ++ [hd]) i (Char.ofNat 48) = List.getD (List.reverse tl) i (Char.ofNat 48)
Tactic:
rw [List.getD_append]
Proof state after:
case P.true.h
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)
R✝ : Char.ofNat 48 = List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
R : Char.ofNat 48 = hd
i : ℕ
h : i < List.length tl
⊢ i < List.length (List.reverse tl)
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case P.true.h
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)
R✝ : Char.ofNat 48 = List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
R : Char.ofNat 48 = hd
i : ℕ
h : i < List.length tl
⊢ i < List.length (List.reverse tl)
Tactic:
simp only [List.length_reverse, h]
Proof state after:
no goals
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case P.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)
R✝ : Char.ofNat 48 = List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
R : Char.ofNat 48 = hd
i : ℕ
h : decide (i < List.length tl) = false
⊢ List.getD (List.reverse tl ++ [hd]) i (Char.ofNat 48) = List.getD (List.reverse tl) i (Char.ofNat 48)
Tactic:
simp only [decide_eq_false_iff_not, not_lt] at h
Proof state after:
case P.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)
R✝ : Char.ofNat 48 = List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
R : Char.ofNat 48 = hd
i : ℕ
h : List.length tl ≤ i
⊢ List.getD (List.reverse tl ++ [hd]) i (Char.ofNat 48) = List.getD (List.reverse tl) i (Char.ofNat 48)
Theorem: String.toNatΔ_eq_of_rev_get_eq_aux
Proof state before:
case P.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)
R✝ : Char.ofNat 48 = List.getD (List.reverse (hd :: tl)) (List.length tl) (Char.ofNat 48)
R : Char.ofNat 48 = hd
i : ℕ
h : List.length tl ≤ i
⊢ List.getD (List.reverse tl ++ [hd]) i (Char.ofNat 48) = List.getD (List.reverse tl) i (Char.ofNat 48)
Tactic:
rw [List.getD_append_right, ←R, List.getD_singleton_default_eq, List.getD_eq_default] <;> 
  simp only [List.length_reverse, ge_iff_le, h]
Proof state after:
no goals
Theorem: String.toNatΔ_eq_of_rev_get_eq
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)
⊢ toNatΔ a = toNatΔ b
Tactic:
cases h: decide (List.length a ≤ List.length b) with
| true =>
  simp only [decide_eq_true_eq] at h
  apply String.toNatΔ_eq_of_rev_get_eq_aux P h
| false =>
  simp only [decide_eq_false_iff_not, not_le] at h
  apply Eq.symm
  apply (String.toNatΔ_eq_of_rev_get_eq_aux (a:=b) (b:=a) (Q:=le_of_lt h))
  intro i
  apply Eq.symm
  apply P
Proof state after:
no goals
Theorem: String.toNatΔ_eq_of_rev_get_eq
Proof state before:
case true
a b : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
h : decide (List.length a ≤ List.length b) = true
⊢ toNatΔ a = toNatΔ b
Tactic:
simp only [decide_eq_true_eq] at h
Proof state after:
case true
a b : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
h : List.length a ≤ List.length b
⊢ toNatΔ a = toNatΔ b
Theorem: String.toNatΔ_eq_of_rev_get_eq
Proof state before:
case true
a b : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
h : List.length a ≤ List.length b
⊢ toNatΔ a = toNatΔ b
Tactic:
apply String.toNatΔ_eq_of_rev_get_eq_aux P h
Proof state after:
no goals
Theorem: String.toNatΔ_eq_of_rev_get_eq
Proof state before:
case false
a b : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
h : decide (List.length a ≤ List.length b) = false
⊢ toNatΔ a = toNatΔ b
Tactic:
simp only [decide_eq_false_iff_not, not_le] at h
Proof state after:
case false
a b : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
h : List.length b < List.length a
⊢ toNatΔ a = toNatΔ b
Theorem: String.toNatΔ_eq_of_rev_get_eq
Proof state before:
case false
a b : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
h : List.length b < List.length a
⊢ toNatΔ a = toNatΔ b
Tactic:
apply Eq.symm
Proof state after:
case false.h
a b : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
h : List.length b < List.length a
⊢ toNatΔ b = toNatΔ a
Theorem: String.toNatΔ_eq_of_rev_get_eq
Proof state before:
case false.h
a b : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
h : List.length b < List.length a
⊢ toNatΔ b = toNatΔ a
Tactic:
apply (String.toNatΔ_eq_of_rev_get_eq_aux (a:=b) (b:=a) (Q:=le_of_lt h))
Proof state after:
case false.h
a b : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
h : List.length b < List.length a
⊢ ∀ (i : ℕ), List.getD (List.reverse b) i (Char.ofNat 48) = List.getD (List.reverse a) i (Char.ofNat 48)
Theorem: String.toNatΔ_eq_of_rev_get_eq
Proof state before:
case false.h
a b : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
h : List.length b < List.length a
⊢ ∀ (i : ℕ), List.getD (List.reverse b) i (Char.ofNat 48) = List.getD (List.reverse a) i (Char.ofNat 48)
Tactic:
intro i
Proof state after:
case false.h
a b : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
h : List.length b < List.length a
i : ℕ
⊢ List.getD (List.reverse b) i (Char.ofNat 48) = List.getD (List.reverse a) i (Char.ofNat 48)
Theorem: String.toNatΔ_eq_of_rev_get_eq
Proof state before:
case false.h
a b : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
h : List.length b < List.length a
i : ℕ
⊢ List.getD (List.reverse b) i (Char.ofNat 48) = List.getD (List.reverse a) i (Char.ofNat 48)
Tactic:
apply Eq.symm
Proof state after:
case false.h.h
a b : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
h : List.length b < List.length a
i : ℕ
⊢ List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
Theorem: String.toNatΔ_eq_of_rev_get_eq
Proof state before:
case false.h.h
a b : List Char
P : ∀ (i : ℕ), List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
h : List.length b < List.length a
i : ℕ
⊢ List.getD (List.reverse a) i (Char.ofNat 48) = List.getD (List.reverse b) i (Char.ofNat 48)
Tactic:
apply P
Proof state after:
no goals
Theorem: List.getD_take
Proof state before:
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
⊢ getD (take n l) i d = getD l i d
Tactic:
conv => right; rw [← List.take_append_drop n l]
Proof state after:
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d
Theorem: List.getD_take
Proof state before:
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d
Tactic:
cases h: decide (i < List.length l) with
| true =>
  simp only [decide_eq_true_eq] at h
  rw [List.getD_append]
  simp only [length_take, min_le_iff, ge_iff_le, lt_min_iff]
  exact ⟨P,h⟩
| false =>
  simp only [decide_eq_false_iff_not, not_lt] at h
  rw [List.getD_eq_default, List.getD_eq_default]
  . simp only [take_append_drop, ge_iff_le, h]
  . simp only [length_take, min_le_iff, ge_iff_le, h, or_true]
Proof state after:
no goals
Theorem: List.getD_take
Proof state before:
case true
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : decide (i < length l) = true
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d
Tactic:
simp only [decide_eq_true_eq] at h
Proof state after:
case true
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : i < length l
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d
Theorem: List.getD_take
Proof state before:
case true
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : i < length l
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d
Tactic:
rw [List.getD_append]
Proof state after:
case true.h
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : i < length l
⊢ i < length (take n l)
Theorem: List.getD_take
Proof state before:
case true.h
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : i < length l
⊢ i < length (take n l)
Tactic:
simp only [length_take, min_le_iff, ge_iff_le, lt_min_iff]
Proof state after:
case true.h
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : i < length l
⊢ i < n ∧ i < length l
Theorem: List.getD_take
Proof state before:
case true.h
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : i < length l
⊢ i < n ∧ i < length l
Tactic:
exact ⟨P,h⟩
Proof state after:
no goals
Theorem: List.getD_take
Proof state before:
case false
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : decide (i < length l) = false
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d
Tactic:
simp only [decide_eq_false_iff_not, not_lt] at h
Proof state after:
case false
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d
Theorem: List.getD_take
Proof state before:
case false
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ getD (take n l) i d = getD (take n l ++ drop n l) i d
Tactic:
rw [List.getD_eq_default, List.getD_eq_default]
Proof state after:
case false.hn
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ length (take n l ++ drop n l) ≤ i

case false.hn
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ length (take n l) ≤ i
Theorem: List.getD_take
Proof state before:
case false.hn
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ length (take n l ++ drop n l) ≤ i

case false.hn
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ length (take n l) ≤ i
Tactic:
. simp only [take_append_drop, ge_iff_le, h]
Proof state after:
case false.hn
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ length (take n l) ≤ i
Theorem: List.getD_take
Proof state before:
case false.hn
i n : ℕ
α✝ : Type u_1
l : List α✝
d : α✝
P : i < n
h : length l ≤ i
⊢ length (take n l) ≤ i
Tactic:
. simp only [length_take, min_le_iff, ge_iff_le, h, or_true]
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits_tail
Proof 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
Proof 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)