From 30b1c57d49c1b9cb8ed656413bb6f9a89fe67b27 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Iv=C3=A1n=20Renison?=
 <85908989+IvanRenison@users.noreply.github.com>
Date: Wed, 18 Sep 2024 09:28:15 -0300
Subject: [PATCH] Use `Sum.inl` and `Sum.inr`

---
 Mathlib/Combinatorics/SimpleGraph/Sum.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Sum.lean b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
index bd199088a58d6..bace95cb896ad 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Sum.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
@@ -39,7 +39,7 @@ protected def Sum (G : SimpleGraph α) (H : SimpleGraph β) : SimpleGraph (α 
     | Sum.inl _, Sum.inr _ | Sum.inr _, Sum.inl _ => id
   loopless u := by cases u <;> simp
 
-@[simps]
+@[simps!]
 instance : HAdd (SimpleGraph α) (SimpleGraph β) (SimpleGraph (α ⊕ β)) := ⟨SimpleGraph.Sum⟩
 
 variable {G : SimpleGraph α} {H : SimpleGraph β}
@@ -62,15 +62,15 @@ def SumAssoc {I : SimpleGraph γ} : (G + H) + I ≃g G + (H + I) := ⟨Equiv.sum
 
 /-- The embedding of `G` into `G + H`. -/
 @[simps]
-def SumLeft : G ↪g G + H where
-  toFun u := Sum.inl u
+protected def Sum.inl : G ↪g G + H where
+  toFun u := _root_.Sum.inl u
   inj' u v := by simp
   map_rel_iff' := by simp
 
 /-- The embedding of `H` into `G + H`. -/
 @[simps]
-def SumRight : H ↪g G + H where
-  toFun u := Sum.inr u
+protected def Sum.inr : H ↪g G + H where
+  toFun u := _root_.Sum.inr u
   inj' u v := by simp
   map_rel_iff' := by simp