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

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
State after:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h3 : c ≠ 0
⊢ n ≥ 153846

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

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

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]
State after:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h4 : c = 0
h5 : (digits 10 c).length = 0
⊢ False

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

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

State before:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h3 : c ≠ 0
⊢ 1 < 10
Tactic:
decide
State after:
no goals

State before:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h3 : c ≠ 0
⊢ 1 ≤ 10
Tactic:
decide
State after:
no goals

State before:
c n : ℕ
h1 : (digits 10 c).length ≥ 6
h2 : ProblemPredicate' c n
h3 : c ≠ 0
⊢ 10 ^ 6 ≥ 153846
Tactic:
norm_num
State after:
no goals