Theorem: String.toIntΔ_inv_IntreprΔ (One.lean)

State before:
i : ℤ
⊢ toIntΔ (Int.reprΔ i) = i
Tactic:
unfold toIntΔ Int.reprΔ
State after:
i : ℤ
⊢ (match
      match i with
      | Int.ofNat m => Nat.toDigits 10 m
      | Int.negSucc m => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m) with
    | [] => 0
    | h :: tail => if h = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (h :: tail))) =
    i

State before:
i : ℤ
⊢ (match
      match i with
      | Int.ofNat m => Nat.toDigits 10 m
      | Int.negSucc m => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m) with
    | [] => 0
    | h :: tail => if h = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (h :: tail))) =
    i
Tactic:
cases i with
| ofNat n =>
  simp only [Int.ofNat_eq_coe]
  split
  case h_1 s heq =>
    simp only [Nat.toDigits_ne_nil
  ] at heq
  case h_2 head tail heq =>
    split
    case inl h =>
      have h₂: (List.all (head::tail) Char.isDigit == true) = true := by
        rw [← heq]
        apply Nat.toDigits_digits <;> decide
      simp at h₂
      have ⟨ h₃, _⟩ :=h₂
      simp only [h] at h₃
    . simp only [← heq, toNatΔ_inv_NattoDigits]
| negSucc n =>
  simp only [List.singleton_append, toNatΔ_inv_NattoDigits, Nat.cast_succ, neg_add_rev, ite_true,
    Int.negSucc_eq]
State after:
no goals

State before:
case ofNat
n : ℕ
⊢ (match
      match Int.ofNat n with
      | Int.ofNat m => Nat.toDigits 10 m
      | Int.negSucc m => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m) with
    | [] => 0
    | h :: tail => if h = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (h :: tail))) =
    Int.ofNat n
Tactic:
simp only [Int.ofNat_eq_coe]
State after:
case ofNat
n : ℕ
⊢ (match Nat.toDigits 10 n with
    | [] => 0
    | h :: tail => if h = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (h :: tail))) =
    ↑n

State before:
case ofNat
n : ℕ
⊢ (match Nat.toDigits 10 n with
    | [] => 0
    | h :: tail => if h = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (h :: tail))) =
    ↑n
Tactic:
split
State after:
case ofNat.h_1
n : ℕ
s✝ : List Char
heq✝ : Nat.toDigits 10 n = []
⊢ 0 = ↑n

case ofNat.h_2
n : ℕ
s✝ : List Char
head✝ : Char
tail✝ : List Char
heq✝ : Nat.toDigits 10 n = head✝ :: tail✝
⊢ (if head✝ = Char.ofNat 45 then -↑(toNatΔ tail✝) else ↑(toNatΔ (head✝ :: tail✝))) = ↑n

State before:
n : ℕ
s : List Char
heq : Nat.toDigits 10 n = []
⊢ 0 = ↑n
Tactic:
case h_1 s heq =>
  simp only [Nat.toDigits_ne_nil
] at heq
State after:
no goals

State before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
⊢ (if head = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (head :: tail))) = ↑n
Tactic:
case h_2 head tail heq =>
  split
  case inl h =>
    have h₂: (List.all (head::tail) Char.isDigit == true) = true := by
      rw [← heq]
      apply Nat.toDigits_digits <;> decide
    simp at h₂
    have ⟨ h₃, _⟩ :=h₂
    simp only [h] at h₃
  . simp only [← heq, toNatΔ_inv_NattoDigits]
State after:
no goals

State before:
n : ℕ
s : List Char
heq : Nat.toDigits 10 n = []
⊢ 0 = ↑n
Tactic:
simp only [Nat.toDigits_ne_nil
] at heq
State after:
no goals

State before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
⊢ (if head = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (head :: tail))) = ↑n
Tactic:
split
State after:
case inl
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h✝ : head = Char.ofNat 45
⊢ -↑(toNatΔ tail) = ↑n

case inr
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h✝ : ¬head = Char.ofNat 45
⊢ ↑(toNatΔ (head :: tail)) = ↑n

State before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
⊢ -↑(toNatΔ tail) = ↑n
Tactic:
case inl h =>
  have h₂: (List.all (head::tail) Char.isDigit == true) = true := by
    rw [← heq]
    apply Nat.toDigits_digits <;> decide
  simp at h₂
  have ⟨ h₃, _⟩ :=h₂
  simp only [h] at h₃
State after:
no goals

State before:
case inr
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h✝ : ¬head = Char.ofNat 45
⊢ ↑(toNatΔ (head :: tail)) = ↑n
Tactic:
. simp only [← heq, toNatΔ_inv_NattoDigits]
State after:
no goals

State before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
⊢ -↑(toNatΔ tail) = ↑n
Tactic:
have h₂: (List.all (head::tail) Char.isDigit == true) = true := by
  rw [← heq]
  apply Nat.toDigits_digits <;> decide
State after:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
h₂ : (List.all (head :: tail) Char.isDigit == true) = true
⊢ -↑(toNatΔ tail) = ↑n

State before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
h₂ : (List.all (head :: tail) Char.isDigit == true) = true
⊢ -↑(toNatΔ tail) = ↑n
Tactic:
simp at h₂
State after:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
h₂ : Char.isDigit head = true ∧ ∀ (x : Char), x ∈ tail → Char.isDigit x = true
⊢ -↑(toNatΔ tail) = ↑n

State before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
h₂ : Char.isDigit head = true ∧ ∀ (x : Char), x ∈ tail → Char.isDigit x = true
⊢ -↑(toNatΔ tail) = ↑n
Tactic:
have ⟨ h₃, _⟩ :=h₂
State after:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
h₂ : Char.isDigit head = true ∧ ∀ (x : Char), x ∈ tail → Char.isDigit x = true
h₃ : Char.isDigit head = true
right✝ : ∀ (x : Char), x ∈ tail → Char.isDigit x = true
⊢ -↑(toNatΔ tail) = ↑n

State before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
h₂ : Char.isDigit head = true ∧ ∀ (x : Char), x ∈ tail → Char.isDigit x = true
h₃ : Char.isDigit head = true
right✝ : ∀ (x : Char), x ∈ tail → Char.isDigit x = true
⊢ -↑(toNatΔ tail) = ↑n
Tactic:
simp only [h] at h₃
State after:
no goals

State before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
⊢ (List.all (head :: tail) Char.isDigit == true) = true
Tactic:
rw [← heq]
State after:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
⊢ (List.all (Nat.toDigits 10 n) Char.isDigit == true) = true

State before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
⊢ (List.all (Nat.toDigits 10 n) Char.isDigit == true) = true
Tactic:
apply Nat.toDigits_digits <;> decide
State after:
no goals

State before:
case negSucc
n : ℕ
⊢ (match
      match Int.negSucc n with
      | Int.ofNat m => Nat.toDigits 10 m
      | Int.negSucc m => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m) with
    | [] => 0
    | h :: tail => if h = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (h :: tail))) =
    Int.negSucc n
Tactic:
simp only [List.singleton_append, toNatΔ_inv_NattoDigits, Nat.cast_succ, neg_add_rev, ite_true,
  Int.negSucc_eq]
State after:
no goals