ι : Type u_3
R : Type u_1
S : Type ?u.488476
M : ι → Type ?u.488481
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
⊢ ∀ (i : ι) (x : { x // x ∈ p i }) (v : Π₀ (i : ι), { x // x ∈ p i }),
    ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (erase i v) = ↑x → x = 0
ι : Type u_3
R : Type u_1
S : Type ?u.488476
M : ι → Type ?u.488481
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
⊢ Independent p
rw [independent_iff_forall_dfinsupp]
ι : Type u_3
R : Type u_1
S : Type ?u.488476
M : ι → Type ?u.488481
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
i : ι
x : { x // x ∈ p i }
v : Π₀ (i : ι), { x // x ∈ p i }
hv : ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (erase i v) = ↑x
⊢ x = 0
ι : Type u_3
R : Type u_1
S : Type ?u.488476
M : ι → Type ?u.488481
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
⊢ ∀ (i : ι) (x : { x // x ∈ p i }) (v : Π₀ (i : ι), { x // x ∈ p i }),
    ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (erase i v) = ↑x → x = 0
intro i x v hv
case hv
ι : Type u_3
R : Type u_1
S : Type ?u.488476
M : ι → Type ?u.488481
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
i : ι
x : { x // x ∈ p i }
v : Π₀ (i : ι), { x // x ∈ p i }
hv : ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (erase i v) = ↑x
⊢ ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (erase i v) = ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (single i x)

ι : Type u_3
R : Type u_1
S : Type ?u.488476
M : ι → Type ?u.488481
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
i : ι
x : { x // x ∈ p i }
v : Π₀ (i : ι), { x // x ∈ p i }
hv :
  ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (erase i v) = ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (single i x)
⊢ x = 0
ι : Type u_3
R : Type u_1
S : Type ?u.488476
M : ι → Type ?u.488481
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
i : ι
x : { x // x ∈ p i }
v : Π₀ (i : ι), { x // x ∈ p i }
hv : ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (erase i v) = ↑x
⊢ x = 0
replace hv :
  lsum ℕ (M := fun i ↦ ↥(p i)) (fun i => (p i).subtype) (erase i v) =
    lsum ℕ (M := fun i ↦ ↥(p i)) (fun i => (p i).subtype) (single i x)
ι : Type u_3
R : Type u_1
S : Type ?u.488476
M : ι → Type ?u.488481
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
i : ι
x : { x // x ∈ p i }
v : Π₀ (i : ι), { x // x ∈ p i }
hv :
  ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (erase i v) = ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (single i x)
this : ↑(erase i v) i = ↑(single i x) i
⊢ x = 0
ι : Type u_3
R : Type u_1
S : Type ?u.488476
M : ι → Type ?u.488481
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
i : ι
x : { x // x ∈ p i }
v : Π₀ (i : ι), { x // x ∈ p i }
hv :
  ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (erase i v) = ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (single i x)
⊢ x = 0
have := FunLike.ext_iff.mp (h hv) i
no goals
ι : Type u_3
R : Type u_1
S : Type ?u.488476
M : ι → Type ?u.488481
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
i : ι
x : { x // x ∈ p i }
v : Π₀ (i : ι), { x // x ∈ p i }
hv :
  ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (erase i v) = ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (single i x)
this : ↑(erase i v) i = ↑(single i x) i
⊢ x = 0
simpa [eq_comm] using this
no goals
case hv
ι : Type u_3
R : Type u_1
S : Type ?u.488476
M : ι → Type ?u.488481
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
i : ι
x : { x // x ∈ p i }
v : Π₀ (i : ι), { x // x ∈ p i }
hv : ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (erase i v) = ↑x
⊢ ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (erase i v) = ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (single i x)
simpa only [lsum_single] using hv