From 3ff330e4a3db063cb55990c27c563f420d6d6573 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 31 Oct 2024 13:30:17 +0000
Subject: [PATCH] chore: add a helper lemma for `linearCombination`

---
 Mathlib/LinearAlgebra/Finsupp.lean           | 15 +++++++++------
 Mathlib/LinearAlgebra/LinearIndependent.lean |  8 ++------
 2 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean
index d8827696368ab..b925e5828c76f 100644
--- a/Mathlib/LinearAlgebra/Finsupp.lean
+++ b/Mathlib/LinearAlgebra/Finsupp.lean
@@ -636,9 +636,14 @@ theorem linearCombination_zero : linearCombination R (0 : α → M) = 0 :=
 
 variable {α M}
 
+theorem linearCombination_comp_linear (f : M →ₗ[R] M') :
+    linearCombination R (f ∘ v) = f ∘ₗ linearCombination R v := by
+  ext
+  simp [linearCombination_apply]
+
 theorem apply_linearCombination (f : M →ₗ[R] M') (v) (l : α →₀ R) :
-    f (linearCombination R v l) = linearCombination R (f ∘ v) l := by
-  apply Finsupp.induction_linear l <;> simp (config := { contextual := true })
+    f (linearCombination R v l) = linearCombination R (f ∘ v) l :=
+  congr($(linearCombination_comp_linear R f) l).symm
 
 @[deprecated (since := "2024-08-29")] alias apply_total := apply_linearCombination
 
@@ -1225,10 +1230,8 @@ protected theorem Submodule.finsupp_sum_mem {ι β : Type*} [Zero β] (S : Submo
   AddSubmonoidClass.finsupp_sum_mem S f g h
 
 theorem LinearMap.map_finsupp_linearCombination (f : M →ₗ[R] N) {ι : Type*} {g : ι → M}
-    (l : ι →₀ R) : f (linearCombination R g l) = linearCombination R (f ∘ g) l := by
-  -- Porting note: `(· ∘ ·)` is required.
-  simp only [linearCombination_apply, linearCombination_apply, Finsupp.sum, map_sum, map_smul,
-             (· ∘ ·)]
+    (l : ι →₀ R) : f (linearCombination R g l) = linearCombination R (f ∘ g) l :=
+  apply_linearCombination _ _ _ _
 
 @[deprecated (since := "2024-08-29")] alias LinearMap.map_finsupp_total :=
   LinearMap.map_finsupp_linearCombination
diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean
index 1c1b164bab895..325ee21927ba3 100644
--- a/Mathlib/LinearAlgebra/LinearIndependent.lean
+++ b/Mathlib/LinearAlgebra/LinearIndependent.lean
@@ -282,18 +282,14 @@ theorem LinearIndependent.map (hv : LinearIndependent R v) {f : M →ₗ[R] M'}
       at hf_inj
   rw [linearIndependent_iff_ker] at hv ⊢
   rw [hv, le_bot_iff] at hf_inj
-  haveI : Inhabited M := ⟨0⟩
-  rw [Finsupp.linearCombination_comp, Finsupp.lmapDomain_linearCombination _ _ f,
-      LinearMap.ker_comp, hf_inj]
-  exact fun _ => rfl
+  rw [Finsupp.linearCombination_comp_linear, LinearMap.ker_comp, hf_inj]
 
 /-- If `v` is an injective family of vectors such that `f ∘ v` is linearly independent, then `v`
     spans a submodule disjoint from the kernel of `f` -/
 theorem Submodule.range_ker_disjoint {f : M →ₗ[R] M'}
     (hv : LinearIndependent R (f ∘ v)) :
     Disjoint (span R (range v)) (LinearMap.ker f) := by
-  rw [linearIndependent_iff_ker, Finsupp.linearCombination_comp,
-      Finsupp.lmapDomain_linearCombination R _ f (fun _ ↦ rfl), LinearMap.ker_comp] at hv
+  rw [linearIndependent_iff_ker, Finsupp.linearCombination_comp_linear, LinearMap.ker_comp] at hv
   rw [disjoint_iff_inf_le, ← Set.image_univ, Finsupp.span_image_eq_map_linearCombination,
     map_inf_eq_map_inf_comap, hv, inf_bot_eq, map_bot]