From 18306db3969b451db2bee37629bdfb43fa95fca1 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Sat, 2 Mar 2024 00:01:39 +1100
Subject: [PATCH] chore: protect Int.add_right_inj et al (#3551)

Reducing some name conflicts in Mathlib.
---
 src/Init/Data/Int/Lemmas.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Init/Data/Int/Lemmas.lean b/src/Init/Data/Int/Lemmas.lean
index 462591e5b9..82ce1f69f2 100644
--- a/src/Init/Data/Int/Lemmas.lean
+++ b/src/Init/Data/Int/Lemmas.lean
@@ -324,22 +324,22 @@ theorem toNat_sub (m n : Nat) : toNat (m - n) = m - n := by
 /- ## add/sub injectivity -/
 
 @[simp]
-theorem add_right_inj (i j k : Int) : (i + k = j + k) ↔ i = j := by
+protected theorem add_right_inj (i j k : Int) : (i + k = j + k) ↔ i = j := by
   apply Iff.intro
   · intro p
     rw [←Int.add_sub_cancel i k, ←Int.add_sub_cancel j k, p]
   · exact congrArg (· + k)
 
 @[simp]
-theorem add_left_inj (i j k : Int) : (k + i = k + j) ↔ i = j := by
+protected theorem add_left_inj (i j k : Int) : (k + i = k + j) ↔ i = j := by
   simp [Int.add_comm k]
 
 @[simp]
-theorem sub_left_inj (i j k : Int) : (k - i = k - j) ↔ i = j := by
+protected theorem sub_left_inj (i j k : Int) : (k - i = k - j) ↔ i = j := by
   simp [Int.sub_eq_add_neg, Int.neg_inj]
 
 @[simp]
-theorem sub_right_inj (i j k : Int) : (i - k = j - k) ↔ i = j := by
+protected theorem sub_right_inj (i j k : Int) : (i - k = j - k) ↔ i = j := by
   simp [Int.sub_eq_add_neg]
 
 /- ## Ring properties -/