case z₀
n : ℕ
⊢ digits 2 0 = List.map (fun b => bif b then 1 else 0) (bits 0)

case z₁
n : ℕ
⊢ digits 2 1 = List.map (fun b => bif b then 1 else 0) (bits 1)

case f
n✝ : ℕ
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ digits 2 (bit b n) = List.map (fun b => bif b then 1 else 0) (bits (bit b n))
n✝ n : ℕ
⊢ digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
induction' n using Nat.binaryRecFromOne with b n h ih
case f
n✝ : ℕ
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ digits 2 (bit b n) = List.map (fun b => bif b then 1 else 0) (b :: bits n)
case f
n✝ : ℕ
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ digits 2 (bit b n) = List.map (fun b => bif b then 1 else 0) (bits (bit b n))
rw [bits_append_bit _ _ fun hn => absurd hn h]
case f.false
n✝ n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ digits 2 (bit false n) = List.map (fun b => bif b then 1 else 0) (false :: bits n)

case f.true
n✝ n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ digits 2 (bit true n) = List.map (fun b => bif b then 1 else 0) (true :: bits n)
case f
n✝ : ℕ
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ digits 2 (bit b n) = List.map (fun b => bif b then 1 else 0) (b :: bits n)
cases b
no goals
case z₀
n : ℕ
⊢ digits 2 0 = List.map (fun b => bif b then 1 else 0) (bits 0)
simp
case z₁
n : ℕ
⊢ digits 2 (1 / 2) =
    List.map (fun b => bif b then 1 else 0)
      (Acc.rec (fun x₁ h ih => if h : x₁ = 0 then [] else bodd x₁ :: ih (div2 x₁) (_ : div2 x₁ < x₁))
        (_ : Acc (InvImage WellFoundedRelation.rel fun a => sizeOf a) (div2 1)))
case z₁
n : ℕ
⊢ digits 2 1 = List.map (fun b => bif b then 1 else 0) (bits 1)
simp
no goals
case z₁
n : ℕ
⊢ digits 2 (1 / 2) =
    List.map (fun b => bif b then 1 else 0)
      (Acc.rec (fun x₁ h ih => if h : x₁ = 0 then [] else bodd x₁ :: ih (div2 x₁) (_ : div2 x₁ < x₁))
        (_ : Acc (InvImage WellFoundedRelation.rel fun a => sizeOf a) (div2 1)))
trivial
case f.false
n✝ n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ bit false n % 2 :: digits 2 (bit false n / 2) = List.map (fun b => bif b then 1 else 0) (false :: bits n)

case f.false
n✝ n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ 0 < bit false n
case f.false
n✝ n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ digits 2 (bit false n) = List.map (fun b => bif b then 1 else 0) (false :: bits n)
rw [digits_def' one_lt_two]
no goals
case f.false
n✝ n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ bit false n % 2 :: digits 2 (bit false n / 2) = List.map (fun b => bif b then 1 else 0) (false :: bits n)
simpa [Nat.bit, Nat.bit0_val n]
no goals
case f.false
n✝ n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ 0 < bit false n
simpa [pos_iff_ne_zero, bit_eq_zero_iff]
no goals
case f.true
n✝ n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun b => bif b then 1 else 0) (bits n)
⊢ digits 2 (bit true n) = List.map (fun b => bif b then 1 else 0) (true :: bits n)
simpa [Nat.bit, Nat.bit1_val n, add_comm, digits_add 2 one_lt_two 1 n]