[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
src✝¹ : AddMonoidWithOne (α × β) := instAddMonoidWithOne
src✝ : AddGroup (α × β) := instAddGroup
x✝ : ℕ
⊢ IntCast.intCast ↑x✝ = ↑x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
src✝¹ : AddMonoidWithOne (α × β) := instAddMonoidWithOne
src✝ : AddGroup (α × β) := instAddGroup
x✝ : ℕ
⊢ (↑x✝, ↑x✝) = ↑x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
src✝¹ : AddMonoidWithOne (α × β) := instAddMonoidWithOne
src✝ : AddGroup (α × β) := instAddGroup
x✝ : ℕ
⊢ IntCast.intCast (Int.negSucc x✝) = -↑(x✝ + 1)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : AddGroupWithOne α
inst✝ : AddGroupWithOne β
src✝¹ : AddMonoidWithOne (α × β) := instAddMonoidWithOne
src✝ : AddGroup (α × β) := instAddGroup
x✝ : ℕ
⊢ (-1 + -↑x✝, -1 + -↑x✝) = -1 + -↑x✝
[PROOFSTEP]
rfl
