diff --git a/Mathlib/Combinatorics/SimpleGraph/Sum.lean b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
index fd1f40e9d8ce5..bd199088a58d6 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Sum.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
@@ -39,8 +39,8 @@ protected def Sum (G : SimpleGraph α) (H : SimpleGraph β) : SimpleGraph (α 
     | Sum.inl _, Sum.inr _ | Sum.inr _, Sum.inl _ => id
   loopless u := by cases u <;> simp
 
-/-- Disjoint sum of `G` and `H`. -/
-infixl:60 " + " => SimpleGraph.Sum
+@[simps]
+instance : HAdd (SimpleGraph α) (SimpleGraph β) (SimpleGraph (α ⊕ β)) := ⟨SimpleGraph.Sum⟩
 
 variable {G : SimpleGraph α} {H : SimpleGraph β}