Refactor sumMap and related lemmas for clarity

Author: robertmaxton42

Mathlib/Topology/ContinuousMap/Basic.lean

@@ -205,8 +205,8 @@ def prodSwap : C(α × β, β × α) := .prodMk .snd .fst
 end Prod
 
 section Sum
-variable {X Y Z : Type*}
-  [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
+variable {X Y Z W : Type*}
+  [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W]
 
 /-- `Sum.inl : X → X ⊕ Y` as a bundled continuous map. -/
 def inl : C(X, X ⊕ Y) where
@@ -242,21 +242,17 @@ lemma sumElim_comp_inr (f : C(X, Z)) (g : C(Y, Z)) : (sumElim f g) ∘ Sum.inr =
 /-- A continuous map between sums can be defined fiberwise by its action on the summands.
 This is `Continuous.sumMap` bundled into a continuous map. -/
 @[simps]
-def sumMap {X Y Z W : Type*}
-    [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W]
-    (f : C(X, Z)) (g : C(Y, W)) : C(X ⊕ Y, Z ⊕ W) where
+def sumMap (f : C(X, Z)) (g : C(Y, W)) : C(X ⊕ Y, Z ⊕ W) where
   toFun := Sum.map f g
 
 @[simp]
-lemma sumMap_comp_inl {X Y Z W : Type*}
-    [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W]
-    (f : C(X, Z)) (g : C(Y, W)) : (sumMap f g) ∘ Sum.inl = Sum.inl ∘ f := by
+lemma sumMap_comp_inl (f : C(X, Z)) (g : C(Y, W)) :
+    (sumMap f g) ∘ Sum.inl = Sum.inl ∘ f := by
   ext x; simp
 
 @[simp]
-lemma sumMap_comp_inr {X Y Z W : Type*}
-    [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W]
-    (f : C(X, Z)) (g : C(Y, W)) : (sumMap f g) ∘ Sum.inr = Sum.inr ∘ g := by
+lemma sumMap_comp_inr (f : C(X, Z)) (g : C(Y, W)) :
+    (sumMap f g) ∘ Sum.inr = Sum.inr ∘ g := by
   ext x; simp
 
 end Sum