no goals
α : Type ?u.445696
⊢ ofNat' 0 = ↑0
simp
α : Type ?u.445696
b : Bool
n : ℕ
IH : Nat.binaryRec 0 (fun b x => bif b then Num.bit1 else Num.bit0) n = ↑n
⊢ Nat.binaryRec 0 (fun b x => bif b then Num.bit1 else Num.bit0) (Nat.bit b n) = ↑(Nat.bit b n)
α : Type ?u.445696
b : Bool
n : ℕ
IH : ofNat' n = ↑n
⊢ ofNat' (Nat.bit b n) = ↑(Nat.bit b n)
rw [ofNat'] at IH ⊢
α : Type ?u.445696
b : Bool
n : ℕ
IH : Nat.binaryRec 0 (fun b x => bif b then Num.bit1 else Num.bit0) n = ↑n
⊢ cond b Num.bit1 Num.bit0 ↑n = ↑(Nat.bit b n)

case h
α : Type ?u.445696
b : Bool
n : ℕ
IH : Nat.binaryRec 0 (fun b x => bif b then Num.bit1 else Num.bit0) n = ↑n
⊢ cond false Num.bit1 Num.bit0 0 = 0
α : Type ?u.445696
b : Bool
n : ℕ
IH : Nat.binaryRec 0 (fun b x => bif b then Num.bit1 else Num.bit0) n = ↑n
⊢ Nat.binaryRec 0 (fun b x => bif b then Num.bit1 else Num.bit0) (Nat.bit b n) = ↑(Nat.bit b n)
rw [Nat.binaryRec_eq, IH]
no goals
α : Type ?u.445696
b : Bool
n : ℕ
IH : Nat.binaryRec 0 (fun b x => bif b then Num.bit1 else Num.bit0) n = ↑n
⊢ cond b Num.bit1 Num.bit0 ↑n = ↑(Nat.bit b n)
cases b <;> simp [Nat.bit, bit0_of_bit0, bit1_of_bit1, Nat.cast_bit0, Nat.cast_bit1]
no goals
case h
α : Type ?u.445696
b : Bool
n : ℕ
IH : Nat.binaryRec 0 (fun b x => bif b then Num.bit1 else Num.bit0) n = ↑n
⊢ cond false Num.bit1 Num.bit0 0 = 0
rfl