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

State before:
c n : ℕ
h1 : (digits 10 c).length = 0
⊢ ¬ProblemPredicate' c n
Tactic:
intro h2
State after:
c n : ℕ
h1 : (digits 10 c).length = 0
h2 : ProblemPredicate' c n
⊢ False

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

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

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

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

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