/-
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad

! This file was ported from Lean 3 source module data.int.order.units
! leanprover-community/mathlib commit d012cd09a9b256d870751284dd6a29882b0be105
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Int.Order.Basic
import Mathlib.Data.Int.Units
import Mathlib.Algebra.GroupPower.Order

/-!
# Lemmas about units in `ℤ`, which interact with the order structure.
-/


namespace Int

theorem 
isUnit_iff_abs_eq: ∀ {x : ℤ}, IsUnit x ↔ abs x = 1
isUnit_iff_abs_eq {
x: ℤ
x : 
ℤ: Type
ℤ} : 
IsUnit: {M : Type ?u.4} → [inst : Monoid M] → M → Prop
IsUnit 
x: ℤ
x ↔ 
abs: {α : Type ?u.15} → [self : Abs α] → α → α
abs 
x: ℤ
x = 
1: ?m.121
1 := by
Goals accomplished! 🐙
  
x: ℤ

IsUnit x ↔ abs x = 1rw [
x: ℤ

IsUnit x ↔ abs x = 1
isUnit_iff_natAbs_eq: ∀ {n : ℤ}, IsUnit n ↔ natAbs n = 1
isUnit_iff_natAbs_eq,
x: ℤ

natAbs x = 1 ↔ abs x = 1 
x: ℤ

IsUnit x ↔ abs x = 1
abs_eq_natAbs: ∀ (a : ℤ), abs a = ↑(natAbs a)
abs_eq_natAbs,
x: ℤ

natAbs x = 1 ↔ ↑(natAbs x) = 1 
x: ℤ

IsUnit x ↔ abs x = 1← 
Int.ofNat_one: ↑1 = 1
Int.ofNat_one,
x: ℤ

natAbs x = 1 ↔ ↑(natAbs x) = ↑1 
x: ℤ

IsUnit x ↔ abs x = 1
coe_nat_inj': ∀ {m n : ℕ}, ↑m = ↑n ↔ m = n
coe_nat_inj'
x: ℤ

natAbs x = 1 ↔ natAbs x = 1]
Goals accomplished! 🐙
#align int.is_unit_iff_abs_eq 
Int.isUnit_iff_abs_eq: ∀ {x : ℤ}, IsUnit x ↔ abs x = 1
Int.isUnit_iff_abs_eq

theorem 
isUnit_sq: ∀ {a : ℤ}, IsUnit a → a ^ 2 = 1
isUnit_sq {
a: ℤ
a : 
ℤ: Type
ℤ} (
ha: IsUnit a
ha : 
IsUnit: {M : Type ?u.198} → [inst : Monoid M] → M → Prop
IsUnit 
a: ℤ
a) : 
a: ℤ
a ^ 
2: ?m.232
2 = 
1: ?m.246
1 := by
Goals accomplished! 🐙 
a: ℤ

ha: IsUnit a

a ^ 2 = 1rw [
a: ℤ

ha: IsUnit a

a ^ 2 = 1
sq: ∀ {M : Type ?u.441} [inst : Monoid M] (a : M), a ^ 2 = a * a
sq,
a: ℤ

ha: IsUnit a

a * a = 1 
a: ℤ

ha: IsUnit a

a ^ 2 = 1
isUnit_mul_self: ∀ {a : ℤ}, IsUnit a → a * a = 1
isUnit_mul_self 
ha: IsUnit a
ha
a: ℤ

ha: IsUnit a

1 = 1]
Goals accomplished! 🐙
#align int.is_unit_sq 
Int.isUnit_sq: ∀ {a : ℤ}, IsUnit a → a ^ 2 = 1
Int.isUnit_sq

@[simp]
theorem 
units_sq: ∀ (u : ℤˣ), u ^ 2 = 1
units_sq (
u: ℤˣ
u : 
ℤ: Type
ℤˣ) : 
u: ℤˣ
u ^ 
2: ?m.533
2 = 
1: ?m.547
1 := by
Goals accomplished! 🐙
  
u: ℤˣ

u ^ 2 = 1rw [
u: ℤˣ

u ^ 2 = 1
Units.ext_iff: ∀ {α : Type ?u.1230} [inst : Monoid α] {a b : αˣ}, a = b ↔ ↑a = ↑b
Units.ext_iff,
u: ℤˣ

↑(u ^ 2) = ↑1 
u: ℤˣ

u ^ 2 = 1
Units.val_pow_eq_pow_val: ∀ {M : Type ?u.1276} [inst : Monoid M] (u : Mˣ) (n : ℕ), ↑(u ^ n) = ↑u ^ n
Units.val_pow_eq_pow_val,
u: ℤˣ

↑u ^ 2 = ↑1 
u: ℤˣ

u ^ 2 = 1
Units.val_one: ∀ {α : Type ?u.1331} [inst : Monoid α], ↑1 = 1
Units.val_one,
u: ℤˣ

↑u ^ 2 = 1 
u: ℤˣ

u ^ 2 = 1
isUnit_sq: ∀ {a : ℤ}, IsUnit a → a ^ 2 = 1
isUnit_sq 
u: ℤˣ
u.
isUnit: ∀ {M : Type ?u.1387} [inst : Monoid M] (u : Mˣ), IsUnit ↑u
isUnit
u: ℤˣ

1 = 1]
Goals accomplished! 🐙
#align int.units_sq 
Int.units_sq: ∀ (u : ℤˣ), u ^ 2 = 1
Int.units_sq

alias 
units_sq: ∀ (u : ℤˣ), u ^ 2 = 1
units_sq ← 
units_pow_two: ∀ (u : ℤˣ), u ^ 2 = 1
units_pow_two
#align int.units_pow_two 
Int.units_pow_two: ∀ (u : ℤˣ), u ^ 2 = 1
Int.units_pow_two

@[simp]
theorem 
units_mul_self: ∀ (u : ℤˣ), u * u = 1
units_mul_self (
u: ℤˣ
u : 
ℤ: Type
ℤˣ) : 
u: ℤˣ
u * 
u: ℤˣ
u = 
1: ?m.1441
1 := by
Goals accomplished! 🐙 
u: ℤˣ

u * u = 1rw [
u: ℤˣ

u * u = 1← 
sq: ∀ {M : Type ?u.2331} [inst : Monoid M] (a : M), a ^ 2 = a * a
sq,
u: ℤˣ

u ^ 2 = 1 
u: ℤˣ

u * u = 1
units_sq: ∀ (u : ℤˣ), u ^ 2 = 1
units_sq
u: ℤˣ

1 = 1]
Goals accomplished! 🐙
#align int.units_mul_self 
Int.units_mul_self: ∀ (u : ℤˣ), u * u = 1
Int.units_mul_self

@[simp]
theorem 
units_inv_eq_self: ∀ (u : ℤˣ), u⁻¹ = u
units_inv_eq_self (
u: ℤˣ
u : 
ℤ: Type
ℤˣ) : 
u: ℤˣ
u⁻¹ = 
u: ℤˣ
u := by
Goals accomplished! 🐙 
u: ℤˣ

u⁻¹ = urw [
u: ℤˣ

u⁻¹ = u
inv_eq_iff_mul_eq_one: ∀ {G : Type ?u.2636} [inst : Group G] {a b : G}, a⁻¹ = b ↔ a * b = 1
inv_eq_iff_mul_eq_one,
u: ℤˣ

u * u = 1 
u: ℤˣ

u⁻¹ = u
units_mul_self: ∀ (u : ℤˣ), u * u = 1
units_mul_self
u: ℤˣ

1 = 1]
Goals accomplished! 🐙
#align int.units_inv_eq_self 
Int.units_inv_eq_self: ∀ (u : ℤˣ), u⁻¹ = u
Int.units_inv_eq_self

-- `Units.val_mul` is a "wrong turn" for the simplifier, this undoes it and simplifies further
@[simp]
theorem 
units_coe_mul_self: ∀ (u : ℤˣ), ↑u * ↑u = 1
units_coe_mul_self (
u: ℤˣ
u : 
ℤ: Type
ℤˣ) : (
u: ℤˣ
u * 
u: ℤˣ
u : 
ℤ: Type
ℤ) = 
1: ?m.5822
1 := by
Goals accomplished! 🐙
  
u: ℤˣ

↑u * ↑u = 1rw [
u: ℤˣ

↑u * ↑u = 1← 
Units.val_mul: ∀ {α : Type ?u.5850} [inst : Monoid α] (a b : αˣ), ↑(a * b) = ↑a * ↑b
Units.val_mul,
u: ℤˣ

↑(u * u) = 1 
u: ℤˣ

↑u * ↑u = 1
units_mul_self: ∀ (u : ℤˣ), u * u = 1
units_mul_self,
u: ℤˣ

↑1 = 1 
u: ℤˣ

↑u * ↑u = 1
Units.val_one: ∀ {α : Type ?u.5909} [inst : Monoid α], ↑1 = 1
Units.val_one
u: ℤˣ

1 = 1]
Goals accomplished! 🐙
#align int.units_coe_mul_self 
Int.units_coe_mul_self: ∀ (u : ℤˣ), ↑u * ↑u = 1
Int.units_coe_mul_self

@[simp]
theorem 
neg_one_pow_ne_zero: ∀ {n : ℕ}, (-1) ^ n ≠ 0
neg_one_pow_ne_zero {
n: ℕ
n : 
ℕ: Type
ℕ} : (-
1: ?m.6040
1 : 
ℤ: Type
ℤ) ^ 
n: ℕ
n ≠ 
0: ?m.6215
0 :=
  
pow_ne_zero: ∀ {M : Type ?u.6224} [inst : MonoidWithZero M] [inst_1 : NoZeroDivisors M] {a : M} (n : ℕ), a ≠ 0 → a ^ n ≠ 0
pow_ne_zero 
_: ℕ
_ (
abs_pos: ∀ {α : Type ?u.6311} [inst : AddGroup α] [inst_1 : LinearOrder α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, 0 < abs a ↔ a ≠ 0
abs_pos.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp (by
Goals accomplished! 🐙 
n: ℕ

0 < abs (-1)simp
Goals accomplished! 🐙))
#align int.neg_one_pow_ne_zero 
Int.neg_one_pow_ne_zero: ∀ {n : ℕ}, (-1) ^ n ≠ 0
Int.neg_one_pow_ne_zero

theorem 
sq_eq_one_of_sq_lt_four: ∀ {x : ℤ}, x ^ 2 < 4 → x ≠ 0 → x ^ 2 = 1
sq_eq_one_of_sq_lt_four {
x: ℤ
x : 
ℤ: Type
ℤ} (
h1: x ^ 2 < 4
h1 : 
x: ℤ
x ^ 
2: ?m.6664
2 < 
4: ?m.6678
4) (
h2: x ≠ 0
h2 : 
x: ℤ
x ≠ 
0: ?m.6830
0) : 
x: ℤ
x ^ 
2: ?m.6843
2 = 
1: ?m.6857
1 :=
  
sq_eq_one_iff: ∀ {R : Type ?u.7036} [inst : Ring R] {a : R} [inst_1 : NoZeroDivisors R], a ^ 2 = 1 ↔ a = 1 ∨ a = -1
sq_eq_one_iff.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
    ((
abs_eq: ∀ {α : Type ?u.7090} [inst : LinearOrderedAddCommGroup α] {a b : α}, 0 ≤ b → (abs a = b ↔ a = b ∨ a = -b)
abs_eq (
zero_le_one': ∀ (α : Type ?u.7095) [inst : Zero α] [inst_1 : One α] [inst_2 : LE α] [inst_3 : ZeroLEOneClass α], 0 ≤ 1
zero_le_one' 
ℤ: Type
ℤ)).
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp
      (
le_antisymm: ∀ {α : Type ?u.7331} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm (
lt_add_one_iff: ∀ {a b : ℤ}, a < b + 1 ↔ a ≤ b
lt_add_one_iff.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp (
abs_lt_of_sq_lt_sq: ∀ {R : Type ?u.7406} [inst : LinearOrderedRing R] {x y : R}, x ^ 2 < y ^ 2 → 0 ≤ y → abs x < y
abs_lt_of_sq_lt_sq 
h1: x ^ 2 < 4
h1 
zero_le_two: ∀ {α : Type ?u.7506} [inst : AddMonoidWithOne α] [inst_1 : Preorder α] [inst_2 : ZeroLEOneClass α]
  [inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 0 ≤ 2
zero_le_two))
        (
sub_one_lt_iff: ∀ {a b : ℤ}, a - 1 < b ↔ a ≤ b
sub_one_lt_iff.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp (
abs_pos: ∀ {α : Type ?u.7839} [inst : AddGroup α] [inst_1 : LinearOrder α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, 0 < abs a ↔ a ≠ 0
abs_pos.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr 
h2: x ≠ 0
h2))))
#align int.sq_eq_one_of_sq_lt_four 
Int.sq_eq_one_of_sq_lt_four: ∀ {x : ℤ}, x ^ 2 < 4 → x ≠ 0 → x ^ 2 = 1
Int.sq_eq_one_of_sq_lt_four

theorem 
sq_eq_one_of_sq_le_three: ∀ {x : ℤ}, x ^ 2 ≤ 3 → x ≠ 0 → x ^ 2 = 1
sq_eq_one_of_sq_le_three {
x: ℤ
x : 
ℤ: Type
ℤ} (
h1: x ^ 2 ≤ 3
h1 : 
x: ℤ
x ^ 
2: ?m.8089
2 ≤ 
3: ?m.8103
3) (
h2: x ≠ 0
h2 : 
x: ℤ
x ≠ 
0: ?m.8255
0) : 
x: ℤ
x ^ 
2: ?m.8268
2 = 
1: ?m.8282
1 :=
  
sq_eq_one_of_sq_lt_four: ∀ {x : ℤ}, x ^ 2 < 4 → x ≠ 0 → x ^ 2 = 1
sq_eq_one_of_sq_lt_four (
lt_of_le_of_lt: ∀ {α : Type ?u.8471} [inst : Preorder α] {a b c : α}, a ≤ b → b < c → a < c
lt_of_le_of_lt 
h1: x ^ 2 ≤ 3
h1 (
lt_add_one: ∀ {α : Type ?u.8552} [inst : One α] [inst_1 : AddZeroClass α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
  [inst_4 : NeZero 1] [inst_5 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α), a < a + 1
lt_add_one (
3: ?m.8562
3 : 
ℤ: Type
ℤ))) 
h2: x ≠ 0
h2
#align int.sq_eq_one_of_sq_le_three 
Int.sq_eq_one_of_sq_le_three: ∀ {x : ℤ}, x ^ 2 ≤ 3 → x ≠ 0 → x ^ 2 = 1
Int.sq_eq_one_of_sq_le_three

theorem 
units_pow_eq_pow_mod_two: ∀ (u : ℤˣ) (n : ℕ), u ^ n = u ^ (n % 2)
units_pow_eq_pow_mod_two (
u: ℤˣ
u : 
ℤ: Type
ℤˣ) (
n: ℕ
n : 
ℕ: Type
ℕ) : 
u: ℤˣ
u ^ 
n: ℕ
n = 
u: ℤˣ
u ^ (
n: ℕ
n % 
2: ?m.8912
2) := by
Goals accomplished! 🐙
  
u: ℤˣ

n: ℕ

u ^ n = u ^ (n % 2)conv =>
u: ℤˣ

n: ℕ

u ^ (n % 2)
      
u: ℤˣ

n: ℕ

u ^ n = u ^ (n % 2)lhs
u: ℤˣ

n: ℕ

u ^ n
      
u: ℤˣ

n: ℕ

u ^ n = u ^ (n % 2)rw [
u: ℤˣ

n: ℕ

u ^ n← 
Nat.mod_add_div: ∀ (m k : ℕ), m % k + k * (m / k) = m
Nat.mod_add_div 
n: ℕ
n 
2: ?m.12802
2
u: ℤˣ

n: ℕ

u ^ (n % 2 + 2 * (n / 2))]
u: ℤˣ

n: ℕ

u ^ (n % 2 + 2 * (n / 2));
u: ℤˣ

n: ℕ

u ^ (n % 2 + 2 * (n / 2))
      
u: ℤˣ

n: ℕ

u ^ n = u ^ (n % 2)rw [
u: ℤˣ

n: ℕ

u ^ (n % 2 + 2 * (n / 2))
pow_add: ∀ {M : Type ?u.12807} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
pow_add,
u: ℤˣ

n: ℕ

u ^ (n % 2) * u ^ (2 * (n / 2)) 
u: ℤˣ

n: ℕ

u ^ (n % 2 + 2 * (n / 2))
pow_mul: ∀ {M : Type ?u.13038} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ m) ^ n
pow_mul,
u: ℤˣ

n: ℕ

u ^ (n % 2) * (u ^ 2) ^ (n / 2) 
u: ℤˣ

n: ℕ

u ^ (n % 2 + 2 * (n / 2))
units_sq: ∀ (u : ℤˣ), u ^ 2 = 1
units_sq,
u: ℤˣ

n: ℕ

u ^ (n % 2) * 1 ^ (n / 2) 
u: ℤˣ

n: ℕ

u ^ (n % 2 + 2 * (n / 2))
one_pow: ∀ {M : Type ?u.13124} [inst : Monoid M] (n : ℕ), 1 ^ n = 1
one_pow,
u: ℤˣ

n: ℕ

u ^ (n % 2) * 1 
u: ℤˣ

n: ℕ

u ^ (n % 2 + 2 * (n / 2))
mul_one: ∀ {M : Type ?u.13243} [inst : MulOneClass M] (a : M), a * 1 = a
mul_one
u: ℤˣ

n: ℕ

u ^ (n % 2)]
u: ℤˣ

n: ℕ

u ^ (n % 2)
#align int.units_pow_eq_pow_mod_two 
Int.units_pow_eq_pow_mod_two: ∀ (u : ℤˣ) (n : ℕ), u ^ n = u ^ (n % 2)
Int.units_pow_eq_pow_mod_two

end Int