-- 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
⊢ LinearIndependent R v

Tactic:
let _ := Classical.decEq ι

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 ι
⊢ 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
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
⊢ a = 0

Tactic:
apply hp.dfinsupp_lsum_injective

Result:
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

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 = 0 ∨ v i = 0
⊢ (fun c => c • v i) (l i) = (fun c => c • v i) (0 i)

Tactic:
simpa

Result:
no goals

Proof state:
case h
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 : ι
⊢ l i = 0 i

Tactic:
apply smul_left_injective R (hv' i)

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 : ι
⊢ (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 ι
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

Tactic:
ext i

Result:
case h
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 : ι
⊢ l i = 0 i