no goals
F : Type ?u.7255
ι : Type ?u.7258
α : Type u_1
β : Type ?u.7264
inst✝ : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑↑n) x
simpa using n.cast_commute x
no goals
F : Type ?u.7255
ι : Type ?u.7258
α : Type u_1
β : Type ?u.7264
inst✝ : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑-[n+1]) x
simpa only [cast_negSucc, Commute.neg_left_iff, Commute.neg_right_iff] using
  (n + 1).cast_commute (-x)