-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
have :
  Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
    (linearCombination R fun (ix : (i : ι) × φ i) ↦
      single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
        (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
    ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
        linearCombination R (f i)) ∘ₗ
      (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))
have₁ :
  ∀
    (this :
      Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
        (linearCombination R fun (ix : (i : ι) × φ i) ↦
          single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
            (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
        ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
            linearCombination R (f i)) ∘ₗ
          (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))),
    LinearIndependent R (M := Π₀ (i : ι), M i) fun (ix : (i : ι) × φ i) ↦
      single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
        (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))
have₂ :
  Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
    (linearCombination R fun (ix : (i : ι) × φ i) ↦
      single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
        (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
    ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
        linearCombination R (f i)) ∘ₗ
      (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))
have₃ have₄ :
  ∀
    (this :
      Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
        (linearCombination R fun (ix : (i : ι) × φ i) ↦
          single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
            (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
        ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
            linearCombination R (f i)) ∘ₗ
          (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))),
    LinearIndependent R (M := Π₀ (i : ι), M i) fun (ix : (i : ι) × φ i) ↦
      single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
        (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))
have₅ :
  ∀
    (this :
      Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
        (linearCombination R fun (ix : (i : ι) × φ i) ↦
          single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
            (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
        ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
            linearCombination R (f i)) ∘ₗ
          (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))),
    Function.Injective (α := (i : ι) × φ i →₀ R) (β := Π₀ (i : ι), M i)
      (⇑((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
              linearCombination R (f i)) ∘ₗ
            (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R)) :
        (a : (i : ι) × φ i →₀ R) → Π₀ (i : ι), M i)
⊢ LinearIndependent R (M := Π₀ (i : ι), M i) fun (ix : (i : ι) × φ i) ↦
    single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
      (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))

Tactic:
classical
  have : linearCombination R (fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)) =
    DFinsupp.mapRange.linearMap (fun i ↦ linearCombination R (f i)) ∘ₗ
    (sigmaFinsuppLequivDFinsupp R).toLinearMap := by ext; simp
  rw [LinearIndependent, this]
  exact ((DFinsupp.mapRange_injective _ fun _ ↦ map_zero _).mpr hf).comp (Equiv.injective _)

Premises used: Iff.mpr, map_zero, DFinsupp.mapRange_injective, Function.Injective.comp, LinearIndependent, Equiv.injective