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

State before:
n : ℕ
h1 : ProblemPredicate n
⊢ 100 ≤ n
Tactic:
have h2 : 10 ^ 3 ≤ 10 * n := by
  rw [← h1.left]
  refine Nat.base_pow_length_digits_le 10 n ?_ (not_zero h1)
  simp
State after:
n : ℕ
h1 : ProblemPredicate n
h2 : 10 ^ 3 ≤ 10 * n
⊢ 100 ≤ n

State before:
n : ℕ
h1 : ProblemPredicate n
h2 : 10 ^ 3 ≤ 10 * n
⊢ 100 ≤ n
Tactic:
linarith
State after:
no goals

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

State before:
n : ℕ
h1 : ProblemPredicate n
⊢ 10 ^ (digits 10 n).length ≤ 10 * n
Tactic:
refine Nat.base_pow_length_digits_le 10 n ?_ (not_zero h1)
State after:
n : ℕ
h1 : ProblemPredicate n
⊢ 1 < 10

State before:
n : ℕ
h1 : ProblemPredicate n
⊢ 1 < 10
Tactic:
simp
State after:
no goals