feat: port Data.Int.Units (#807)

mathlib3 SHA: 62a5626868683c104774de8d85b9855234ac807c

I'm a bit confused about the choice of indenting that mathport uses in proofs - I've tried to copy it, but I can't find any documentation to explain a preferred style in Lean 4. I also added a missing `#align` in `Algebra.Group.Units`.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: zeramorphic

Mathlib.lean

@@ -79,6 +79,7 @@ import Mathlib.Data.Int.Cast
 import Mathlib.Data.Int.Cast.Basic
 import Mathlib.Data.Int.Cast.Defs
 import Mathlib.Data.Int.Order.Basic
+import Mathlib.Data.Int.Units
 import Mathlib.Data.KVMap
 import Mathlib.Data.LazyList
 import Mathlib.Data.List.Basic

Mathlib/Algebra/Group/Units.lean

@@ -614,6 +614,8 @@ namespace IsUnit
 theorem mul_iff [CommMonoid M] {x y : M} : IsUnit (x * y) ↔ IsUnit x ∧ IsUnit y :=
   ⟨fun h => ⟨isUnit_of_mul_isUnit_left h, isUnit_of_mul_isUnit_right h⟩,
    fun h => IsUnit.mul h.1 h.2⟩
+#align is_unit.mul_iff IsUnit.mul_iff
+#align is_add_unit.add_iff IsAddUnit.add_iff
 
 section Monoid
 

Mathlib/Data/Int/Units.lean

@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad
+-/
+import Mathlib.Data.Nat.Units
+import Mathlib.Data.Int.Basic
+import Mathlib.Algebra.Ring.Units
+
+/-!
+# Lemmas about units in `ℤ`.
+-/
+
+
+namespace Int
+
+/-! ### units -/
+
+@[simp]
+theorem units_natAbs (u : ℤˣ) : natAbs u = 1 :=
+  Units.ext_iff.1 <|
+    Nat.units_eq_one
+      ⟨natAbs u, natAbs ↑u⁻¹, by rw [← natAbs_mul, Units.mul_inv]; rfl, by
+        rw [← natAbs_mul, Units.inv_mul]; rfl⟩
+#align int.units_nat_abs Int.units_natAbs
+
+theorem units_eq_one_or (u : ℤˣ) : u = 1 ∨ u = -1 := by
+  simpa only [Units.ext_iff, units_natAbs] using natAbs_eq u
+#align int.units_eq_one_or Int.units_eq_one_or
+
+theorem isUnit_eq_one_or {a : ℤ} : IsUnit a → a = 1 ∨ a = -1
+  | ⟨_, hx⟩ => hx ▸ (units_eq_one_or _).imp (congr_arg Units.val) (congr_arg Units.val)
+#align int.is_unit_eq_one_or Int.isUnit_eq_one_or
+
+theorem isUnit_iff {a : ℤ} : IsUnit a ↔ a = 1 ∨ a = -1 := by
+  refine' ⟨fun h => isUnit_eq_one_or h, fun h => _⟩
+  rcases h with (rfl | rfl)
+  · exact isUnit_one
+  · exact isUnit_one.neg
+#align int.is_unit_iff Int.isUnit_iff
+
+theorem isUnit_eq_or_eq_neg {a b : ℤ} (ha : IsUnit a) (hb : IsUnit b) : a = b ∨ a = -b := by
+  rcases isUnit_eq_one_or hb with (rfl | rfl)
+  · exact isUnit_eq_one_or ha
+  · rwa [or_comm, neg_neg, ← isUnit_iff]
+#align int.is_unit_eq_or_eq_neg Int.isUnit_eq_or_eq_neg
+
+theorem eq_one_or_neg_one_of_mul_eq_one {z w : ℤ} (h : z * w = 1) : z = 1 ∨ z = -1 :=
+  isUnit_iff.mp (isUnit_of_mul_eq_one z w h)
+#align int.eq_one_or_neg_one_of_mul_eq_one Int.eq_one_or_neg_one_of_mul_eq_one
+
+-- Porting note: this was proven in mathlib3 with `tauto` which hasn't been ported yet
+theorem eq_one_or_neg_one_of_mul_eq_one' {z w : ℤ} (h : z * w = 1) :
+    z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1 := by
+  have h' : w * z = 1 := mul_comm z w ▸ h
+  rcases eq_one_or_neg_one_of_mul_eq_one h with (rfl | rfl) <;>
+      rcases eq_one_or_neg_one_of_mul_eq_one h' with (rfl | rfl) <;>
+    try cases h
+  · exact Or.inl ⟨rfl, rfl⟩
+  · exact Or.inr ⟨rfl, rfl⟩
+#align int.eq_one_or_neg_one_of_mul_eq_one' Int.eq_one_or_neg_one_of_mul_eq_one'
+
+theorem mul_eq_one_iff_eq_one_or_neg_one {z w : ℤ} : z * w = 1 ↔ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1 :=
+  by
+  refine' ⟨eq_one_or_neg_one_of_mul_eq_one', fun h => Or.elim h (fun H => _) fun H => _⟩ <;>
+      rcases H with ⟨rfl, rfl⟩ <;>
+    rfl
+#align int.mul_eq_one_iff_eq_one_or_neg_one Int.mul_eq_one_iff_eq_one_or_neg_one
+
+theorem eq_one_or_neg_one_of_mul_eq_neg_one' {z w : ℤ} (h : z * w = -1) :
+    z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1 := by
+  rcases isUnit_eq_one_or (IsUnit.mul_iff.mp (Int.isUnit_iff.mpr (Or.inr h))).1 with (rfl | rfl)
+  · exact Or.inl ⟨rfl, one_mul w ▸ h⟩
+  · exact Or.inr ⟨rfl, neg_inj.mp (neg_one_mul w ▸ h)⟩
+#align int.eq_one_or_neg_one_of_mul_eq_neg_one' Int.eq_one_or_neg_one_of_mul_eq_neg_one'
+
+theorem mul_eq_neg_one_iff_eq_one_or_neg_one {z w : ℤ} :
+    z * w = -1 ↔ z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1 := by
+  refine' ⟨eq_one_or_neg_one_of_mul_eq_neg_one', fun h => Or.elim h (fun H => _) fun H => _⟩ <;>
+      rcases H with ⟨rfl, rfl⟩ <;>
+    rfl
+#align int.mul_eq_neg_one_iff_eq_one_or_neg_one Int.mul_eq_neg_one_iff_eq_one_or_neg_one
+
+theorem isUnit_iff_natAbs_eq {n : ℤ} : IsUnit n ↔ n.natAbs = 1 := by
+  simp [natAbs_eq_iff, isUnit_iff, Nat.cast_zero]
+#align int.is_unit_iff_nat_abs_eq Int.isUnit_iff_natAbs_eq
+
+alias isUnit_iff_natAbs_eq ↔ isUnit.natAbs_eq _
+
+-- Porting note: `rw` didn't work on `natAbs_ofNat`, so had to change to `simp`,
+-- presumably because `(n : ℤ)` is `Nat.cast` and not just `ofNat`
+@[norm_cast]
+theorem ofNat_isUnit {n : ℕ} : IsUnit (n : ℤ) ↔ IsUnit n := by
+  simp [isUnit_iff_natAbs_eq]
+#align int.of_nat_is_unit Int.ofNat_isUnit
+
+theorem isUnit_mul_self {a : ℤ} (ha : IsUnit a) : a * a = 1 :=
+  (isUnit_eq_one_or ha).elim (fun h => h.symm ▸ rfl) fun h => h.symm ▸ rfl
+#align int.is_unit_mul_self Int.isUnit_mul_self
+
+-- Porting note: this was proven in mathlib3 with `tidy` which hasn't been ported yet
+theorem isUnit_add_isUnit_eq_isUnit_add_isUnit {a b c d : ℤ} (ha : IsUnit a) (hb : IsUnit b)
+    (hc : IsUnit c) (hd : IsUnit d) : a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c := by
+  rw [isUnit_iff] at ha hb hc hd
+  cases ha <;> cases hb <;> cases hc <;> cases hd <;>
+      subst a <;> subst b <;> subst c <;> subst d <;>
+    simp
+#align int.is_unit_add_is_unit_eq_is_unit_add_is_unit Int.isUnit_add_isUnit_eq_isUnit_add_isUnit
+
+theorem eq_one_or_neg_one_of_mul_eq_neg_one {z w : ℤ} (h : z * w = -1) : z = 1 ∨ z = -1 :=
+  Or.elim (eq_one_or_neg_one_of_mul_eq_neg_one' h) (fun H => Or.inl H.1) fun H => Or.inr H.1
+#align int.eq_one_or_neg_one_of_mul_eq_neg_one Int.eq_one_or_neg_one_of_mul_eq_neg_one
+
+end Int

Mathlib/Init/Data/Int/Basic.lean

@@ -85,6 +85,8 @@ protected theorem neg_eq_neg {a b : ℤ} (h : -a = -b) : a = b := Int.neg_inj.1
 #align int.sub_nat_nat_of_lt Int.subNatNat_of_lt
 #align int.nat_abs_of_nat Int.natAbs_ofNat
 
+#align int.nat_abs Int.natAbs
+
 @[deprecated natAbs_eq_zero]
 theorem eq_zero_of_natAbs_eq_zero : ∀ {a : ℤ}, natAbs a = 0 → a = 0 := natAbs_eq_zero.1
 #align int.eq_zero_of_nat_abs_eq_zero Int.eq_zero_of_natAbs_eq_zero