-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
rw rw₁ rw₂ rw₃ :
  ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)), l = 0
rw₄ :
  ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)), l = 0
rw₅ :
  ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)),
    let a : Π₀ (i : ι), ↥(p i) :=
      (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
            LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
          (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
        l.toDFinsupp;
    ∀ (ha : a = 0), l = 0
h :
  ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)),
    let a : Π₀ (i : ι), ↥(p i) :=
      (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
            LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
          (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
        l.toDFinsupp;
    ∀ (ha : a = 0) (i : ι), Eq.{u_3 + 1} (α := R) ((l : (a : ι) → R) i : R) ((0 : (a : ι) → R) i : R)
h₁ :
  ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)),
    let a : Π₀ (i : ι), ↥(p i) :=
      (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
            LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
          (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
        l.toDFinsupp;
    ∀ (ha : a = 0) (i : ι),
      Eq.{u_6 + 1} (α := N) ((fun (x : R) ↦ x • v i) ((l : (a : ι) → R) i))
        ((fun (x : R) ↦ x • v i) ((0 : (a : ι) → R) i))
⊢ LinearIndependent R v
have h₂ : ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)),
  let a : Π₀ (i : ι), ↥(p i) :=
    (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
          LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) sorry) :
        (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
      l.toDFinsupp;
  ∀ (ha : a = 0) (i : ι)
    (this : HSMul.hSMul.{u_3, u_6, u_6} (α := R) ((l : (a : ι) → R) i : R) (v i) = (↑((a : (a : ι) → ↥(p a)) i) : N)),
    Eq.{u_6 + 1} (α := N) ((fun (x : R) ↦ x • v i) ((l : (a : ι) → R) i))
      ((fun (x : R) ↦ x • v i) ((0 : (a : ι) → R) i))
Tactic: classical
  rw [linearIndependent_iff]
  intro l hl
  let a :=
    DFinsupp.mapRange.linearMap (fun i => LinearMap.toSpanSingleton R (p i) ⟨v i, hv i⟩)
      l.toDFinsupp
  have ha : a = 0 := by
    apply hp.dfinsupp_lsum_injective
    rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl
  ext i
  apply smul_left_injective R (hv' i)
  have : l i • v i = a i := rfl
  simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this
  simpa