internlm/Lean-Github huggingface dataset:
Theorem: Imo1962P1.without_digits
Proof state before:
case h
n : ℕ
h1 : ProblemPredicate n
⊢ ProblemPredicate' (n / 10) n
Tactic:
cases' n with n
Proof 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)
Theorem: Imo1962P1.without_digits
Proof state before:
case h.zero
h1 : ProblemPredicate 0
⊢ ProblemPredicate' (0 / 10) 0
Tactic:
have h2 : ¬ProblemPredicate 0 := by norm_num [ProblemPredicate]
Proof state after:
case h.zero
h1 : ProblemPredicate 0
h2 : ¬ProblemPredicate 0
⊢ ProblemPredicate' (0 / 10) 0
Theorem: Imo1962P1.without_digits
Proof state before:
case h.zero
h1 : ProblemPredicate 0
h2 : ¬ProblemPredicate 0
⊢ ProblemPredicate' (0 / 10) 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Imo1962P1.without_digits
Proof state before:
h1 : ProblemPredicate 0
⊢ ¬ProblemPredicate 0
Tactic:
norm_num [ProblemPredicate]
Proof state after:
no goals
Theorem: Imo1962P1.without_digits
Proof 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
Proof 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)
Theorem: Imo1962P1.without_digits
Proof 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
Proof 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)
Theorem: Imo1962P1.without_digits
Proof 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
Proof state after:
no goals
Theorem: Imo1962P1.without_digits
Proof 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]
Proof state after:
no goals
Theorem: Imo1962P1.without_digits
Proof 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]
Proof state after:
no goals
Theorem: Imo1962P1.case_0_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 0
⊢ ¬ProblemPredicate' c n
Tactic:
intro h2
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 0
h2 : ProblemPredicate' c n
⊢ False
Theorem: Imo1962P1.case_0_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 0
h2 : ProblemPredicate' c n
⊢ False
Tactic:
have h3 : 6 * 10 ^ 0 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [h1]
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 0
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 0 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ False
Theorem: Imo1962P1.case_0_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 0
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 0 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ False
Tactic:
have h4 : 6 * 10 ^ 0 + c = 4 * (10 * c + 6) := by rw [h3, h2.right, h2.left]
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 0
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 0 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 0 + c = 4 * (10 * c + 6)
⊢ False
Theorem: Imo1962P1.case_0_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 0
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 0 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 0 + c = 4 * (10 * c + 6)
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1962P1.case_0_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 0
h2 : ProblemPredicate' c n
⊢ 6 * 10 ^ 0 + c = 6 * 10 ^ (digits 10 c).length + c
Tactic:
rw [h1]
Proof state after:
no goals
Theorem: Imo1962P1.case_0_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 0
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 0 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ 6 * 10 ^ 0 + c = 4 * (10 * c + 6)
Tactic:
rw [h3, h2.right, h2.left]
Proof state after:
no goals
Theorem: Imo1962P1.case_1_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 1
⊢ ¬ProblemPredicate' c n
Tactic:
intro h2
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 1
h2 : ProblemPredicate' c n
⊢ False
Theorem: Imo1962P1.case_1_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 1
h2 : ProblemPredicate' c n
⊢ False
Tactic:
have h3 : 6 * 10 ^ 1 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [h1]
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 1
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 1 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ False
Theorem: Imo1962P1.case_1_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 1
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 1 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ False
Tactic:
have h4 : 6 * 10 ^ 1 + c = 4 * (10 * c + 6) := by rw [h3, h2.right, h2.left]
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 1
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 1 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 1 + c = 4 * (10 * c + 6)
⊢ False
Theorem: Imo1962P1.case_1_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 1
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 1 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 1 + c = 4 * (10 * c + 6)
⊢ False
Tactic:
have h6 : c > 0 := by linarith
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 1
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 1 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 1 + c = 4 * (10 * c + 6)
h6 : c > 0
⊢ False
Theorem: Imo1962P1.case_1_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 1
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 1 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 1 + c = 4 * (10 * c + 6)
h6 : c > 0
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1962P1.case_1_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 1
h2 : ProblemPredicate' c n
⊢ 6 * 10 ^ 1 + c = 6 * 10 ^ (digits 10 c).length + c
Tactic:
rw [h1]
Proof state after:
no goals
Theorem: Imo1962P1.case_1_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 1
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 1 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ 6 * 10 ^ 1 + c = 4 * (10 * c + 6)
Tactic:
rw [h3, h2.right, h2.left]
Proof state after:
no goals
Theorem: Imo1962P1.case_1_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 1
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 1 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 1 + c = 4 * (10 * c + 6)
⊢ c > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1962P1.case_2_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 2
⊢ ¬ProblemPredicate' c n
Tactic:
intro h2
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 2
h2 : ProblemPredicate' c n
⊢ False
Theorem: Imo1962P1.case_2_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 2
h2 : ProblemPredicate' c n
⊢ False
Tactic:
have h3 : 6 * 10 ^ 2 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [h1]
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 2
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 2 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ False
Theorem: Imo1962P1.case_2_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 2
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 2 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ False
Tactic:
have h4 : 6 * 10 ^ 2 + c = 4 * (10 * c + 6) := by rw [h3, h2.right, h2.left]
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 2
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 2 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 2 + c = 4 * (10 * c + 6)
⊢ False
Theorem: Imo1962P1.case_2_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 2
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 2 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 2 + c = 4 * (10 * c + 6)
⊢ False
Tactic:
have h5 : c > 14 := by linarith
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 2
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 2 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 2 + c = 4 * (10 * c + 6)
h5 : c > 14
⊢ False
Theorem: Imo1962P1.case_2_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 2
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 2 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 2 + c = 4 * (10 * c + 6)
h5 : c > 14
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1962P1.case_2_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 2
h2 : ProblemPredicate' c n
⊢ 6 * 10 ^ 2 + c = 6 * 10 ^ (digits 10 c).length + c
Tactic:
rw [h1]
Proof state after:
no goals
Theorem: Imo1962P1.case_2_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 2
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 2 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ 6 * 10 ^ 2 + c = 4 * (10 * c + 6)
Tactic:
rw [h3, h2.right, h2.left]
Proof state after:
no goals
Theorem: Imo1962P1.case_2_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 2
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 2 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 2 + c = 4 * (10 * c + 6)
⊢ c > 14
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1962P1.case_3_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 3
⊢ ¬ProblemPredicate' c n
Tactic:
intro h2
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 3
h2 : ProblemPredicate' c n
⊢ False
Theorem: Imo1962P1.case_3_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 3
h2 : ProblemPredicate' c n
⊢ False
Tactic:
have h3 : 6 * 10 ^ 3 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [h1]
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 3
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 3 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ False
Theorem: Imo1962P1.case_3_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 3
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 3 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ False
Tactic:
have h4 : 6 * 10 ^ 3 + c = 4 * (10 * c + 6) := by rw [h3, h2.right, h2.left]
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 3
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 3 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 3 + c = 4 * (10 * c + 6)
⊢ False
Theorem: Imo1962P1.case_3_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 3
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 3 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 3 + c = 4 * (10 * c + 6)
⊢ False
Tactic:
have h5 : c > 153 := by linarith
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 3
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 3 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 3 + c = 4 * (10 * c + 6)
h5 : c > 153
⊢ False
Theorem: Imo1962P1.case_3_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 3
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 3 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 3 + c = 4 * (10 * c + 6)
h5 : c > 153
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1962P1.case_3_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 3
h2 : ProblemPredicate' c n
⊢ 6 * 10 ^ 3 + c = 6 * 10 ^ (digits 10 c).length + c
Tactic:
rw [h1]
Proof state after:
no goals
Theorem: Imo1962P1.case_3_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 3
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 3 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ 6 * 10 ^ 3 + c = 4 * (10 * c + 6)
Tactic:
rw [h3, h2.right, h2.left]
Proof state after:
no goals
Theorem: Imo1962P1.case_3_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 3
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 3 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 3 + c = 4 * (10 * c + 6)
⊢ c > 153
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1962P1.case_4_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 4
⊢ ¬ProblemPredicate' c n
Tactic:
intro h2
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 4
h2 : ProblemPredicate' c n
⊢ False
Theorem: Imo1962P1.case_4_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 4
h2 : ProblemPredicate' c n
⊢ False
Tactic:
have h3 : 6 * 10 ^ 4 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [h1]
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 4
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 4 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ False
Theorem: Imo1962P1.case_4_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 4
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 4 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ False
Tactic:
have h4 : 6 * 10 ^ 4 + c = 4 * (10 * c + 6) := by rw [h3, h2.right, h2.left]
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 4
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 4 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 4 + c = 4 * (10 * c + 6)
⊢ False
Theorem: Imo1962P1.case_4_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 4
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 4 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 4 + c = 4 * (10 * c + 6)
⊢ False
Tactic:
have h5 : c > 1537 := by linarith
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 4
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 4 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 4 + c = 4 * (10 * c + 6)
h5 : c > 1537
⊢ False
Theorem: Imo1962P1.case_4_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 4
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 4 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 4 + c = 4 * (10 * c + 6)
h5 : c > 1537
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1962P1.case_4_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 4
h2 : ProblemPredicate' c n
⊢ 6 * 10 ^ 4 + c = 6 * 10 ^ (digits 10 c).length + c
Tactic:
rw [h1]
Proof state after:
no goals
Theorem: Imo1962P1.case_4_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 4
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 4 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ 6 * 10 ^ 4 + c = 4 * (10 * c + 6)
Tactic:
rw [h3, h2.right, h2.left]
Proof state after:
no goals
Theorem: Imo1962P1.case_4_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 4
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 4 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 4 + c = 4 * (10 * c + 6)
⊢ c > 1537
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1962P1.helper_5_digit
Proof state before:
c : ℤ
h : 6 * 10 ^ 5 + c = 4 * (10 * c + 6)
⊢ c = 15384
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1962P1.case_5_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 5
h2 : ProblemPredicate' c n
⊢ c = 15384
Tactic:
have h3 : 6 * 10 ^ 5 + c = 6 * 10 ^ (digits 10 c).length + c := by rw [h1]
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 5
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 5 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ c = 15384
Theorem: Imo1962P1.case_5_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 5
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 5 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ c = 15384
Tactic:
have h4 : 6 * 10 ^ 5 + c = 4 * (10 * c + 6) := by rw [h3, h2.right, h2.left]
Proof state after:
c n : ℕ
h1 : (digits 10 c).length = 5
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 5 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 5 + c = 4 * (10 * c + 6)
⊢ c = 15384
Theorem: Imo1962P1.case_5_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 5
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 5 + c = 6 * 10 ^ (digits 10 c).length + c
h4 : 6 * 10 ^ 5 + c = 4 * (10 * c + 6)
⊢ c = 15384
Tactic:
zify at *
Proof state after:
c n : ℕ
h2 : ProblemPredicate' c n
h1 : ↑(digits 10 c).length = 5
h3 : 6 * 10 ^ 5 + ↑c = 6 * 10 ^ (digits 10 c).length + ↑c
h4 : 6 * 10 ^ 5 + ↑c = 4 * (10 * ↑c + 6)
⊢ ↑c = 15384
Theorem: Imo1962P1.case_5_digit
Proof state before:
c n : ℕ
h2 : ProblemPredicate' c n
h1 : ↑(digits 10 c).length = 5
h3 : 6 * 10 ^ 5 + ↑c = 6 * 10 ^ (digits 10 c).length + ↑c
h4 : 6 * 10 ^ 5 + ↑c = 4 * (10 * ↑c + 6)
⊢ ↑c = 15384
Tactic:
exact helper_5_digit h4
Proof state after:
no goals
Theorem: Imo1962P1.case_5_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 5
h2 : ProblemPredicate' c n
⊢ 6 * 10 ^ 5 + c = 6 * 10 ^ (digits 10 c).length + c
Tactic:
rw [h1]
Proof state after:
no goals
Theorem: Imo1962P1.case_5_digit
Proof state before:
c n : ℕ
h1 : (digits 10 c).length = 5
h2 : ProblemPredicate' c n
h3 : 6 * 10 ^ 5 + c = 6 * 10 ^ (digits 10 c).length + c
⊢ 6 * 10 ^ 5 + c = 4 * (10 * c + 6)
Tactic:
rw [h3, h2.right, h2.left]
Proof state after:
no goals
Theorem: Imo1962P1.case_more_digits
Proof state before:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
⊢ n ≥ 153846
Tactic:
have h3 : c ≠ 0 := by
  intro h4
  have h5 : (digits 10 c).length = 0 := by simp [h4]
  exact case_0_digit h5 h2
Proof state after:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h3 : c ≠ 0
⊢ n ≥ 153846
Theorem: Imo1962P1.case_more_digits
Proof state before:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h3 : c ≠ 0
⊢ n ≥ 153846
Tactic:
calc
  n ≥ 10 * c := le.intro h2.left.symm
  _ ≥ 10 ^ (digits 10 c).length := (base_pow_length_digits_le 10 c (by decide) h3)
  _ ≥ 10 ^ 6 := pow_le_pow_right (by decide) h1
  _ ≥ 153846 := by norm_num
Proof state after:
no goals
Theorem: Imo1962P1.case_more_digits
Proof state before:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
⊢ c ≠ 0
Tactic:
intro h4
Proof state after:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h4 : c = 0
⊢ False
Theorem: Imo1962P1.case_more_digits
Proof state before:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h4 : c = 0
⊢ False
Tactic:
have h5 : (digits 10 c).length = 0 := by simp [h4]
Proof state after:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h4 : c = 0
h5 : (digits 10 c).length = 0
⊢ False
Theorem: Imo1962P1.case_more_digits
Proof state before:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h4 : c = 0
h5 : (digits 10 c).length = 0
⊢ False
Tactic:
exact case_0_digit h5 h2
Proof state after:
no goals
Theorem: Imo1962P1.case_more_digits
Proof state before:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h4 : c = 0
⊢ (digits 10 c).length = 0
Tactic:
simp [h4]
Proof state after:
no goals
Theorem: Imo1962P1.case_more_digits
Proof state before:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h3 : c ≠ 0
⊢ 1 < 10
Tactic:
decide
Proof state after:
no goals
Theorem: Imo1962P1.case_more_digits
Proof state before:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h3 : c ≠ 0
⊢ 1 ≤ 10
Tactic:
decide
Proof state after:
no goals
Theorem: Imo1962P1.case_more_digits
Proof state before:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h3 : c ≠ 0
⊢ 10 ^ 6 ≥ 153846
Tactic:
norm_num
Proof state after:
no goals
Theorem: Imo1962P1.satisfied_by_153846
Proof state before:
⊢ ProblemPredicate 153846
Tactic:
norm_num [ProblemPredicate]
Proof state after:
⊢ ofDigits 10 [4, 8, 3, 5, 1, 6] = 615384
Theorem: Imo1962P1.satisfied_by_153846
Proof state before:
⊢ ofDigits 10 [4, 8, 3, 5, 1, 6] = 615384
Tactic:
decide
Proof state after:
no goals
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
n : ℕ
h1 : ProblemPredicate n
⊢ n ≥ 153846
Tactic:
have ⟨c, h2⟩ := without_digits h1
Proof state after:
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
⊢ n ≥ 153846
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
⊢ n ≥ 153846
Tactic:
have h3 : (digits 10 c).length < 6 ∨ (digits 10 c).length ≥ 6 := by apply lt_or_ge
Proof state after:
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h3 : (digits 10 c).length < 6 ∨ (digits 10 c).length ≥ 6
⊢ n ≥ 153846
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
⊢ (digits 10 c).length < 6 ∨ (digits 10 c).length ≥ 6
Tactic:
apply lt_or_ge
Proof state after:
no goals
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inr
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h3 : (digits 10 c).length ≥ 6
⊢ n ≥ 153846
Tactic:
exact case_more_digits h3 h2
Proof state after:
no goals
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inl
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h3 : (digits 10 c).length < 6
⊢ n ≥ 153846
Tactic:
interval_cases h : (digits 10 c).length
Proof state after:
case inl.«0»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 0
h3 : 0 < 6
⊢ n ≥ 153846

case inl.«1»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 1
h3 : 1 < 6
⊢ n ≥ 153846

case inl.«2»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 2
h3 : 2 < 6
⊢ n ≥ 153846

case inl.«3»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 3
h3 : 3 < 6
⊢ n ≥ 153846

case inl.«4»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 4
h3 : 4 < 6
⊢ n ≥ 153846

case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
⊢ n ≥ 153846
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inl.«0»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 0
h3 : 0 < 6
⊢ n ≥ 153846
Tactic:
exfalso
Proof state after:
case inl.«0»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 0
h3 : 0 < 6
⊢ False
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inl.«0»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 0
h3 : 0 < 6
⊢ False
Tactic:
exact case_0_digit h h2
Proof state after:
no goals
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inl.«1»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 1
h3 : 1 < 6
⊢ n ≥ 153846
Tactic:
exfalso
Proof state after:
case inl.«1»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 1
h3 : 1 < 6
⊢ False
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inl.«1»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 1
h3 : 1 < 6
⊢ False
Tactic:
exact case_1_digit h h2
Proof state after:
no goals
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inl.«2»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 2
h3 : 2 < 6
⊢ n ≥ 153846
Tactic:
exfalso
Proof state after:
case inl.«2»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 2
h3 : 2 < 6
⊢ False
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inl.«2»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 2
h3 : 2 < 6
⊢ False
Tactic:
exact case_2_digit h h2
Proof state after:
no goals
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inl.«3»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 3
h3 : 3 < 6
⊢ n ≥ 153846
Tactic:
exfalso
Proof state after:
case inl.«3»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 3
h3 : 3 < 6
⊢ False