[GOAL]
x : ℤ
⊢ IsUnit x ↔ |x| = 1
[PROOFSTEP]
rw [isUnit_iff_natAbs_eq, abs_eq_natAbs, ← Int.ofNat_one, coe_nat_inj']
[GOAL]
a : ℤ
ha : IsUnit a
⊢ a ^ 2 = 1
[PROOFSTEP]
rw [sq, isUnit_mul_self ha]
[GOAL]
u : ℤˣ
⊢ u ^ 2 = 1
[PROOFSTEP]
rw [Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one, isUnit_sq u.isUnit]
[GOAL]
u : ℤˣ
⊢ u * u = 1
[PROOFSTEP]
rw [← sq, units_sq]
[GOAL]
u : ℤˣ
⊢ u⁻¹ = u
[PROOFSTEP]
rw [inv_eq_iff_mul_eq_one, units_mul_self]
[GOAL]
u : ℤˣ
⊢ ↑u * ↑u = 1
[PROOFSTEP]
rw [← Units.val_mul, units_mul_self, Units.val_one]
[GOAL]
n : ℕ
⊢ 0 < |(-1)|
[PROOFSTEP]
simp
[GOAL]
u : ℤˣ
n : ℕ
⊢ u ^ n = u ^ (n % 2)
[PROOFSTEP]
conv =>
  lhs
  rw [← Nat.mod_add_div n 2]; rw [pow_add, pow_mul, units_sq, one_pow, mul_one]
[GOAL]
u : ℤˣ
n : ℕ
| u ^ n = u ^ (n % 2)
[PROOFSTEP]
  lhs
  rw [← Nat.mod_add_div n 2]; rw [pow_add, pow_mul, units_sq, one_pow, mul_one]
[GOAL]
u : ℤˣ
n : ℕ
| u ^ n = u ^ (n % 2)
[PROOFSTEP]
  lhs
  rw [← Nat.mod_add_div n 2]; rw [pow_add, pow_mul, units_sq, one_pow, mul_one]
[GOAL]
u : ℤˣ
n : ℕ
| u ^ n = u ^ (n % 2)
[PROOFSTEP]
lhs
[GOAL]
u : ℤˣ
n : ℕ
| u ^ n
[PROOFSTEP]
rw [← Nat.mod_add_div n 2]
[GOAL]
u : ℤˣ
n : ℕ
| u ^ (n % 2 + 2 * (n / 2))
[PROOFSTEP]
rw [pow_add, pow_mul, units_sq, one_pow, mul_one]
