R : Type u
inst✝ : AddGroupWithOne R
n : ℤ
⊢ bit0 ↑n + 1 = bit1 ↑n
R : Type u
inst✝ : AddGroupWithOne R
n : ℤ
⊢ ↑(bit1 n) = bit1 ↑n
rw [bit1, Int.cast_add, Int.cast_one, cast_bit0]
no goals
R : Type u
inst✝ : AddGroupWithOne R
n : ℤ
⊢ bit0 ↑n + 1 = bit1 ↑n
rfl