diff --git a/src/Init/Data/Int/Gcd.lean b/src/Init/Data/Int/Gcd.lean
index 913c857fef..49f3b2027d 100644
--- a/src/Init/Data/Int/Gcd.lean
+++ b/src/Init/Data/Int/Gcd.lean
@@ -113,6 +113,8 @@ theorem gcd_eq_right_iff_dvd (hb : 0 ≤ b) : gcd a b = b ↔ b ∣ a := by
 
 theorem gcd_assoc (a b c : Int) : gcd (gcd a b) c = gcd a (gcd b c) := Nat.gcd_assoc ..
 
+theorem gcd_left_comm (a b c : Int) : gcd a (gcd b c) = gcd b (gcd a c) := Nat.gcd_left_comm ..
+
 theorem gcd_mul_left (m n k : Int) : gcd (m * n) (m * k) = m.natAbs * gcd n k := by
   simp [gcd_eq_natAbs_gcd_natAbs, Nat.gcd_mul_left, natAbs_mul]
 
diff --git a/src/Init/Data/Nat/Gcd.lean b/src/Init/Data/Nat/Gcd.lean
index 7a1a573ea8..60ef917ea4 100644
--- a/src/Init/Data/Nat/Gcd.lean
+++ b/src/Init/Data/Nat/Gcd.lean
@@ -129,6 +129,9 @@ theorem gcd_assoc (m n k : Nat) : gcd (gcd m n) k = gcd m (gcd n k) :=
       (Nat.dvd_trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k)))
 instance : Std.Associative gcd := ⟨gcd_assoc⟩
 
+theorem gcd_left_comm (m n k : Nat) : gcd m (gcd n k) = gcd n (gcd m k) := by
+  rw [← gcd_assoc, ← gcd_assoc, gcd_comm m n]
+
 @[simp] theorem gcd_one_right (n : Nat) : gcd n 1 = 1 := (gcd_comm n 1).trans (gcd_one_left n)
 
 theorem gcd_mul_left (m n k : Nat) : gcd (m * n) (m * k) = m * gcd n k := by