-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem iSupIndep.dfinsupp_lsum_injective {p : ι → Submodule R N} (h : iSupIndep p) :
    Function.Injective (lsum ℕ (M := fun i ↦ ↥(p i)) fun i => (p i).subtype)

Proof state:
case h
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
m : Π₀ (i : ι), ↥(p i)
hm : ((lsum ℕ) fun i => (p i).subtype) m = 0
i : ι
⊢ m i = 0 i

Tactic:
rw [DFinsupp.zero_apply, ← neg_eq_zero]

Result:
case h
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
m : Π₀ (i : ι), ↥(p i)
hm : ((lsum ℕ) fun i => (p i).subtype) m = 0
i : ι
⊢ -m i = 0

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
⊢ Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)

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

Result:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
⊢ LinearMap.ker ((lsum ℕ) fun i => (p i).subtype) = ⊥

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : iSupIndep p
⊢ Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)

Tactic:
rw [iSupIndep_iff_forall_dfinsupp] at h

Result:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
⊢ Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)

Proof state:
case h
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
m : Π₀ (i : ι), ↥(p i)
hm : ((lsum ℕ) fun i => (p i).subtype) m = 0
i : ι
⊢ -m i = 0

Tactic:
refine h i (-m i) m ?_

Result:
case h
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
m : Π₀ (i : ι), ↥(p i)
hm : ((lsum ℕ) fun i => (p i).subtype) m = 0
i : ι
⊢ ((lsum ℕ) fun i => (p i).subtype) (erase i m) = ↑(-m i)

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
thisI : AddCommGroup (Π₀ (i : ι), ↥(p i)) := inferInstance
this : Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)
⊢ Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)

Tactic:
exact this

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
this : LinearMap.ker ((lsum ℕ) fun i => (p i).subtype) = ⊥
thisI : AddCommGroup (Π₀ (i : ι), ↥(p i)) := inferInstance
⊢ Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)

Tactic:
rw [LinearMap.ker_eq_bot] at this

Result:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
thisI : AddCommGroup (Π₀ (i : ι), ↥(p i)) := inferInstance
this : Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)
⊢ Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
m : Π₀ (i : ι), ↥(p i)
hm : ((lsum ℕ) fun i => (p i).subtype) m = 0
⊢ m = 0

Tactic:
ext i : 1

Result:
case h
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
m : Π₀ (i : ι), ↥(p i)
hm : ((lsum ℕ) fun i => (p i).subtype) m = 0
i : ι
⊢ m i = 0 i

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
⊢ LinearMap.ker ((lsum ℕ) fun i => (p i).subtype) = ⊥

Tactic:
rw [LinearMap.ker_eq_bot']

Result:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
⊢ ∀ (m : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) m = 0 → m = 0

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
⊢ ∀ (m : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) m = 0 → m = 0

Tactic:
intro m hm

Result:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
m : Π₀ (i : ι), ↥(p i)
hm : ((lsum ℕ) fun i => (p i).subtype) m = 0
⊢ m = 0

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
this : LinearMap.ker ((lsum ℕ) fun i => (p i).subtype) = ⊥
⊢ Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)

Tactic:
letI thisI : AddCommGroup (Π₀ i, p i) := inferInstance

Result:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i => (p i).subtype) (erase i v) = ↑x → x = 0
this : LinearMap.ker ((lsum ℕ) fun i => (p i).subtype) = ⊥
thisI : AddCommGroup (Π₀ (i : ι), ↥(p i)) := inferInstance
⊢ Function.Injective ⇑((lsum ℕ) fun i => (p i).subtype)