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

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

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

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

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

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

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