Theorem: String.toNatΔ_eq_of_rev_get_eq (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)
⊢ 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
State after:
no goals

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

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

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

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

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

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

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

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