-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem iSupIndep.linearIndependent [NoZeroSMulDivisors R N] {ι} (p : ι → Submodule R N)
    (hp : iSupIndep p) {v : ι → N} (hv : ∀ i, v i ∈ p i) (hv' : ∀ i, v i ≠ 0) :
    LinearIndependent R v

Proof state:
R : Type u_2
N : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : NoZeroSMulDivisors R N
ι : Type u_6
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : DecidableEq R := Classical.decEq R
⊢ LinearIndependent R v

Tactic:
rw [linearIndependent_iff]

Result:
R : Type u_2
N : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : NoZeroSMulDivisors R N
ι : Type u_6
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : DecidableEq R := Classical.decEq R
⊢ ∀ (l : ι →₀ R), (Finsupp.linearCombination R v) l = 0 → l = 0

Proof state:
R : Type u_2
N : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : NoZeroSMulDivisors R N
ι : Type u_6
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : DecidableEq R := Classical.decEq R
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
⊢ l = 0

Tactic:
let a :=
  DFinsupp.mapRange.linearMap (fun i => LinearMap.toSpanSingleton R (p i) ⟨v i, hv i⟩)
    l.toDFinsupp

Result:
R : Type u_2
N : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : NoZeroSMulDivisors R N
ι : Type u_6
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : DecidableEq R := Classical.decEq R
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp
⊢ l = 0

Proof state:
case h.a
R : Type u_2
N : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : NoZeroSMulDivisors R N
ι : Type u_6
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : DecidableEq R := Classical.decEq R
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp
ha : a = 0
i : ι
⊢ (fun c => c • v i) (l i) = (fun c => c • v i) (0 i)

Tactic:
have : l i • v i = a i := rfl

Result:
case h.a
R : Type u_2
N : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : NoZeroSMulDivisors R N
ι : Type u_6
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : DecidableEq R := Classical.decEq R
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp
ha : a = 0
i : ι
this : l i • v i = ↑(a i)
⊢ (fun c => c • v i) (l i) = (fun c => c • v i) (0 i)

Proof state:
R : Type u_2
N : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : NoZeroSMulDivisors R N
ι : Type u_6
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
x✝ : DecidableEq ι := Classical.decEq ι
⊢ LinearIndependent R v

Tactic:
let _ := Classical.decEq R

Result:
R : Type u_2
N : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : NoZeroSMulDivisors R N
ι : Type u_6
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : DecidableEq R := Classical.decEq R
⊢ LinearIndependent R v

Proof state:
case h.a
R : Type u_2
N : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : NoZeroSMulDivisors R N
ι : Type u_6
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : DecidableEq R := Classical.decEq R
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp
ha : a = 0
i : ι
this : l i • v i = ↑(a i)
⊢ (fun c => c • v i) (l i) = (fun c => c • v i) (0 i)

Tactic:
simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this

Result:
case h.a
R : Type u_2
N : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : NoZeroSMulDivisors R N
ι : Type u_6
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : DecidableEq R := Classical.decEq R
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp
ha : a = 0
i : ι
this : l i = 0 ∨ v i = 0
⊢ (fun c => c • v i) (l i) = (fun c => c • v i) (0 i)

Proof state:
case a
R : Type u_2
N : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : NoZeroSMulDivisors R N
ι : Type u_6
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : DecidableEq R := Classical.decEq R
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp
⊢ ((lsum ℕ) fun i => (p i).subtype) a = ((lsum ℕ) fun i => (p i).subtype) 0

Tactic:
rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl

Result:
no goals

Proof state:
R : Type u_2
N : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : NoZeroSMulDivisors R N
ι : Type u_6
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : DecidableEq R := Classical.decEq R
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp
⊢ l = 0

Tactic:
have ha : a = 0 := by
  apply hp.dfinsupp_lsum_injective
  rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl

Result:
R : Type u_2
N : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : NoZeroSMulDivisors R N
ι : Type u_6
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : DecidableEq R := Classical.decEq R
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp
ha : a = 0
⊢ l = 0

Proof state:
R : Type u_2
N : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : NoZeroSMulDivisors R N
ι : Type u_6
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : DecidableEq R := Classical.decEq R
⊢ ∀ (l : ι →₀ R), (Finsupp.linearCombination R v) l = 0 → l = 0

Tactic:
intro l hl

Result:
R : Type u_2
N : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : NoZeroSMulDivisors R N
ι : Type u_6
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
x✝¹ : DecidableEq ι := Classical.decEq ι
x✝ : DecidableEq R := Classical.decEq R
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
⊢ l = 0