-- Mathlib/Data/Num/Lemmas.lean
theorem cast_sub' [AddGroupWithOne α] : ∀ m n : PosNum, (sub' m n : α) = m - n
  | a, 1 => by
    rw [sub'_one, Num.cast_toZNum, ← Num.cast_to_nat, pred'_to_nat, ← Nat.sub_one]
    simp [PosNum.cast_pos]
  | 1, b => by
    rw [one_sub', Num.cast_toZNumNeg, ← neg_sub, neg_inj, ← Num.cast_to_nat, pred'_to_nat,
        ← Nat.sub_one]
    simp [PosNum.cast_pos]
  | bit0 a, bit0 b => by
    rw [sub', ZNum.cast_bit0, cast_sub' a b]
    have : ((a + -b + (a + -b) : ℤ) : α) = a + a + (-b + -b)

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑(a.sub' 1) = ↑a - ↑1

Tactic:
rw [sub'_one, Num.cast_toZNum, ← Num.cast_to_nat, pred'_to_nat, ← Nat.sub_one]

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑(↑a - 1) = ↑a - ↑1

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑a - ↑b + (↑a - ↑b) = ↑a.bit0 - ↑b.bit0

Tactic:
have : ((a + -b + (a + -b) : ℤ) : α) = a + a + (-b + -b) := by simp [add_left_comm]

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(↑a + -↑b + (↑a + -↑b)) = ↑a + ↑a + (-↑b + -↑b)
⊢ ↑a - ↑b + (↑a - ↑b) = ↑a.bit0 - ↑b.bit0

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑a - ↑b + (↑a - ↑b) = ↑a.bit1 - ↑b.bit1

Tactic:
have : ((-b + (a + -b) : ℤ) : α) = a + (-b + -b) := by simp [add_left_comm]

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + -↑b)) = ↑a + (-↑b + -↑b)
⊢ ↑a - ↑b + (↑a - ↑b) = ↑a.bit1 - ↑b.bit1

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ ↑(↑b - 1) = ↑b - ↑1

Tactic:
simp [PosNum.cast_pos]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑(↑a - 1) = ↑a - ↑1

Tactic:
simp [PosNum.cast_pos]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.bit0.sub' b.bit0) = ↑a.bit0 - ↑b.bit0

Tactic:
rw [sub', ZNum.cast_bit0, cast_sub' a b]

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑a - ↑b + (↑a - ↑b) = ↑a.bit0 - ↑b.bit0

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(↑a + -↑b + (↑a + -↑b)) = ↑a + ↑a + (-↑b + -↑b)
⊢ ↑a - ↑b + (↑a - ↑b) = ↑a.bit0 - ↑b.bit0

Tactic:
simpa [sub_eq_add_neg] using this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.bit1.sub' b.bit1) = ↑a.bit1 - ↑b.bit1

Tactic:
rw [sub', ZNum.cast_bit0, cast_sub' a b]

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑a - ↑b + (↑a - ↑b) = ↑a.bit1 - ↑b.bit1

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑a - ↑b + (↑a - ↑b) + 1 = ↑a.bit1 - ↑b.bit0

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

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + (-↑b + 1))) = ↑(↑a + 1 + (-↑b + -↑b))
⊢ ↑a - ↑b + (↑a - ↑b) + 1 = ↑a.bit1 - ↑b.bit0

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + (-↑b + -1))) = ↑(↑a + -1 + (-↑b + -↑b))
⊢ ↑a - ↑b + (↑a - ↑b) - 1 = ↑a.bit0 - ↑b.bit1

Tactic:
simpa [sub_eq_add_neg] using this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.bit0.sub' b.bit1) = ↑a.bit0 - ↑b.bit1

Tactic:
rw [sub', ZNum.cast_bitm1, cast_sub' a b]

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑a - ↑b + (↑a - ↑b) - 1 = ↑a.bit0 - ↑b.bit1

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + (-↑b + 1))) = ↑(↑a + 1 + (-↑b + -↑b))
⊢ ↑a - ↑b + (↑a - ↑b) + 1 = ↑a.bit1 - ↑b.bit0

Tactic:
simpa [sub_eq_add_neg] using this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ ↑(sub' 1 b) = ↑1 - ↑b

Tactic:
rw [one_sub', Num.cast_toZNumNeg, ← neg_sub, neg_inj, ← Num.cast_to_nat, pred'_to_nat,
    ← Nat.sub_one]

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ ↑(↑b - 1) = ↑b - ↑1

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(↑a + -↑b + (↑a + -↑b)) = ↑a + ↑a + (-↑b + -↑b)

Tactic:
simp [add_left_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + -↑b)) = ↑a + (-↑b + -↑b)
⊢ ↑a - ↑b + (↑a - ↑b) = ↑a.bit1 - ↑b.bit1

Tactic:
simpa [sub_eq_add_neg] using this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(-↑b + (↑a + (-↑b + 1))) = ↑(↑a + 1 + (-↑b + -↑b))

Tactic:
simp [add_comm, add_left_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(-↑b + (↑a + -↑b)) = ↑a + (-↑b + -↑b)

Tactic:
simp [add_left_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑a - ↑b + (↑a - ↑b) - 1 = ↑a.bit0 - ↑b.bit1

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

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
this : ↑(-↑b + (↑a + (-↑b + -1))) = ↑(↑a + -1 + (-↑b + -↑b))
⊢ ↑a - ↑b + (↑a - ↑b) - 1 = ↑a.bit0 - ↑b.bit1

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.bit1.sub' b.bit0) = ↑a.bit1 - ↑b.bit0

Tactic:
rw [sub', ZNum.cast_bit1, cast_sub' a b]

Result:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑a - ↑b + (↑a - ↑b) + 1 = ↑a.bit1 - ↑b.bit0

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(-↑b + (↑a + (-↑b + -1))) = ↑(↑a + -1 + (-↑b + -↑b))

Tactic:
simp [add_comm, add_left_comm]

Result:
no goals