Theorem: Int.not_newline_mem_reprΔ (One.lean)

State before:
n : ℤ
⊢ ¬Char.ofNat 10 ∈ reprΔ n
Tactic:
unfold reprΔ
State after:
n : ℤ
⊢ ¬Char.ofNat 10 ∈
      match n with
      | ofNat m => Nat.toDigits 10 m
      | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)

State before:
n : ℤ
⊢ ¬Char.ofNat 10 ∈
      match n with
      | ofNat m => Nat.toDigits 10 m
      | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)
Tactic:
intro contr
State after:
n : ℤ
contr :
  Char.ofNat 10 ∈
    match n with
    | ofNat m => Nat.toDigits 10 m
    | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)
⊢ False

State before:
n : ℤ
contr :
  Char.ofNat 10 ∈
    match n with
    | ofNat m => Nat.toDigits 10 m
    | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)
⊢ False
Tactic:
split at contr
State after:
case h_1
i✝ : ℤ
m✝ : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 m✝
⊢ False

case h_2
i✝ : ℤ
m✝ : ℕ
contr : Char.ofNat 10 ∈ [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m✝)
⊢ False

State before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
⊢ False
Tactic:
case h_1 n =>
    have isdig := Nat.toDigits_digits 10 n
    simp only [beq_iff_eq, List.all_eq_true, forall_true_left] at isdig
    have h := isdig '\n' contr
    simp only at h
State after:
no goals

State before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ n)
⊢ False
Tactic:
case h_2 n =>
  simp only [List.singleton_append, List.find?, List.mem_cons, false_or] at contr
  have isdig := Nat.toDigits_digits 10 (Nat.succ n)
  simp only [beq_iff_eq, List.all_eq_true, forall_true_left] at isdig
  have h := isdig '\n' contr
  simp only at h
State after:
no goals

State before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
⊢ False
Tactic:
have isdig := Nat.toDigits_digits 10 n
State after:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
isdig : 10 ≤ 10 → 10 > 1 → (List.all (Nat.toDigits 10 n) Char.isDigit == true) = true
⊢ False

State before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
isdig : 10 ≤ 10 → 10 > 1 → (List.all (Nat.toDigits 10 n) Char.isDigit == true) = true
⊢ False
Tactic:
simp only [beq_iff_eq, List.all_eq_true, forall_true_left] at isdig
State after:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 n → Char.isDigit x = true
⊢ False

State before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 n → Char.isDigit x = true
⊢ False
Tactic:
have h := isdig '\n' contr
State after:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 n → Char.isDigit x = true
h : Char.isDigit (Char.ofNat 10) = true
⊢ False

State before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 n → Char.isDigit x = true
h : Char.isDigit (Char.ofNat 10) = true
⊢ False
Tactic:
simp only at h
State after:
no goals

State before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ n)
⊢ False
Tactic:
simp only [List.singleton_append, List.find?, List.mem_cons, false_or] at contr
State after:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
⊢ False

State before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
⊢ False
Tactic:
have isdig := Nat.toDigits_digits 10 (Nat.succ n)
State after:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
isdig : 10 ≤ 10 → 10 > 1 → (List.all (Nat.toDigits 10 (Nat.succ n)) Char.isDigit == true) = true
⊢ False

State before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
isdig : 10 ≤ 10 → 10 > 1 → (List.all (Nat.toDigits 10 (Nat.succ n)) Char.isDigit == true) = true
⊢ False
Tactic:
simp only [beq_iff_eq, List.all_eq_true, forall_true_left] at isdig
State after:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 (Nat.succ n) → Char.isDigit x = true
⊢ False

State before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 (Nat.succ n) → Char.isDigit x = true
⊢ False
Tactic:
have h := isdig '\n' contr
State after:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 (Nat.succ n) → Char.isDigit x = true
h : Char.isDigit (Char.ofNat 10) = true
⊢ False

State before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 (Nat.succ n) → Char.isDigit x = true
h : Char.isDigit (Char.ofNat 10) = true
⊢ False
Tactic:
simp only at h
State after:
no goals