no goals
α : Type u_1
inst✝ : AddGroupWithOne α
⊢ ↑(ZNum.bit1 0) = _root_.bit1 ↑0
simp [ZNum.bit1, _root_.bit1, _root_.bit0]
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(PosNum.bit1 p) = _root_.bit1 ↑p
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(ZNum.bit1 (pos p)) = _root_.bit1 ↑(pos p)
rw [ZNum.bit1, cast_pos, cast_pos]
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(PosNum.bit1 p) = _root_.bit1 ↑p
rfl
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ -↑(Num.casesOn (pred' p) 1 PosNum.bit1) = _root_.bit1 (-↑p)
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(ZNum.bit1 (neg p)) = _root_.bit1 ↑(neg p)
rw [ZNum.bit1, cast_neg, cast_neg]
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : pred' p = Num.zero
ep : p = Num.succ' Num.zero
⊢ -↑(Num.casesOn Num.zero 1 PosNum.bit1) = _root_.bit1 (-↑p)

case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : pred' p = Num.pos a
ep : p = Num.succ' (Num.pos a)
⊢ -↑(Num.casesOn (Num.pos a) 1 PosNum.bit1) = _root_.bit1 (-↑p)
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ -↑(Num.casesOn (pred' p) 1 PosNum.bit1) = _root_.bit1 (-↑p)
cases' e : pred' p with a <;>
  have ep : p = _ := (succ'_pred' p).symm.trans (congr_arg Num.succ' e)
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : pred' p = Num.zero
ep : p = 1
⊢ -↑(Num.casesOn Num.zero 1 PosNum.bit1) = _root_.bit1 (-↑p)
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : pred' p = Num.zero
ep : p = Num.succ' Num.zero
⊢ -↑(Num.casesOn Num.zero 1 PosNum.bit1) = _root_.bit1 (-↑p)
conv at ep => change p = 1
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
e : pred' 1 = Num.zero
⊢ -↑(Num.casesOn Num.zero 1 PosNum.bit1) = _root_.bit1 (-↑1)
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : pred' p = Num.zero
ep : p = 1
⊢ -↑(Num.casesOn Num.zero 1 PosNum.bit1) = _root_.bit1 (-↑p)
subst p
no goals
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
e : pred' 1 = Num.zero
⊢ -↑(Num.casesOn Num.zero 1 PosNum.bit1) = _root_.bit1 (-↑1)
simp [_root_.bit1, _root_.bit0]
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : pred' p = Num.pos a
ep : p = PosNum.succ a
⊢ -↑(Num.casesOn (Num.pos a) 1 PosNum.bit1) = _root_.bit1 (-↑p)
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : pred' p = Num.pos a
ep : p = Num.succ' (Num.pos a)
⊢ -↑(Num.casesOn (Num.pos a) 1 PosNum.bit1) = _root_.bit1 (-↑p)
dsimp only [Num.succ'] at ep
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
e : pred' (PosNum.succ a) = Num.pos a
⊢ -↑(Num.casesOn (Num.pos a) 1 PosNum.bit1) = _root_.bit1 (-↑(PosNum.succ a))
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : pred' p = Num.pos a
ep : p = PosNum.succ a
⊢ -↑(Num.casesOn (Num.pos a) 1 PosNum.bit1) = _root_.bit1 (-↑p)
subst p
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
e : pred' (PosNum.succ a) = Num.pos a
this : ↑(-↑a) = -1 + ↑(-↑a + 1)
⊢ -↑(Num.casesOn (Num.pos a) 1 PosNum.bit1) = _root_.bit1 (-↑(PosNum.succ a))
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
e : pred' (PosNum.succ a) = Num.pos a
⊢ -↑(Num.casesOn (Num.pos a) 1 PosNum.bit1) = _root_.bit1 (-↑(PosNum.succ a))
have : (↑(-↑a : ℤ) : α) = -1 + ↑(-↑a + 1 : ℤ) := by simp [add_comm (- ↑a : ℤ) 1]
no goals
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
e : pred' (PosNum.succ a) = Num.pos a
this : ↑(-↑a) = -1 + ↑(-↑a + 1)
⊢ -↑(Num.casesOn (Num.pos a) 1 PosNum.bit1) = _root_.bit1 (-↑(PosNum.succ a))
simpa [_root_.bit1, _root_.bit0] using this
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
e : pred' (PosNum.succ a) = Num.pos a
⊢ ↑(-↑a) = -1 + ↑(-↑a + 1)
simp [add_comm (- ↑a : ℤ) 1]