English
For any α with AddGroupWithOne, (n.bit1 : α) = ((n : α) + n) + 1.
Русский
Для любого α с AddGroupWithOne: (n.bit1 : α) = ((n : α) + n) + 1.
LaTeX
$$$$\forall n:\mathrm{ZNum},\ (n.\text{bit1} : \alpha) = ((n : \alpha) + n) + 1.$$$$
Lean4
@[simp, norm_cast]
theorem cast_bit1 [AddGroupWithOne α] : ∀ n : ZNum, (n.bit1 : α) = ((n : α) + n) + 1
| 0 => by simp [ZNum.bit1]
| pos p => by rw [ZNum.bit1, cast_pos, cast_pos]; rfl
| neg p => by
rw [ZNum.bit1, cast_neg, cast_neg]
rcases e : pred' p with - | a <;> have ep : p = _ := (succ'_pred' p).symm.trans (congr_arg Num.succ' e)
· conv at ep => change p = 1
subst p
simp
· dsimp only [Num.succ'] at ep
subst p
have : (↑(-↑a : ℤ) : α) = -1 + ↑(-↑a + 1 : ℤ) := by simp [add_comm (-↑a : ℤ) 1]
simpa using this
