Theorem: Usa1992P1.lemma2 (Compfiles/Usa1992P1.lean)

State before:
m y : ℕ
hy : y < 10 ^ m
⊢ (Nat.digits 10 y).length < m + 1
Tactic:
revert y
State after:
m : ℕ
⊢ ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1

State before:
m : ℕ
⊢ ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
Tactic:
induction' m with m ih
State after:
case zero

⊢ ∀ {y : ℕ}, y < 10 ^ 0 → (Nat.digits 10 y).length < 0 + 1

case succ
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
⊢ ∀ {y : ℕ}, y < 10 ^ (m + 1) → (Nat.digits 10 y).length < m + 1 + 1

State before:
case succ
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
⊢ ∀ {y : ℕ}, y < 10 ^ (m + 1) → (Nat.digits 10 y).length < m + 1 + 1
Tactic:
intro y hy
State after:
case succ
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
⊢ (Nat.digits 10 y).length < m + 1 + 1

State before:
case succ
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
⊢ (Nat.digits 10 y).length < m + 1 + 1
Tactic:
obtain rfl | hyp := Nat.eq_zero_or_pos y
State after:
case succ.inl
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
hy : 0 < 10 ^ (m + 1)
⊢ (Nat.digits 10 0).length < m + 1 + 1

case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (Nat.digits 10 y).length < m + 1 + 1

State before:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (Nat.digits 10 y).length < m + 1 + 1
Tactic:
rw [Nat.digits_def' (by norm_num) hyp]
State after:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (y % 10 :: Nat.digits 10 (y / 10)).length < m + 1 + 1

State before:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (y % 10 :: Nat.digits 10 (y / 10)).length < m + 1 + 1
Tactic:
rw [List.length_cons]
State after:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (Nat.digits 10 (y / 10)).length.succ < m + 1 + 1

State before:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (Nat.digits 10 (y / 10)).length.succ < m + 1 + 1
Tactic:
rw [Nat.succ_eq_add_one, add_lt_add_iff_right]
State after:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (Nat.digits 10 (y / 10)).length < m + 1

State before:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (Nat.digits 10 (y / 10)).length < m + 1
Tactic:
have h2 : y / 10 < 10 ^ m := by omega
State after:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
h2 : y / 10 < 10 ^ m
⊢ (Nat.digits 10 (y / 10)).length < m + 1

State before:
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
h2 : y / 10 < 10 ^ m
⊢ (Nat.digits 10 (y / 10)).length < m + 1
Tactic:
exact ih h2
State after:
no goals

State before:
case zero

⊢ ∀ {y : ℕ}, y < 10 ^ 0 → (Nat.digits 10 y).length < 0 + 1
Tactic:
intro y hy
State after:
case zero
y : ℕ
hy : y < 10 ^ 0
⊢ (Nat.digits 10 y).length < 0 + 1

State before:
case zero
y : ℕ
hy : y < 10 ^ 0
⊢ (Nat.digits 10 y).length < 0 + 1
Tactic:
obtain rfl: y = 0 := by omega
State after:
case zero
hy : 0 < 10 ^ 0
⊢ (Nat.digits 10 0).length < 0 + 1

State before:
case zero
hy : 0 < 10 ^ 0
⊢ (Nat.digits 10 0).length < 0 + 1
Tactic:
simp
State after:
no goals

State before:
y : ℕ
hy : y < 10 ^ 0
⊢ y = 0
Tactic:
omega
State after:
no goals

State before:
case succ.inl
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
hy : 0 < 10 ^ (m + 1)
⊢ (Nat.digits 10 0).length < m + 1 + 1
Tactic:
simp
State after:
no goals

State before:
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ 1 < 10
Tactic:
norm_num
State after:
no goals

State before:
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ y / 10 < 10 ^ m
Tactic:
omega
State after:
no goals