From def59e38d3eba6f27ac4e87da6c62df12df808e6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Iv=C3=A1n=20Renison?=
 <85908989+IvanRenison@users.noreply.github.com>
Date: Wed, 1 Apr 2026 10:17:38 -0300
Subject: [PATCH 1/6] Add homomorphism, embedding and isomorphism of sums

---
 Mathlib/Combinatorics/SimpleGraph/Sum.lean | 23 ++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Sum.lean b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
index f8a034bdb330fd..a60f35353eda0d 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Sum.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
@@ -28,8 +28,8 @@ both in `G` and adjacent in `G`, or they are both in `H` and adjacent in `H`.
 @[expose] public section
 
 namespace SimpleGraph
-variable {V W U γ : Type*} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph U}
-  {v v' : V} {w w' : W}
+variable {V W U V' W' γ : Type*} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph U}
+  {G' : SimpleGraph V'} {H' : SimpleGraph W'} {v v' : V} {w w' : W}
 
 /-- Disjoint sum of `G` and `H`. -/
 @[simps!]
@@ -71,6 +71,25 @@ def Embedding.sumInr : H ↪g G ⊕g H where
   inj' u v := by simp
   map_rel_iff' := by simp
 
+/-- Given homomorphisms `f : G →g G'` and `g : H →g H'`, returns a homomorphism from `G ⊕g H` to
+  `G' ⊕g H'` that applies `f` to the left component and `g` to the right component. -/
+def Hom.sum (f : G →g G') (g : H →g H') : G ⊕g H →g G' ⊕g H' where
+  toFun := Sum.map f g
+  map_rel' {u v} := by cases u <;> cases v <;> simp_all [f.map_rel, g.map_rel]
+
+/-- Given embeddings `f : G ↪g G'` and `g : H ↪g H'`, returns an embedding from `G ⊕g H` to
+  `G' ⊕g H'` that applies `f` to the left component and `g` to the right component. -/
+def Enbedding.sum (f : G ↪g G') (g : H ↪g H') : G ⊕g H ↪g G' ⊕g H' where
+  toFun := Sum.map f g
+  inj' u v := by cases u <;> cases v <;> simp
+  map_rel_iff' {u v} := by cases u <;> cases v <;> simp
+
+/-- Given isomorphisms `f : G ≃g G'` and `g : H ≃g H'`, returns an isomorphism from `G ⊕g H` to
+  `G' ⊕g H'` that applies `f` to the left component and `g` to the right component. -/
+def Iso.sum (f : G ≃g G') (g : H ≃g H') : G ⊕g H ≃g G' ⊕g H' where
+  toEquiv := Equiv.sumCongr f.toEquiv g.toEquiv
+  map_rel_iff' {u v} := by cases u <;> cases v <;> simp [f.map_rel_iff, g.map_rel_iff]
+
 lemma Reachable.sum_sup_edge (hv : G.Reachable v v') (hw : H.Reachable w w') :
     (G.sum H ⊔ edge (.inl v) (.inr w)).Reachable (.inl v') (.inr w') :=
   ((hv.symm.map Embedding.sumInl.toHom).mono le_sup_left).trans <| .trans

From beaff80a5e6035d2d66129caa555c233addc09e1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Iv=C3=A1n=20Renison?=
 <85908989+IvanRenison@users.noreply.github.com>
Date: Thu, 2 Apr 2026 15:15:43 -0300
Subject: [PATCH 2/6] Apply suggestions

---
 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 545e3f94f02a99..638a277a5fae3e 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Sum.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
@@ -72,21 +72,21 @@ def Embedding.sumInr : H ↪g G ⊕g H where
   map_rel_iff' := by simp
 
 /-- Given homomorphisms `f : G →g G'` and `g : H →g H'`, returns a homomorphism from `G ⊕g H` to
-  `G' ⊕g H'` that applies `f` to the left component and `g` to the right component. -/
+`G' ⊕g H'` that applies `f` to the left component and `g` to the right component. -/
 def Hom.sum (f : G →g G') (g : H →g H') : G ⊕g H →g G' ⊕g H' where
   toFun := Sum.map f g
   map_rel' {u v} := by cases u <;> cases v <;> simp_all [f.map_rel, g.map_rel]
 
 /-- Given embeddings `f : G ↪g G'` and `g : H ↪g H'`, returns an embedding from `G ⊕g H` to
-  `G' ⊕g H'` that applies `f` to the left component and `g` to the right component. -/
-def Enbedding.sum (f : G ↪g G') (g : H ↪g H') : G ⊕g H ↪g G' ⊕g H' where
+`G' ⊕g H'` that applies `f` to the left component and `g` to the right component. -/
+def Embedding.sum (f : G ↪g G') (g : H ↪g H') : G ⊕g H ↪g G' ⊕g H' where
   toFun := Sum.map f g
   inj' u v := by cases u <;> cases v <;> simp
   map_rel_iff' {u v} := by cases u <;> cases v <;> simp
 
 /-- Given isomorphisms `f : G ≃g G'` and `g : H ≃g H'`, returns an isomorphism from `G ⊕g H` to
-  `G' ⊕g H'` that applies `f` to the left component and `g` to the right component. -/
-def Iso.sum (f : G ≃g G') (g : H ≃g H') : G ⊕g H ≃g G' ⊕g H' where
+`G' ⊕g H'` that applies `f` to the left component and `g` to the right component. -/
+def Iso.sumCongr (f : G ≃g G') (g : H ≃g H') : G ⊕g H ≃g G' ⊕g H' where
   toEquiv := Equiv.sumCongr f.toEquiv g.toEquiv
   map_rel_iff' {u v} := by cases u <;> cases v <;> simp [f.map_rel_iff, g.map_rel_iff]
 

From 95631e4b23a111b6407fd0ac798168df822c0d7a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Iv=C3=A1n=20Renison?=
 <85908989+IvanRenison@users.noreply.github.com>
Date: Thu, 2 Apr 2026 19:42:46 -0300
Subject: [PATCH 3/6] Apply suggestions

---
 Mathlib/Combinatorics/SimpleGraph/Sum.lean | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Sum.lean b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
index 638a277a5fae3e..3b38b3ae4d3138 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Sum.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
@@ -28,7 +28,7 @@ both in `G` and adjacent in `G`, or they are both in `H` and adjacent in `H`.
 @[expose] public section
 
 namespace SimpleGraph
-variable {V W U V' W' γ : Type*} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph U}
+variable {U V V' W W' γ : Type*} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph U}
   {G' : SimpleGraph V'} {H' : SimpleGraph W'} {v v' : V} {w w' : W}
 
 /-- Disjoint sum of `G` and `H`. -/
@@ -73,23 +73,34 @@ def Embedding.sumInr : H ↪g G ⊕g H where
 
 /-- Given homomorphisms `f : G →g G'` and `g : H →g H'`, returns a homomorphism from `G ⊕g H` to
 `G' ⊕g H'` that applies `f` to the left component and `g` to the right component. -/
+@[simps]
 def Hom.sum (f : G →g G') (g : H →g H') : G ⊕g H →g G' ⊕g H' where
   toFun := Sum.map f g
   map_rel' {u v} := by cases u <;> cases v <;> simp_all [f.map_rel, g.map_rel]
 
 /-- Given embeddings `f : G ↪g G'` and `g : H ↪g H'`, returns an embedding from `G ⊕g H` to
 `G' ⊕g H'` that applies `f` to the left component and `g` to the right component. -/
+@[simps]
 def Embedding.sum (f : G ↪g G') (g : H ↪g H') : G ⊕g H ↪g G' ⊕g H' where
   toFun := Sum.map f g
   inj' u v := by cases u <;> cases v <;> simp
   map_rel_iff' {u v} := by cases u <;> cases v <;> simp
 
+lemma Embedding.toHom_sum (f : G ↪g G') (g : H ↪g H') :
+  (Embedding.sum f g).toHom = Hom.sum f.toHom g.toHom := rfl
+
 /-- Given isomorphisms `f : G ≃g G'` and `g : H ≃g H'`, returns an isomorphism from `G ⊕g H` to
 `G' ⊕g H'` that applies `f` to the left component and `g` to the right component. -/
 def Iso.sumCongr (f : G ≃g G') (g : H ≃g H') : G ⊕g H ≃g G' ⊕g H' where
-  toEquiv := Equiv.sumCongr f.toEquiv g.toEquiv
+  toEquiv := f.toEquiv.sumCongr g.toEquiv
   map_rel_iff' {u v} := by cases u <;> cases v <;> simp [f.map_rel_iff, g.map_rel_iff]
 
+lemma Iso.toHom_sumCongr (f : G ≃g G') (g : H ≃g H') :
+  (Iso.sumCongr f g).toHom = Hom.sum f.toHom g.toHom := rfl
+
+lemma Iso.toEmbedding_sumCongr (f : G ≃g G') (g : H ≃g H') :
+  (Iso.sumCongr f g).toEmbedding = Embedding.sum f.toEmbedding g.toEmbedding := rfl
+
 lemma Reachable.sum_sup_edge (hv : G.Reachable v v') (hw : H.Reachable w w') :
     (G.sum H ⊔ edge (.inl v) (.inr w)).Reachable (.inl v') (.inr w') :=
   ((hv.symm.map Embedding.sumInl.toHom).mono le_sup_left).trans <| .trans

From 51936b8c4d2bec9094b7f0118aa529a106482376 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Iv=C3=A1n=20Renison?=
 <85908989+IvanRenison@users.noreply.github.com>
Date: Fri, 3 Apr 2026 08:53:13 -0300
Subject: [PATCH 4/6] Add `@[simps!, simps toEquiv]`

---
 Mathlib/Combinatorics/SimpleGraph/Sum.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Sum.lean b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
index 3b38b3ae4d3138..1d0a922c73fb51 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Sum.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
@@ -91,6 +91,7 @@ lemma Embedding.toHom_sum (f : G ↪g G') (g : H ↪g H') :
 
 /-- Given isomorphisms `f : G ≃g G'` and `g : H ≃g H'`, returns an isomorphism from `G ⊕g H` to
 `G' ⊕g H'` that applies `f` to the left component and `g` to the right component. -/
+@[simps!, simps toEquiv]
 def Iso.sumCongr (f : G ≃g G') (g : H ≃g H') : G ⊕g H ≃g G' ⊕g H' where
   toEquiv := f.toEquiv.sumCongr g.toEquiv
   map_rel_iff' {u v} := by cases u <;> cases v <;> simp [f.map_rel_iff, g.map_rel_iff]

From 2d3334064afaff43ed7d07a7dd7e720b180a70c8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Iv=C3=A1n=20Renison?=
 <85908989+IvanRenison@users.noreply.github.com>
Date: Fri, 3 Apr 2026 10:37:19 -0300
Subject: [PATCH 5/6] Add `sum_comm_sumComm` and `sum_assoc_sumAssoc` lemmas

---
 Mathlib/Combinatorics/SimpleGraph/Sum.lean | 29 ++++++++++++++++++++--
 1 file changed, 27 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Sum.lean b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
index 1d0a922c73fb51..db8daf751be735 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Sum.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
@@ -28,8 +28,8 @@ both in `G` and adjacent in `G`, or they are both in `H` and adjacent in `H`.
 @[expose] public section
 
 namespace SimpleGraph
-variable {U V V' W W' γ : Type*} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph U}
-  {G' : SimpleGraph V'} {H' : SimpleGraph W'} {v v' : V} {w w' : W}
+variable {U U' V V' W W' γ : Type*} {G : SimpleGraph V} {H : SimpleGraph W} {I : SimpleGraph U}
+  {G' : SimpleGraph V'} {H' : SimpleGraph W'} {I' : SimpleGraph U'} {v v' : V} {w w' : W}
 
 /-- Disjoint sum of `G` and `H`. -/
 @[simps!]
@@ -78,6 +78,14 @@ def Hom.sum (f : G →g G') (g : H →g H') : G ⊕g H →g G' ⊕g H' where
   toFun := Sum.map f g
   map_rel' {u v} := by cases u <;> cases v <;> simp_all [f.map_rel, g.map_rel]
 
+lemma Hom.sum_comm_sumComm (f : G →g G') (g : H →g H') :
+    comp (sum f g) Iso.sumComm.toHom = comp Iso.sumComm.toHom (sum g f) := by
+  ext (v | w) <;> simp
+
+lemma Hom.sum_assoc_sumAssoc (f : G →g G') (g : H →g H') (h : I →g I') :
+    comp Iso.sumAssoc.toHom (sum (sum f g) h) = comp (sum f (sum g h)) Iso.sumAssoc.toHom := by
+  ext ((v | w) | u) <;> simp
+
 /-- Given embeddings `f : G ↪g G'` and `g : H ↪g H'`, returns an embedding from `G ⊕g H` to
 `G' ⊕g H'` that applies `f` to the left component and `g` to the right component. -/
 @[simps]
@@ -89,6 +97,15 @@ def Embedding.sum (f : G ↪g G') (g : H ↪g H') : G ⊕g H ↪g G' ⊕g H' whe
 lemma Embedding.toHom_sum (f : G ↪g G') (g : H ↪g H') :
   (Embedding.sum f g).toHom = Hom.sum f.toHom g.toHom := rfl
 
+lemma Embedding.sum_comm_sumComm (f : G ↪g G') (g : H ↪g H') :
+    comp Iso.sumComm.toEmbedding (sum f g) = comp (sum g f) Iso.sumComm.toEmbedding := by
+  ext (v | w) <;> simp
+
+lemma Embedding.sum_assoc_sumAssoc (f : G ↪g G') (g : H ↪g H') (h : I ↪g I') :
+    comp Iso.sumAssoc.toEmbedding (sum (sum f g) h) =
+      comp (sum f (sum g h)) Iso.sumAssoc.toEmbedding := by
+  ext ((v | w) | u) <;> simp
+
 /-- Given isomorphisms `f : G ≃g G'` and `g : H ≃g H'`, returns an isomorphism from `G ⊕g H` to
 `G' ⊕g H'` that applies `f` to the left component and `g` to the right component. -/
 @[simps!, simps toEquiv]
@@ -102,6 +119,14 @@ lemma Iso.toHom_sumCongr (f : G ≃g G') (g : H ≃g H') :
 lemma Iso.toEmbedding_sumCongr (f : G ≃g G') (g : H ≃g H') :
   (Iso.sumCongr f g).toEmbedding = Embedding.sum f.toEmbedding g.toEmbedding := rfl
 
+lemma Iso.sumCongr_comm_sumComm (f : G ≃g G') (g : H ≃g H') :
+    comp sumComm (sumCongr f g) = comp (sumCongr g f) sumComm := by
+  ext (v | w) <;> simp
+
+lemma Iso.sumCongr_assoc_sumAssoc (f : G ≃g G') (g : H ≃g H') (h : I ≃g I') :
+    comp sumAssoc (sumCongr (sumCongr f g) h) = comp (sumCongr f (sumCongr g h)) sumAssoc := by
+  ext ((v | w) | u) <;> simp
+
 lemma Reachable.sum_sup_edge (hv : G.Reachable v v') (hw : H.Reachable w w') :
     (G.sum H ⊔ edge (.inl v) (.inr w)).Reachable (.inl v') (.inr w') :=
   ((hv.symm.map Embedding.sumInl.toHom).mono le_sup_left).trans <| .trans

From 6b367e679ec3fb4045753af4e0c5084ad2a7f237 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Iv=C3=A1n=20Renison?=
 <85908989+IvanRenison@users.noreply.github.com>
Date: Fri, 3 Apr 2026 10:59:10 -0300
Subject: [PATCH 6/6] Rename with comp

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

diff --git a/Mathlib/Combinatorics/SimpleGraph/Sum.lean b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
index db8daf751be735..a323b247bbf938 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Sum.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Sum.lean
@@ -78,11 +78,11 @@ def Hom.sum (f : G →g G') (g : H →g H') : G ⊕g H →g G' ⊕g H' where
   toFun := Sum.map f g
   map_rel' {u v} := by cases u <;> cases v <;> simp_all [f.map_rel, g.map_rel]
 
-lemma Hom.sum_comm_sumComm (f : G →g G') (g : H →g H') :
+lemma Hom.sum_comp_sumComm (f : G →g G') (g : H →g H') :
     comp (sum f g) Iso.sumComm.toHom = comp Iso.sumComm.toHom (sum g f) := by
   ext (v | w) <;> simp
 
-lemma Hom.sum_assoc_sumAssoc (f : G →g G') (g : H →g H') (h : I →g I') :
+lemma Hom.sum_comp_sumAssoc (f : G →g G') (g : H →g H') (h : I →g I') :
     comp Iso.sumAssoc.toHom (sum (sum f g) h) = comp (sum f (sum g h)) Iso.sumAssoc.toHom := by
   ext ((v | w) | u) <;> simp
 
@@ -97,11 +97,11 @@ def Embedding.sum (f : G ↪g G') (g : H ↪g H') : G ⊕g H ↪g G' ⊕g H' whe
 lemma Embedding.toHom_sum (f : G ↪g G') (g : H ↪g H') :
   (Embedding.sum f g).toHom = Hom.sum f.toHom g.toHom := rfl
 
-lemma Embedding.sum_comm_sumComm (f : G ↪g G') (g : H ↪g H') :
+lemma Embedding.sum_comp_sumComm (f : G ↪g G') (g : H ↪g H') :
     comp Iso.sumComm.toEmbedding (sum f g) = comp (sum g f) Iso.sumComm.toEmbedding := by
   ext (v | w) <;> simp
 
-lemma Embedding.sum_assoc_sumAssoc (f : G ↪g G') (g : H ↪g H') (h : I ↪g I') :
+lemma Embedding.sum_comp_sumAssoc (f : G ↪g G') (g : H ↪g H') (h : I ↪g I') :
     comp Iso.sumAssoc.toEmbedding (sum (sum f g) h) =
       comp (sum f (sum g h)) Iso.sumAssoc.toEmbedding := by
   ext ((v | w) | u) <;> simp
@@ -119,11 +119,11 @@ lemma Iso.toHom_sumCongr (f : G ≃g G') (g : H ≃g H') :
 lemma Iso.toEmbedding_sumCongr (f : G ≃g G') (g : H ≃g H') :
   (Iso.sumCongr f g).toEmbedding = Embedding.sum f.toEmbedding g.toEmbedding := rfl
 
-lemma Iso.sumCongr_comm_sumComm (f : G ≃g G') (g : H ≃g H') :
+lemma Iso.sumCongr_comp_sumComm (f : G ≃g G') (g : H ≃g H') :
     comp sumComm (sumCongr f g) = comp (sumCongr g f) sumComm := by
   ext (v | w) <;> simp
 
-lemma Iso.sumCongr_assoc_sumAssoc (f : G ≃g G') (g : H ≃g H') (h : I ≃g I') :
+lemma Iso.sumCongr_comp_sumAssoc (f : G ≃g G') (g : H ≃g H') (h : I ≃g I') :
     comp sumAssoc (sumCongr (sumCongr f g) h) = comp (sumCongr f (sumCongr g h)) sumAssoc := by
   ext ((v | w) | u) <;> simp