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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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