Theorem: Imo1962P1.without_digits (Compfiles/Imo1962P1.lean)

State before:
n : ℕ
h1 : ProblemPredicate n
⊢ ∃ c, ProblemPredicate' c n
Tactic:
use n / 10
State after:
case h
n : ℕ
h1 : ProblemPredicate n
⊢ ProblemPredicate' (n / 10) n

State before:
case h
n : ℕ
h1 : ProblemPredicate n
⊢ ProblemPredicate' (n / 10) n
Tactic:
cases' n with n
State after:
case h.zero
h1 : ProblemPredicate 0
⊢ ProblemPredicate' (0 / 10) 0

case h.succ
n : ℕ
h1 : ProblemPredicate (n + 1)
⊢ ProblemPredicate' ((n + 1) / 10) (n + 1)

State before:
case h.zero
h1 : ProblemPredicate 0
⊢ ProblemPredicate' (0 / 10) 0
Tactic:
have h2 : ¬ProblemPredicate 0 := by norm_num [ProblemPredicate]
State after:
case h.zero
h1 : ProblemPredicate 0
h2 : ¬ProblemPredicate 0
⊢ ProblemPredicate' (0 / 10) 0

State before:
case h.zero
h1 : ProblemPredicate 0
h2 : ¬ProblemPredicate 0
⊢ ProblemPredicate' (0 / 10) 0
Tactic:
contradiction
State after:
no goals

State before:
h1 : ProblemPredicate 0
⊢ ¬ProblemPredicate 0
Tactic:
norm_num [ProblemPredicate]
State after:
no goals

State before:
case h.succ
n : ℕ
h1 : ProblemPredicate (n + 1)
⊢ ProblemPredicate' ((n + 1) / 10) (n + 1)
Tactic:
rw [ProblemPredicate, digits_def' (by decide : 2 ≤ 10) n.succ_pos, List.headI, List.tail_cons,
  List.concat_eq_append] at h1
State after:
case h.succ
n : ℕ
h1 :
  (match n.succ % 10 :: digits 10 (n.succ / 10) with
      | [] => default
      | a :: tail => a) =
      6 ∧
    ofDigits 10 (digits 10 (n.succ / 10) ++ [6]) = 4 * (n + 1)
⊢ ProblemPredicate' ((n + 1) / 10) (n + 1)

State before:
case h.succ
n : ℕ
h1 :
  (match n.succ % 10 :: digits 10 (n.succ / 10) with
      | [] => default
      | a :: tail => a) =
      6 ∧
    ofDigits 10 (digits 10 (n.succ / 10) ++ [6]) = 4 * (n + 1)
⊢ ProblemPredicate' ((n + 1) / 10) (n + 1)
Tactic:
constructor
State after:
case h.succ.left
n : ℕ
h1 :
  (match n.succ % 10 :: digits 10 (n.succ / 10) with
      | [] => default
      | a :: tail => a) =
      6 ∧
    ofDigits 10 (digits 10 (n.succ / 10) ++ [6]) = 4 * (n + 1)
⊢ n + 1 = 10 * ((n + 1) / 10) + 6

case h.succ.right
n : ℕ
h1 :
  (match n.succ % 10 :: digits 10 (n.succ / 10) with
      | [] => default
      | a :: tail => a) =
      6 ∧
    ofDigits 10 (digits 10 (n.succ / 10) ++ [6]) = 4 * (n + 1)
⊢ 6 * 10 ^ (digits 10 ((n + 1) / 10)).length + (n + 1) / 10 = 4 * (n + 1)

State before:
n : ℕ
h1 : (digits 10 (n + 1)).headI = 6 ∧ ofDigits 10 ((digits 10 (n + 1)).tail.concat 6) = 4 * (n + 1)
⊢ 2 ≤ 10
Tactic:
decide
State after:
no goals

State before:
case h.succ.left
n : ℕ
h1 :
  (match n.succ % 10 :: digits 10 (n.succ / 10) with
      | [] => default
      | a :: tail => a) =
      6 ∧
    ofDigits 10 (digits 10 (n.succ / 10) ++ [6]) = 4 * (n + 1)
⊢ n + 1 = 10 * ((n + 1) / 10) + 6
Tactic:
rw [← h1.left, div_add_mod (n + 1) 10]
State after:
no goals

State before:
case h.succ.right
n : ℕ
h1 :
  (match n.succ % 10 :: digits 10 (n.succ / 10) with
      | [] => default
      | a :: tail => a) =
      6 ∧
    ofDigits 10 (digits 10 (n.succ / 10) ++ [6]) = 4 * (n + 1)
⊢ 6 * 10 ^ (digits 10 ((n + 1) / 10)).length + (n + 1) / 10 = 4 * (n + 1)
Tactic:
rw [← h1.right, ofDigits_append, ofDigits_digits, ofDigits_singleton, add_comm, mul_comm]
State after:
no goals