ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
⊢ Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : Independent p
⊢ Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
rw [independent_iff_forall_dfinsupp] at h
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
⊢ LinearMap.ker (↑(lsum ℕ) fun i => Submodule.subtype (p i)) = ⊥
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
⊢ Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
suffices LinearMap.ker (lsum ℕ (M := fun i ↦ ↥(p i)) fun i => (p i).subtype) = ⊥ by
  letI thisI : AddCommGroup (Π₀ i, p i) := inferInstance
  rw [LinearMap.ker_eq_bot] at this
  exact this
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
⊢ ∀ (m : Π₀ (i : ι), { x // x ∈ p i }), ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) m = 0 → m = 0
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
⊢ LinearMap.ker (↑(lsum ℕ) fun i => Submodule.subtype (p i)) = ⊥
rw [LinearMap.ker_eq_bot']
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
m : Π₀ (i : ι), { x // x ∈ p i }
hm : ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) m = 0
⊢ m = 0
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
⊢ ∀ (m : Π₀ (i : ι), { x // x ∈ p i }), ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) m = 0 → m = 0
intro m hm
case h
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
m : Π₀ (i : ι), { x // x ∈ p i }
hm : ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) m = 0
i : ι
⊢ ↑m i = ↑0 i
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
m : Π₀ (i : ι), { x // x ∈ p i }
hm : ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) m = 0
⊢ m = 0
ext i : 1
case h
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
m : Π₀ (i : ι), { x // x ∈ p i }
hm : ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) m = 0
i : ι
⊢ -↑m i = 0
case h
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
m : Π₀ (i : ι), { x // x ∈ p i }
hm : ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) m = 0
i : ι
⊢ ↑m i = ↑0 i
rw [Dfinsupp.zero_apply, ← neg_eq_zero]
case h
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
m : Π₀ (i : ι), { x // x ∈ p i }
hm : ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) m = 0
i : ι
⊢ ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (erase i m) = ↑(-↑m i)
case h
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
m : Π₀ (i : ι), { x // x ∈ p i }
hm : ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) m = 0
i : ι
⊢ -↑m i = 0
refine' h i (-m i) m _
no goals
case h
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
m : Π₀ (i : ι), { x // x ∈ p i }
hm : ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) m = 0
i : ι
⊢ ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i)) (erase i m) = ↑(-↑m i)
rwa [← erase_add_single i m, LinearMap.map_add, lsum_single, Submodule.subtype_apply,
  add_eq_zero_iff_eq_neg, ← Submodule.coe_neg] at hm
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
this : LinearMap.ker (↑(lsum ℕ) fun i => Submodule.subtype (p i)) = ⊥
thisI : AddCommGroup (Π₀ (i : ι), { x // x ∈ p i }) := inferInstance
⊢ Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
this : LinearMap.ker (↑(lsum ℕ) fun i => Submodule.subtype (p i)) = ⊥
⊢ Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
letI thisI : AddCommGroup (Π₀ i, p i) := inferInstance
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
thisI : AddCommGroup (Π₀ (i : ι), { x // x ∈ p i }) := inferInstance
this : Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
⊢ Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
this : LinearMap.ker (↑(lsum ℕ) fun i => Submodule.subtype (p i)) = ⊥
thisI : AddCommGroup (Π₀ (i : ι), { x // x ∈ p i }) := inferInstance
⊢ Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
rw [LinearMap.ker_eq_bot] at this
no goals
ι : Type u_3
R : Type u_1
S : Type ?u.648167
M : ι → Type ?u.648172
N : Type u_2
dec_ι : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h✝ : Independent p
h :
  ∀ (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
thisI : AddCommGroup (Π₀ (i : ι), { x // x ∈ p i }) := inferInstance
this : Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
⊢ Function.Injective ↑(↑(lsum ℕ) fun i => Submodule.subtype (p i))
exact this