feat: forward-port leanprover-community/mathlib#18359 (#2106)

Also fixes a lemma statement to use `%` notation like it did in Lean3



Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

Mathlib/Data/Int/Order/Basic.lean

@@ -4,7 +4,7 @@ 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.basic
-! leanprover-community/mathlib commit b86832321b586c6ac23ef8cdef6a7a27e42b13bd
+! leanprover-community/mathlib commit bd835ef554f37ef9b804f0903089211f89cb370b
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -272,6 +272,8 @@ theorem add_emod_eq_add_mod_right {m n k : ℤ} (i : ℤ) (H : m % n = k % n) :
 
 #align int.sub_mod Int.sub_emod
 
+-- porting note: this should be a doc comment, but the lemma isn't here any more!
+/- See also `Int.divModEquiv` for a similar statement as an `Equiv`. -/
 #align int.div_mod_unique Int.ediv_emod_unique
 
 attribute [local simp] Int.zero_emod

Mathlib/Data/Nat/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.nat.basic
-! leanprover-community/mathlib commit 2609ad04e2b77aceb2200e273daf11cc65856fda
+! leanprover-community/mathlib commit bd835ef554f37ef9b804f0903089211f89cb370b
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -716,6 +716,7 @@ theorem div_add_mod' (m k : ℕ) : m / k * k + m % k = m := by
   exact div_add_mod _ _
 #align nat.div_add_mod' Nat.div_add_mod'
 
+/-- See also `Nat.divModEquiv` for a similar statement as an `Equiv`. -/
 protected theorem div_mod_unique {n k m d : ℕ} (h : 0 < k) :
     n / k = d ∧ n % k = m ↔ m + k * d = n ∧ m < k :=
   ⟨fun ⟨e₁, e₂⟩ => e₁ ▸ e₂ ▸ ⟨mod_add_div _ _, mod_lt _ h⟩, fun ⟨h₁, h₂⟩ =>

Mathlib/GroupTheory/Perm/Cycle/Basic.lean

@@ -914,7 +914,7 @@ theorem IsCycleOn.exists_pow_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈
     obtain ⟨n, rfl⟩ := hf.2 ha hb
     obtain ⟨k, hk⟩ := (Int.mod_modEq n s.card).symm.dvd
     refine' ⟨n.natMod s.card, Int.natMod_lt (Nonempty.card_pos ⟨a, ha⟩).ne', _⟩
-    rw [← zpow_ofNat, Int.natMod, ← Int.mod_def',
+    rw [← zpow_ofNat, Int.natMod,
       Int.toNat_of_nonneg (Int.emod_nonneg _ <| Nat.cast_ne_zero.2
         (Nonempty.card_pos ⟨a, ha⟩).ne'),  sub_eq_iff_eq_add'.1 hk, zpow_add, zpow_mul]
     simp only [zpow_coe_nat, coe_mul, comp_apply, EmbeddingLike.apply_eq_iff_eq]

Mathlib/Init/Data/Int/Basic.lean

@@ -129,7 +129,7 @@ theorem natAbs_pos_of_ne_zero {a : ℤ} (h : a ≠ 0) : 0 < natAbs a := natAbs_p
 #align int.to_nat_sub Int.toNat_sub
 
 /-- The modulus of an integer by another as a natural. Uses the E-rounding convention. -/
-def natMod (m n : ℤ) : ℕ := (m.emod n).toNat
+def natMod (m n : ℤ) : ℕ := (m % n).toNat
 #align int.nat_mod Int.natMod
 
 #align int.sign_mul_nat_abs Int.sign_mul_natAbs

Mathlib/Logic/Equiv/Fin.lean

@@ -4,11 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 
 ! This file was ported from Lean 3 source module logic.equiv.fin
-! leanprover-community/mathlib commit 2445c98ae4b87eabebdde552593519b9b6dc350c
+! leanprover-community/mathlib commit bd835ef554f37ef9b804f0903089211f89cb370b
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Data.Fin.VecNotation
+import Mathlib.Data.Int.Order.Basic
 import Mathlib.Logic.Equiv.Defs
 
 /-!
@@ -491,6 +492,41 @@ def finProdFinEquiv : Fin m × Fin n ≃ Fin (m * n)
 #align fin_prod_fin_equiv_apply_val finProdFinEquiv_apply_val
 #align fin_prod_fin_equiv_symm_apply finProdFinEquiv_symm_apply
 
+/-- The equivalence induced by `a ↦ (a / n, a % n)` for nonzero `n`.
+This is like `finProdFinEquiv.symm` but with `m` infinite.
+See `Nat.div_mod_unique` for a similar propositional statement. -/
+@[simps]
+def Nat.divModEquiv (n : ℕ) [NeZero n] : ℕ ≃ ℕ × Fin n where
+  toFun a := (a / n, ↑a)
+  invFun p := p.1 * n + ↑p.2
+  -- TODO: is there a canonical order of `*` and `+` here?
+  left_inv a := Nat.div_add_mod' _ _
+  right_inv p := by
+    refine' Prod.ext _ (Fin.ext <| Nat.mul_add_mod_of_lt p.2.is_lt)
+    dsimp only
+    rw [add_comm, Nat.add_mul_div_right _ _ (NeZero.pos n), Nat.div_eq_of_lt p.2.is_lt, zero_add]
+#align nat.div_mod_equiv Nat.divModEquiv
+
+/-- The equivalence induced by `a ↦ (a / n, a % n)` for nonzero `n`.
+See `Int.ediv_emod_unique` for a similar propositional statement. -/
+@[simps]
+def Int.divModEquiv (n : ℕ) [NeZero n] : ℤ ≃ ℤ × Fin n where
+  -- TODO: could cast from int directly if we import `data.zmod.defs`, though there are few lemmas
+  -- about that coercion.
+  toFun a := (a / n, ↑(a.natMod n))
+  invFun p := p.1 * n + ↑p.2
+  left_inv a := by
+    simp_rw [Fin.coe_ofNat_eq_mod, Int.coe_nat_mod, Int.natMod,
+      Int.toNat_of_nonneg (Int.emod_nonneg _ <| NeZero.ne ↑n), Int.emod_emod,
+      Int.ediv_add_emod']
+  right_inv := fun ⟨q, r, hrn⟩ => by
+    simp only [Fin.val_mk, Prod.mk.inj_iff, Fin.ext_iff]
+    obtain ⟨h1, h2⟩ := Int.coe_nat_nonneg r, Int.ofNat_lt.2 hrn
+    rw [add_comm, Int.add_mul_ediv_right _ _ (NeZero.ne ↑n), Int.ediv_eq_zero_of_lt h1 h2,
+      Int.natMod, Int.add_mul_emod_self, Int.emod_eq_of_lt h1 h2, Int.toNat_coe_nat]
+    exact ⟨zero_add q, Fin.val_cast_of_lt hrn⟩
+#align int.div_mod_equiv Int.divModEquiv
+
 /-- Promote a `Fin n` into a larger `Fin m`, as a subtype where the underlying
 values are retained. This is the `OrderIso` version of `Fin.castLe`. -/
 @[simps apply symm_apply]