Theorem: Imo1960P1.lt_1000 (Compfiles/Imo1960P1.lean)

State before:
n : ℕ
h1 : ProblemPredicate n
⊢ n < 1000
Tactic:
have h2 : n < 10 ^ 3 := by
  rw [← h1.left]
  exact lt_base_pow_length_digits'
State after:
n : ℕ
h1 : ProblemPredicate n
h2 : n < 10 ^ 3
⊢ n < 1000

State before:
n : ℕ
h1 : ProblemPredicate n
h2 : n < 10 ^ 3
⊢ n < 1000
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
h1 : ProblemPredicate n
⊢ n < 10 ^ 3
Tactic:
rw [← h1.left]
State after:
n : ℕ
h1 : ProblemPredicate n
⊢ n < 10 ^ (digits 10 n).length

State before:
n : ℕ
h1 : ProblemPredicate n
⊢ n < 10 ^ (digits 10 n).length
Tactic:
exact lt_base_pow_length_digits'
State after:
no goals