fix

Author: YaelDillies

Mathlib/Data/Finsupp/Basic.lean

@@ -284,15 +284,12 @@ theorem mapDomain_notin_range {f : α → β} (x : α →₀ M) (a : β) (h : a
 @[simp] lemma mapDomain_id : mapDomain id v = v := sum_single _
 @[simp] lemma mapDomain_fun_id : mapDomain (fun x ↦ x) v = v := sum_single _
 
+lemma mapDomain_fun_comp (f : α → β) (g : β → γ) :
+    mapDomain (fun a ↦ g (f a)) v = mapDomain g (mapDomain f v) := by
+  simp [mapDomain, sum_sum_index]
+
 theorem mapDomain_comp {f : α → β} {g : β → γ} :
-    mapDomain (g ∘ f) v = mapDomain g (mapDomain f v) := by
-  refine ((sum_sum_index ?_ ?_).trans ?_).symm
-  · intro
-    exact single_zero _
-  · intro
-    exact single_add _
-  refine sum_congr fun _ _ => sum_single_index ?_
-  exact single_zero _
+    mapDomain (g ∘ f) v = mapDomain g (mapDomain f v) := mapDomain_fun_comp f g
 
 @[simp]
 theorem mapDomain_single {f : α → β} {a : α} {b : M} : mapDomain f (single a b) = single (f a) b :=

Mathlib/LinearAlgebra/Finsupp/Pi.lean

@@ -253,8 +253,7 @@ lemma map_id [Finite X] : map (_root_.id : X → X) (M := M) = _root_.id := by
 
 lemma map_comp [Finite X] [Finite Y] [Finite Z] (g : Y → Z) (f : X → Y) :
     map (g.comp f) (M := M) = (map g).comp (map f) := by
-  ext s
-  simp [map, Finsupp.mapDomain_comp]
+  ext s; simp [map, Finsupp.mapDomain_fun_comp]
 
 end