From 506d5951bf201bd35e62e371aff68909bae2e475 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 11 Jul 2026 08:24:49 +0300
Subject: [PATCH] feat: `Commute` and `IsCoprime` are `Std.Symm`

---
 Mathlib/Algebra/Group/Commute/Defs.lean | 4 ++++
 Mathlib/RingTheory/Coprime/Basic.lean   | 3 +++
 2 files changed, 7 insertions(+)

diff --git a/Mathlib/Algebra/Group/Commute/Defs.lean b/Mathlib/Algebra/Group/Commute/Defs.lean
index 6f2ce3d81994b2..94867aebf3fbc5 100644
--- a/Mathlib/Algebra/Group/Commute/Defs.lean
+++ b/Mathlib/Algebra/Group/Commute/Defs.lean
@@ -76,6 +76,10 @@ protected theorem symm_iff {a b : S} : Commute a b ↔ Commute b a :=
 instance : @Std.Refl S Commute :=
   ⟨Commute.refl⟩
 
+@[to_additive]
+instance : @Std.Symm S Commute where
+  symm _ _ := .symm
+
 -- This instance is useful for `Finset.noncommProd`
 @[to_additive]
 instance on_refl {f : G → S} : Std.Refl fun a b => Commute (f a) (f b) :=
diff --git a/Mathlib/RingTheory/Coprime/Basic.lean b/Mathlib/RingTheory/Coprime/Basic.lean
index 2b88d64f35a22c..f1db8a4060789e 100644
--- a/Mathlib/RingTheory/Coprime/Basic.lean
+++ b/Mathlib/RingTheory/Coprime/Basic.lean
@@ -55,6 +55,9 @@ theorem IsCoprime.symm (H : IsCoprime x y) : IsCoprime y x :=
 theorem isCoprime_comm : IsCoprime x y ↔ IsCoprime y x :=
   ⟨IsCoprime.symm, IsCoprime.symm⟩
 
+instance : @Std.Symm R IsCoprime where
+  symm _ _ := .symm
+
 theorem isCoprime_self : IsCoprime x x ↔ IsUnit x :=
   ⟨fun ⟨a, b, h⟩ => .of_mul_eq_one (a + b) <| by rwa [mul_comm, add_mul], fun h =>
     let ⟨b, hb⟩ := isUnit_iff_exists_inv'.1 h