feat(Algebra/Group/Subgroup/ZPowers): add Int.closure_eq_zmultiples (leanprover-community#39435)

- Show that for `a b : ℤ`, `AddSubgroup.closure {a, b} = AddSubgroup.zmultiples (a.gcd b : ℤ)`
- Used Claude to find the names of relevant theorems to use. However, I wrote the whole proof on my own.

Co-authored-by: tdM05 <taddmao@gmail.com>

Author: tdM05

Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean

@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Group.Subgroup.Ker
 public import Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
 public import Mathlib.Data.Countable.Basic
 public import Mathlib.Data.Int.Cast.Lemmas
+public import Mathlib.Data.Int.GCD
 
 /-!
 # Subgroups generated by an element
@@ -69,4 +70,9 @@ lemma range_nsmulAddMonoidHom (n : ℕ) : (nsmulAddMonoidHom n).range = zmultipl
   simp [mem_zmultiples_iff, dvd_def]
   grind
 
+theorem closure_eq_zmultiples (a b : ℤ) : closure {a, b} = zmultiples (a.gcd b : ℤ) := by
+  apply le_antisymm
+  · grind [closure_le, mem_zmultiples_iff, SetLike.mem_coe, gcd_dvd_left, gcd_dvd_right]
+  · simp [zmultiples_le, mem_closure_pair, gcd_eq_gcd_ab, mul_comm]
+
 end Int