b : Bool
n : ℕ
⊢ (2 * ↑n + bif b then 1 else 0) = ↑(2 * n + bif b then 1 else 0)
b : Bool
n : ℕ
⊢ bit b ↑n = ↑(Nat.bit b n)
rw [bit_val, Nat.bit_val]
no goals
b : Bool
n : ℕ
⊢ (2 * ↑n + bif b then 1 else 0) = ↑(2 * n + bif b then 1 else 0)
cases b <;> rfl