-- Mathlib/Data/Num/Lemmas.lean
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
    -- Porting note: `rw [Num.succ']` yields a `match` pattern.
    · dsimp only [Num.succ'] at ep
      subst p
      have : (↑(-↑a : ℤ) : α) = -1 + ↑(-↑a + 1 : ℤ)

Proof state:
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
e : a.succ.pred' = Num.pos a
this : ↑(-↑a) = -1 + ↑(-↑a + 1)
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑a.succ + -↑a.succ + 1

Tactic:
simpa using this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑p.bit1 = ↑p + ↑p + 1

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ -↑(Num.casesOn p.pred' 1 bit1) = -↑p + -↑p + 1

Tactic:
rcases e : pred' p with - | a <;>
  have ep : p = _ := (succ'_pred' p).symm.trans (congr_arg Num.succ' e)

Result:
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
ep : p = Num.zero.succ'
⊢ -↑(Num.casesOn Num.zero 1 bit1) = -↑p + -↑p + 1

case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
ep : p = (Num.pos a).succ'
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑p + -↑p + 1

Proof state:
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
e : a.succ.pred' = Num.pos a
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑a.succ + -↑a.succ + 1

Tactic:
have : (↑(-↑a : ℤ) : α) = -1 + ↑(-↑a + 1 : ℤ) := by simp [add_comm (- ↑a : ℤ) 1]

Result:
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
e : a.succ.pred' = Num.pos a
this : ↑(-↑a) = -1 + ↑(-↑a + 1)
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑a.succ + -↑a.succ + 1

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
e : a.succ.pred' = Num.pos a
⊢ ↑(-↑a) = -1 + ↑(-↑a + 1)

Tactic:
simp [add_comm (- ↑a : ℤ) 1]

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
ep : p = 1
⊢ -↑(Num.casesOn Num.zero 1 bit1) = -↑p + -↑p + 1

Tactic:
subst p

Result:
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
e : pred' 1 = Num.zero
⊢ -↑(Num.casesOn Num.zero 1 bit1) = -↑1 + -↑1 + 1

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(pos p).bit1 = ↑(pos p) + ↑(pos p) + 1

Tactic:
rw [ZNum.bit1, cast_pos, cast_pos]

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑p.bit1 = ↑p + ↑p + 1

Proof state:
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
e : pred' 1 = Num.zero
⊢ -↑(Num.casesOn Num.zero 1 bit1) = -↑1 + -↑1 + 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
⊢ ↑(ZNum.bit1 0) = ↑0 + ↑0 + 1

Tactic:
simp [ZNum.bit1]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
ep : p = (Num.pos a).succ'
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑p + -↑p + 1

Tactic:
dsimp only [Num.succ'] at ep

Result:
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
ep : p = a.succ
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑p + -↑p + 1

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(neg p).bit1 = ↑(neg p) + ↑(neg p) + 1

Tactic:
rw [ZNum.bit1, cast_neg, cast_neg]

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ -↑(Num.casesOn p.pred' 1 bit1) = -↑p + -↑p + 1

Proof state:
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
ep : p = a.succ
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑p + -↑p + 1

Tactic:
subst p

Result:
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
e : a.succ.pred' = Num.pos a
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑a.succ + -↑a.succ + 1

Proof state:
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
ep : p = Num.zero.succ'
⊢ -↑(Num.casesOn Num.zero 1 bit1) = -↑p + -↑p + 1

Tactic:
conv at ep => change p = 1

Result:
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
ep : p = 1
⊢ -↑(Num.casesOn Num.zero 1 bit1) = -↑p + -↑p + 1