case mp
n✝ b n : ℕ
⊢ digits b n = [] → n = 0

case mpr
n✝ b n : ℕ
⊢ n = 0 → digits b n = []
n✝ b n : ℕ
⊢ digits b n = [] ↔ n = 0
constructor
case mp
n✝ b n : ℕ
h : digits b n = []
⊢ n = 0
case mp
n✝ b n : ℕ
⊢ digits b n = [] → n = 0
intro h
case mp
n✝ b n : ℕ
h : digits b n = []
this : ofDigits b (digits b n) = ofDigits b []
⊢ n = 0
case mp
n✝ b n : ℕ
h : digits b n = []
⊢ n = 0
have : ofDigits b (digits b n) = ofDigits b [] := by rw [h]
case h.e'_2
n✝ b n : ℕ
h : digits b n = []
this : ofDigits b (digits b n) = ofDigits b []
⊢ n = ofDigits b (digits b n)
case mp
n✝ b n : ℕ
h : digits b n = []
this : ofDigits b (digits b n) = ofDigits b []
⊢ n = 0
convert this
no goals
case h.e'_2
n✝ b n : ℕ
h : digits b n = []
this : ofDigits b (digits b n) = ofDigits b []
⊢ n = ofDigits b (digits b n)
rw [ofDigits_digits]
no goals
n✝ b n : ℕ
h : digits b n = []
⊢ ofDigits b (digits b n) = ofDigits b []
rw [h]
case mpr
n b : ℕ
⊢ digits b 0 = []
case mpr
n✝ b n : ℕ
⊢ n = 0 → digits b n = []
rintro rfl
no goals
case mpr
n b : ℕ
⊢ digits b 0 = []
simp