[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
h : m ≤ n
⊢ ↑(n - m) + ↑m = ↑n
[PROOFSTEP]
rw [← cast_add, Nat.sub_add_cancel h]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
h : 0 < 0
⊢ ↑(0 - 1) = ↑0 - 1
[PROOFSTEP]
cases h
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑(n + 1) - 1
[PROOFSTEP]
rw [cast_succ, add_sub_cancel]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑n
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : AddGroupWithOne R
n : ℕ
inst✝ : AtLeastTwo n
⊢ ↑(OfNat.ofNat n) = OfNat.ofNat n
[PROOFSTEP]
simpa only [OfNat.ofNat] using AddGroupWithOne.intCast_ofNat (R := R) n
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑1 = 1
[PROOFSTEP]
erw [cast_ofNat, Nat.cast_one]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑(-↑0) = -↑↑0
[PROOFSTEP]
erw [cast_zero, neg_zero]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(-↑(n + 1)) = -↑↑(n + 1)
[PROOFSTEP]
erw [cast_ofNat, cast_negSucc]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(- -[n+1]) = -↑-[n+1]
[PROOFSTEP]
erw [cast_ofNat, cast_negSucc, neg_neg]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(subNatNat m n) = ↑m - ↑n
[PROOFSTEP]
unfold subNatNat
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(match n - m with
      | 0 => ofNat (m - n)
      | succ k => -[k+1]) =
    ↑m - ↑n
[PROOFSTEP]
cases e : n - m
[GOAL]
case zero
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
e : n - m = zero
⊢ ↑(match zero with
      | 0 => ofNat (m - n)
      | succ k => -[k+1]) =
    ↑m - ↑n
[PROOFSTEP]
simp only [ofNat_eq_coe]
[GOAL]
case zero
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
e : n - m = zero
⊢ ↑↑(m - n) = ↑m - ↑n
[PROOFSTEP]
simp [e, Nat.le_of_sub_eq_zero e]
[GOAL]
case succ
R : Type u
inst✝ : AddGroupWithOne R
m n n✝ : ℕ
e : n - m = succ n✝
⊢ ↑(match succ n✝ with
      | 0 => ofNat (m - n)
      | succ k => -[k+1]) =
    ↑m - ↑n
[PROOFSTEP]
rw [cast_negSucc, Nat.add_one, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e, neg_sub]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(negOfNat n) = -↑n
[PROOFSTEP]
simp [Int.cast_neg, negOfNat_eq]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(↑m + ↑n) = ↑↑m + ↑↑n
[PROOFSTEP]
simp [← Int.ofNat_add, Nat.cast_add]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(↑m + -[n+1]) = ↑↑m + ↑-[n+1]
[PROOFSTEP]
erw [cast_subNatNat, cast_ofNat, cast_negSucc, sub_eq_add_neg]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(-[m+1] + ↑n) = ↑-[m+1] + ↑↑n
[PROOFSTEP]
erw [cast_subNatNat, cast_ofNat, cast_negSucc, sub_eq_iff_eq_add, add_assoc, eq_neg_add_iff_add_eq, ← Nat.cast_add, ←
  Nat.cast_add, Nat.add_comm]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑-[m + n + 1+1] = ↑-[m+1] + ↑-[n+1]
[PROOFSTEP]
rw [cast_negSucc, cast_negSucc, cast_negSucc, ← neg_add_rev, ← Nat.cast_add, Nat.add_right_comm m n 1, Nat.add_assoc,
  Nat.add_comm]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
m n : ℤ
⊢ ↑(m - n) = ↑m - ↑n
[PROOFSTEP]
simp [Int.sub_eq_add_neg, sub_eq_add_neg, Int.cast_neg, Int.cast_add]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
n : ℤ
⊢ ↑(bit1 n) = bit1 ↑n
[PROOFSTEP]
rw [bit1, Int.cast_add, Int.cast_one, cast_bit0]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
n : ℤ
⊢ bit0 ↑n + 1 = bit1 ↑n
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑↑2 = ↑2
[PROOFSTEP]
rw [cast_ofNat, Nat.cast_ofNat]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑↑3 = ↑3
[PROOFSTEP]
rw [cast_ofNat, Nat.cast_ofNat]
[GOAL]
R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑↑4 = ↑4
[PROOFSTEP]
rw [cast_ofNat, Nat.cast_ofNat]
