Theorem: Nat.digit_gt_log_eq_zero (One.lean)

State before:
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ digit b n i = 0
Tactic:
unfold digit
State after:
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ n / b ^ i % b = 0

State before:
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ n / b ^ i % b = 0
Tactic:
convert Nat.zero_mod b
State after:
case e_a.e_a
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ n / b ^ i = 0

State before:
case e_a.e_a
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ n / b ^ i = 0
Tactic:
apply Nat.div_eq_of_lt
State after:
case e_a.e_a.h₀
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ n < b ^ i

State before:
case e_a.e_a.h₀
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ n < b ^ i
Tactic:
apply Nat.lt_pow_of_log_lt
State after:
case e_a.e_a.h₀.hb
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ 1 < b

case e_a.e_a.h₀.a
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ log b n < i

State before:
case e_a.e_a.h₀.hb
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ 1 < b

case e_a.e_a.h₀.a
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ log b n < i
Tactic:
. exact P
State after:
case e_a.e_a.h₀.a
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ log b n < i

State before:
case e_a.e_a.h₀.a
b n i : ℕ
P : b > 1
Q : i > log b n
⊢ log b n < i
Tactic:
. exact Q
State after:
no goals