feat: porting norm_num extensions for Nat.gcd, Nat.lcm, Int.gcd…

…, `Int.lcm`, and `IsCoprime` (#3923)

This completes the porting of these norm_num extensions while adding a new extension for `IsCoprime` over `Int`. It also adds the norm_num extension testing file from mathlib3. Closes #3246.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Mathlib.lean

@@ -1923,6 +1923,8 @@ import Mathlib.Tactic.NormCast.Tactic
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.NormNum.Basic
 import Mathlib.Tactic.NormNum.Core
+import Mathlib.Tactic.NormNum.GCD
+import Mathlib.Tactic.NormNum.IsCoprime
 import Mathlib.Tactic.NthRewrite
 import Mathlib.Tactic.PermuteGoals
 import Mathlib.Tactic.Polyrith

Mathlib/Data/Int/GCD.lean

@@ -9,10 +9,10 @@ Authors: Sangwoo Jo (aka Jason), Guy Leroy, Johannes Hölzl, Mario Carneiro
 ! if you have ported upstream changes.
 -/
 import Mathlib.Data.Nat.GCD.Basic
+import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Algebra.Ring.Regular
 import Mathlib.Data.Int.Dvd.Basic
 import Mathlib.Order.Bounds.Basic
-import Mathlib.Tactic.NormNum
 
 /-!
 # Extended GCD and divisibility over ℤ
@@ -179,6 +179,8 @@ end Nat
 
 namespace Int
 
+theorem gcd_def (i j : ℤ) : gcd i j = Nat.gcd i.natAbs j.natAbs := rfl
+
 protected theorem coe_nat_gcd (m n : ℕ) : Int.gcd ↑m ↑n = Nat.gcd m n :=
   rfl
 #align int.coe_nat_gcd Int.coe_nat_gcd
@@ -508,258 +510,3 @@ theorem pow_gcd_eq_one {M : Type _} [Monoid M] (x : M) {m n : ℕ} (hm : x ^ m =
   simp only [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, hm, hn, one_zpow, one_mul]
 #align pow_gcd_eq_one pow_gcd_eq_one
 #align gcd_nsmul_eq_zero gcd_nsmul_eq_zero
-
-/-! ### GCD prover -/
-
--- open NormNum
-
--- namespace Tactic
-
--- namespace NormNum
-
--- theorem int_gcd_helper' {d : ℕ} {x y a b : ℤ} (h₁ : (d : ℤ) ∣ x) (h₂ : (d : ℤ) ∣ y)
---     (h₃ : x * a + y * b = d) : Int.gcd x y = d := by
---   refine' Nat.dvd_antisymm _ (Int.coe_nat_dvd.1 (Int.dvd_gcd h₁ h₂))
---   rw [← Int.coe_nat_dvd, ← h₃]
---   apply dvd_add
---   · exact (Int.gcd_dvd_left _ _).mul_right _
---   · exact (Int.gcd_dvd_right _ _).mul_right _
--- #align tactic.norm_num.int_gcd_helper' Tactic.NormNum.int_gcd_helper'
-
--- theorem nat_gcd_helper_dvd_left (x y a : ℕ) (h : x * a = y) : Nat.gcd x y = x :=
---   Nat.gcd_eq_left ⟨a, h.symm⟩
--- #align tactic.norm_num.nat_gcd_helper_dvd_left Tactic.NormNum.nat_gcd_helper_dvd_left
-
--- theorem nat_gcd_helper_dvd_right (x y a : ℕ) (h : y * a = x) : Nat.gcd x y = y :=
---   Nat.gcd_eq_right ⟨a, h.symm⟩
--- #align tactic.norm_num.nat_gcd_helper_dvd_right Tactic.NormNum.nat_gcd_helper_dvd_right
-
--- theorem nat_gcd_helper_2 (d x y a b u v tx ty : ℕ) (hu : d * u = x) (hv : d * v = y)
---     (hx : x * a = tx) (hy : y * b = ty) (h : ty + d = tx) : Nat.gcd x y = d := by
---   rw [← Int.coe_nat_gcd];
---   apply
---     @int_gcd_helper' _ _ _ a (-b) (Int.coe_nat_dvd.2 ⟨_, hu.symm⟩) (Int.coe_nat_dvd.2
---      ⟨_, hv.symm⟩)
---   rw [mul_neg, ← sub_eq_add_neg, sub_eq_iff_eq_add']
---   norm_cast; rw [hx, hy, h]
--- #align tactic.norm_num.nat_gcd_helper_2 Tactic.NormNum.nat_gcd_helper_2
-
--- theorem nat_gcd_helper_1 (d x y a b u v tx ty : ℕ) (hu : d * u = x) (hv : d * v = y)
---     (hx : x * a = tx) (hy : y * b = ty) (h : tx + d = ty) : Nat.gcd x y = d :=
---   (Nat.gcd_comm _ _).trans <| nat_gcd_helper_2 _ _ _ _ _ _ _ _ _ hv hu hy hx h
--- #align tactic.norm_num.nat_gcd_helper_1 Tactic.NormNum.nat_gcd_helper_1
-
--- --Porting note: the `simp only` was not necessary in Lean3.
--- theorem nat_lcm_helper (x y d m n : ℕ) (hd : Nat.gcd x y = d) (d0 : 0 < d) (xy : x * y = n)
---     (dm : d * m = n) : Nat.lcm x y = m :=
---   mul_right_injective₀ d0.ne' <| by simp only; rw [dm, ← xy, ← hd, Nat.gcd_mul_lcm]
--- #align tactic.norm_num.nat_lcm_helper Tactic.NormNum.nat_lcm_helper
-
--- theorem nat_coprime_helper_zero_left (x : ℕ) (h : 1 < x) : ¬Nat.coprime 0 x :=
---   mt (Nat.coprime_zero_left _).1 <| ne_of_gt h
--- #align tactic.norm_num.nat_coprime_helper_zero_left Tactic.NormNum.nat_coprime_helper_zero_left
-
--- theorem nat_coprime_helper_zero_right (x : ℕ) (h : 1 < x) : ¬Nat.coprime x 0 :=
---   mt (Nat.coprime_zero_right _).1 <| ne_of_gt h
--- #align tactic.norm_num.nat_coprime_helper_zero_right Tactic.NormNum.nat_coprime_helper_zero_right
-
--- theorem nat_coprime_helper_1 (x y a b tx ty : ℕ) (hx : x * a = tx) (hy : y * b = ty)
---     (h : tx + 1 = ty) : Nat.coprime x y :=
---   nat_gcd_helper_1 _ _ _ _ _ _ _ _ _ (one_mul _) (one_mul _) hx hy h
--- #align tactic.norm_num.nat_coprime_helper_1 Tactic.NormNum.nat_coprime_helper_1
-
--- theorem nat_coprime_helper_2 (x y a b tx ty : ℕ) (hx : x * a = tx) (hy : y * b = ty)
---     (h : ty + 1 = tx) : Nat.coprime x y :=
---   nat_gcd_helper_2 _ _ _ _ _ _ _ _ _ (one_mul _) (one_mul _) hx hy h
--- #align tactic.norm_num.nat_coprime_helper_2 Tactic.NormNum.nat_coprime_helper_2
-
--- theorem nat_not_coprime_helper (d x y u v : ℕ) (hu : d * u = x) (hv : d * v = y) (h : 1 < d) :
---     ¬Nat.coprime x y :=
---   Nat.not_coprime_of_dvd_of_dvd h ⟨_, hu.symm⟩ ⟨_, hv.symm⟩
--- #align tactic.norm_num.nat_not_coprime_helper Tactic.NormNum.nat_not_coprime_helper
-
--- theorem int_gcd_helper (x y : ℤ) (nx ny d : ℕ) (hx : (nx : ℤ) = x) (hy : (ny : ℤ) = y)
---     (h : Nat.gcd nx ny = d) : Int.gcd x y = d := by rwa [← hx, ← hy, Int.coe_nat_gcd]
--- #align tactic.norm_num.int_gcd_helper Tactic.NormNum.int_gcd_helper
-
--- theorem int_gcd_helper_neg_left (x y : ℤ) (d : ℕ) (h : Int.gcd x y = d) : Int.gcd (-x) y = d :=
---  by rw [Int.gcd] at h⊢; rwa [Int.natAbs_neg]
--- #align tactic.norm_num.int_gcd_helper_neg_left Tactic.NormNum.int_gcd_helper_neg_left
-
--- theorem int_gcd_helper_neg_right (x y : ℤ) (d : ℕ) (h : Int.gcd x y = d) : Int.gcd x (-y) = d :=
---  by rw [Int.gcd] at h⊢; rwa [Int.natAbs_neg]
--- #align tactic.norm_num.int_gcd_helper_neg_right Tactic.NormNum.int_gcd_helper_neg_right
-
--- theorem int_lcm_helper (x y : ℤ) (nx ny d : ℕ) (hx : (nx : ℤ) = x) (hy : (ny : ℤ) = y)
---     (h : Nat.lcm nx ny = d) : Int.lcm x y = d := by rwa [← hx, ← hy, Int.coe_nat_lcm]
--- #align tactic.norm_num.int_lcm_helper Tactic.NormNum.int_lcm_helper
-
--- theorem int_lcm_helper_neg_left (x y : ℤ) (d : ℕ) (h : Int.lcm x y = d) : Int.lcm (-x) y = d :=
---  by rw [Int.lcm] at h⊢; rwa [Int.natAbs_neg]
--- #align tactic.norm_num.int_lcm_helper_neg_left Tactic.NormNum.int_lcm_helper_neg_left
-
--- theorem int_lcm_helper_neg_right (x y : ℤ) (d : ℕ) (h : Int.lcm x y = d) : Int.lcm x (-y) = d :=
---  by rw [Int.lcm] at h⊢; rwa [Int.natAbs_neg]
--- #align tactic.norm_num.int_lcm_helper_neg_right Tactic.NormNum.int_lcm_helper_neg_right
-
--- /-- Evaluates the `nat.gcd` function. -/
--- unsafe def prove_gcd_nat (c : instance_cache) (ex ey : expr) :
---     tactic (instance_cache × expr × expr) := do
---   let x ← ex.toNat
---   let y ← ey.toNat
---   match x, y with
---     | 0, _ => pure (c, ey, q(Nat.gcd_zero_left).mk_app [ey])
---     | _, 0 => pure (c, ex, q(Nat.gcd_zero_right).mk_app [ex])
---     | 1, _ => pure (c, q((1 : ℕ)), q(Nat.gcd_one_left).mk_app [ey])
---     | _, 1 => pure (c, q((1 : ℕ)), q(Nat.gcd_one_right).mk_app [ex])
---     | _, _ => do
---       let (d, a, b) := Nat.xgcdAux x 1 0 y 0 1
---       if d = x then do
---           let (c, ea) ← c (y / x)
---           let (c, _, p) ← prove_mul_nat c ex ea
---           pure (c, ex, q(nat_gcd_helper_dvd_left).mk_app [ex, ey, ea, p])
---         else
---           if d = y then do
---             let (c, ea) ← c (x / y)
---             let (c, _, p) ← prove_mul_nat c ey ea
---             pure (c, ey, q(nat_gcd_helper_dvd_right).mk_app [ex, ey, ea, p])
---           else do
---             let (c, ed) ← c d
---             let (c, ea) ← c a
---             let (c, eb) ← c b
---             let (c, eu) ← c (x / d)
---             let (c, ev) ← c (y / d)
---             let (c, _, pu) ← prove_mul_nat c ed eu
---             let (c, _, pv) ← prove_mul_nat c ed ev
---             let (c, etx, px) ← prove_mul_nat c ex ea
---             let (c, ety, py) ← prove_mul_nat c ey eb
---             let (c, p) ← if a ≥ 0 then prove_add_nat c ety ed etx else prove_add_nat c etx ed ety
---             let pf : expr := if a ≥ 0 then q(nat_gcd_helper_2) else q(nat_gcd_helper_1)
---             pure (c, ed, pf [ed, ex, ey, ea, eb, eu, ev, etx, ety, pu, pv, px, py, p])
--- #align tactic.norm_num.prove_gcd_nat tactic.norm_num.prove_gcd_nat
-
--- /-- Evaluates the `nat.lcm` function. -/
--- unsafe def prove_lcm_nat (c : instance_cache) (ex ey : expr) :
---     tactic (instance_cache × expr × expr) := do
---   let x ← ex.toNat
---   let y ← ey.toNat
---   match x, y with
---     | 0, _ => pure (c, q((0 : ℕ)), q(Nat.lcm_zero_left).mk_app [ey])
---     | _, 0 => pure (c, q((0 : ℕ)), q(Nat.lcm_zero_right).mk_app [ex])
---     | 1, _ => pure (c, ey, q(Nat.lcm_one_left).mk_app [ey])
---     | _, 1 => pure (c, ex, q(Nat.lcm_one_right).mk_app [ex])
---     | _, _ => do
---       let (c, ed, pd) ← prove_gcd_nat c ex ey
---       let (c, p0) ← prove_pos c ed
---       let (c, en, xy) ← prove_mul_nat c ex ey
---       let d ← ed
---       let (c, em) ← c (x * y / d)
---       let (c, _, dm) ← prove_mul_nat c ed em
---       pure (c, em, q(nat_lcm_helper).mk_app [ex, ey, ed, em, en, pd, p0, xy, dm])
--- #align tactic.norm_num.prove_lcm_nat tactic.norm_num.prove_lcm_nat
-
--- /-- Evaluates the `int.gcd` function. -/
--- unsafe def prove_gcd_int (zc nc : instance_cache) :
---     expr → expr → tactic (instance_cache × instance_cache × expr × expr)
---   | x, y =>
---     match match_neg x with
---     | some x => do
---       let (zc, nc, d, p) ← prove_gcd_int x y
---       pure (zc, nc, d, q(int_gcd_helper_neg_left).mk_app [x, y, d, p])
---     | none =>
---       match match_neg y with
---       | some y => do
---         let (zc, nc, d, p) ← prove_gcd_int x y
---         pure (zc, nc, d, q(int_gcd_helper_neg_right).mk_app [x, y, d, p])
---       | none => do
---         let (zc, nc, nx, px) ← prove_nat_uncast zc nc x
---         let (zc, nc, ny, py) ← prove_nat_uncast zc nc y
---         let (nc, d, p) ← prove_gcd_nat nc nx ny
---         pure (zc, nc, d, q(int_gcd_helper).mk_app [x, y, nx, ny, d, px, py, p])
--- #align tactic.norm_num.prove_gcd_int tactic.norm_num.prove_gcd_int
-
--- /-- Evaluates the `int.lcm` function. -/
--- unsafe def prove_lcm_int (zc nc : instance_cache) :
---     expr → expr → tactic (instance_cache × instance_cache × expr × expr)
---   | x, y =>
---     match match_neg x with
---     | some x => do
---       let (zc, nc, d, p) ← prove_lcm_int x y
---       pure (zc, nc, d, q(int_lcm_helper_neg_left).mk_app [x, y, d, p])
---     | none =>
---       match match_neg y with
---       | some y => do
---         let (zc, nc, d, p) ← prove_lcm_int x y
---         pure (zc, nc, d, q(int_lcm_helper_neg_right).mk_app [x, y, d, p])
---       | none => do
---         let (zc, nc, nx, px) ← prove_nat_uncast zc nc x
---         let (zc, nc, ny, py) ← prove_nat_uncast zc nc y
---         let (nc, d, p) ← prove_lcm_nat nc nx ny
---         pure (zc, nc, d, q(int_lcm_helper).mk_app [x, y, nx, ny, d, px, py, p])
--- #align tactic.norm_num.prove_lcm_int tactic.norm_num.prove_lcm_int
-
--- /-- Evaluates the `nat.coprime` function. -/
--- unsafe def prove_coprime_nat (c : instance_cache) (ex ey : expr) :
---     tactic (instance_cache × Sum expr expr) := do
---   let x ← ex.toNat
---   let y ← ey.toNat
---   match x, y with
---     | 1, _ => pure (c, Sum.inl <| q(Nat.coprime_one_left).mk_app [ey])
---     | _, 1 => pure (c, Sum.inl <| q(Nat.coprime_one_right).mk_app [ex])
---     | 0, 0 => pure (c, Sum.inr q(Nat.not_coprime_zero_zero))
---     | 0, _ => do
---       let c ← mk_instance_cache q(ℕ)
---       let (c, p) ← prove_lt_nat c q(1) ey
---       pure (c, Sum.inr <| q(nat_coprime_helper_zero_left).mk_app [ey, p])
---     | _, 0 => do
---       let c ← mk_instance_cache q(ℕ)
---       let (c, p) ← prove_lt_nat c q(1) ex
---       pure (c, Sum.inr <| q(nat_coprime_helper_zero_right).mk_app [ex, p])
---     | _, _ => do
---       let c ← mk_instance_cache q(ℕ)
---       let (d, a, b) := Nat.xgcdAux x 1 0 y 0 1
---       if d = 1 then do
---           let (c, ea) ← c a
---           let (c, eb) ← c b
---           let (c, etx, px) ← prove_mul_nat c ex ea
---           let (c, ety, py) ← prove_mul_nat c ey eb
---           let (c, p) ← if a ≥ 0 then
---             prove_add_nat c ety q(1) etx else prove_add_nat c etx q(1) ety
---           let pf : expr := if a ≥ 0 then q(nat_coprime_helper_2) else q(nat_coprime_helper_1)
---           pure (c, Sum.inl <| pf [ex, ey, ea, eb, etx, ety, px, py, p])
---         else do
---           let (c, ed) ← c d
---           let (c, eu) ← c (x / d)
---           let (c, ev) ← c (y / d)
---           let (c, _, pu) ← prove_mul_nat c ed eu
---           let (c, _, pv) ← prove_mul_nat c ed ev
---           let (c, p) ← prove_lt_nat c q(1) ed
---           pure (c, Sum.inr <| q(nat_not_coprime_helper).mk_app [ed, ex, ey, eu, ev, pu, pv, p])
--- #align tactic.norm_num.prove_coprime_nat tactic.norm_num.prove_coprime_nat
-
--- /-- Evaluates the `gcd`, `lcm`, and `coprime` functions. -/
--- @[norm_num]
--- unsafe def eval_gcd : expr → tactic (expr × expr)
---   | q(Nat.gcd $(ex) $(ey)) => do
---     let c ← mk_instance_cache q(ℕ)
---     Prod.snd <$> prove_gcd_nat c ex ey
---   | q(Nat.lcm $(ex) $(ey)) => do
---     let c ← mk_instance_cache q(ℕ)
---     Prod.snd <$> prove_lcm_nat c ex ey
---   | q(Nat.Coprime $(ex) $(ey)) => do
---     let c ← mk_instance_cache q(ℕ)
---     prove_coprime_nat c ex ey >>= Sum.elim true_intro false_intro ∘ Prod.snd
---   | q(Int.gcd $(ex) $(ey)) => do
---     let zc ← mk_instance_cache q(ℤ)
---     let nc ← mk_instance_cache q(ℕ)
---     (Prod.snd ∘ Prod.snd) <$> prove_gcd_int zc nc ex ey
---   | q(Int.lcm $(ex) $(ey)) => do
---     let zc ← mk_instance_cache q(ℤ)
---     let nc ← mk_instance_cache q(ℕ)
---     (Prod.snd ∘ Prod.snd) <$> prove_lcm_int zc nc ex ey
---   | _ => failed
--- #align tactic.norm_num.eval_gcd tactic.norm_num.eval_gcd
-
--- end NormNum
-
--- end Tactic

Mathlib/Data/Nat/ModEq.lean

@@ -10,6 +10,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Data.Int.GCD
 import Mathlib.Data.Int.Order.Lemmas
+import Mathlib.Tactic.NormNum
 
 /-!
 # Congruences modulo a natural number

Mathlib/GroupTheory/Perm/Cycle/Type.lean

@@ -13,6 +13,7 @@ import Mathlib.Combinatorics.Partition
 import Mathlib.Data.List.Rotate
 import Mathlib.GroupTheory.Perm.Cycle.Basic
 import Mathlib.RingTheory.Int.Basic
+import Mathlib.Tactic.NormNum.GCD
 
 /-!
 # Cycle Types
@@ -613,31 +614,9 @@ theorem orderOf {g : Perm α} (ht : IsThreeCycle g) : orderOf g = 3 := by
   rw [← lcm_cycleType, ht.cycleType, Multiset.lcm_singleton, normalize_eq]
 #align equiv.perm.is_three_cycle.order_of Equiv.Perm.IsThreeCycle.orderOf
 
--- Copied the following lemmas from Data/Int/GCD.lean; see #3246
-private theorem int_gcd_helper' {d : ℕ} {x y a b : ℤ} (h₁ : (d : ℤ) ∣ x) (h₂ : (d : ℤ) ∣ y)
-    (h₃ : x * a + y * b = d) : Int.gcd x y = d := by
-  refine' Nat.dvd_antisymm _ (Int.coe_nat_dvd.1 (Int.dvd_gcd h₁ h₂))
-  rw [← Int.coe_nat_dvd, ← h₃]
-  apply dvd_add
-  · exact (Int.gcd_dvd_left _ _).mul_right _
-  · exact (Int.gcd_dvd_right _ _).mul_right _
-private theorem nat_gcd_helper_2 (d x y a b u v tx ty : ℕ) (hu : d * u = x) (hv : d * v = y)
-    (hx : x * a = tx) (hy : y * b = ty) (h : ty + d = tx) : Nat.gcd x y = d := by
-  rw [← Int.coe_nat_gcd];
-  apply
-    @int_gcd_helper' _ _ _ a (-b) (Int.coe_nat_dvd.2 ⟨_, hu.symm⟩) (Int.coe_nat_dvd.2
-     ⟨_, hv.symm⟩)
-  rw [mul_neg, ← sub_eq_add_neg, sub_eq_iff_eq_add']
-  norm_cast; rw [hx, hy, h]
-private theorem nat_gcd_helper_1 (d x y a b u v tx ty : ℕ) (hu : d * u = x) (hv : d * v = y)
-    (hx : x * a = tx) (hy : y * b = ty) (h : tx + d = ty) : Nat.gcd x y = d :=
-  (Nat.gcd_comm _ _).trans <| nat_gcd_helper_2 _ _ _ _ _ _ _ _ _ hv hu hy hx h
-
 theorem isThreeCycle_sq {g : Perm α} (ht : IsThreeCycle g) : IsThreeCycle (g * g) := by
   rw [← pow_two, ← card_support_eq_three_iff, support_pow_coprime, ht.card_support]
-  rw [ht.orderOf, Nat.coprime_iff_gcd_eq_one]
-  -- Porting note: was `norm_num`
-  apply nat_gcd_helper_1 _ _ _ _ _ _ _ _ _ (one_mul _) (one_mul _) (mul_one _) (mul_one _)
+  rw [ht.orderOf]
   norm_num
 #align equiv.perm.is_three_cycle.is_three_cycle_sq Equiv.Perm.IsThreeCycle.isThreeCycle_sq
 

Mathlib/RingTheory/Coprime/Basic.lean

@@ -38,7 +38,6 @@ variable {R : Type u} [CommSemiring R] (x y z : R)
 /-- The proposition that `x` and `y` are coprime, defined to be the existence of `a` and `b` such
 that `a * x + b * y = 1`. Note that elements with no common divisors are not necessarily coprime,
 e.g., the multivariate polynomials `x₁` and `x₂` are not coprime. -/
-@[simp]
 def IsCoprime : Prop :=
   ∃ a b, a * x + b * y = 1
 #align is_coprime IsCoprime

Mathlib/RingTheory/Coprime/Lemmas.lean

@@ -33,18 +33,17 @@ section
 
 open Classical
 
-theorem Nat.isCoprime_iff_coprime {m n : ℕ} : IsCoprime (m : ℤ) n ↔ Nat.coprime m n :=
-  ⟨fun ⟨a, b, H⟩ ↦
-    Nat.eq_one_of_dvd_one <|
-      Int.coe_nat_dvd.1 <| by
-        rw [Int.ofNat_one, ← H]
-        exact
-          dvd_add (dvd_mul_of_dvd_right (Int.coe_nat_dvd.2 <| Nat.gcd_dvd_left m n) _)
-            (dvd_mul_of_dvd_right (Int.coe_nat_dvd.2 <| Nat.gcd_dvd_right m n) _),
-    fun H ↦
-    ⟨Nat.gcdA m n, Nat.gcdB m n, by
-      rw [mul_comm _ (m : ℤ), mul_comm _ (n : ℤ), ← Nat.gcd_eq_gcd_ab, show _ = _ from H,
-        Int.ofNat_one]⟩⟩
+theorem Int.isCoprime_iff_gcd_eq_one {m n : ℤ} : IsCoprime m n ↔ Int.gcd m n = 1 := by
+  constructor
+  · rintro ⟨a, b, h⟩
+    have : 1 = m * a + n * b := by rwa [mul_comm m, mul_comm n, eq_comm]
+    exact Nat.dvd_one.mp (Int.gcd_dvd_iff.mpr ⟨a, b, this⟩)
+  · rw [← Int.ofNat_inj, IsCoprime, Int.gcd_eq_gcd_ab, mul_comm m, mul_comm n, Nat.cast_one]
+    intro h
+    exact ⟨_, _, h⟩
+
+theorem Nat.isCoprime_iff_coprime {m n : ℕ} : IsCoprime (m : ℤ) n ↔ Nat.coprime m n := by
+  rw [Int.isCoprime_iff_gcd_eq_one, Int.coe_nat_gcd]
 #align nat.is_coprime_iff_coprime Nat.isCoprime_iff_coprime
 
 alias Nat.isCoprime_iff_coprime ↔ IsCoprime.nat_coprime Nat.coprime.isCoprime

Mathlib/Tactic.lean

@@ -72,6 +72,8 @@ import Mathlib.Tactic.NormCast.Tactic
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.NormNum.Basic
 import Mathlib.Tactic.NormNum.Core
+import Mathlib.Tactic.NormNum.GCD
+import Mathlib.Tactic.NormNum.IsCoprime
 import Mathlib.Tactic.NthRewrite
 import Mathlib.Tactic.PermuteGoals
 import Mathlib.Tactic.Polyrith