case mp
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
⊢ (∀ (l : ↑s →₀ R), (Finsupp.sum l fun i a => a • v ↑i) = 0 → l = 0) →
    ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0

case mpr
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
⊢ (∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0) →
    ∀ (l : ↑s →₀ R), (Finsupp.sum l fun i a => a • v ↑i) = 0 → l = 0
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
⊢ (∀ (l : ↑s →₀ R), (Finsupp.sum l fun i a => a • v ↑i) = 0 → l = 0) ↔
    ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
constructor
case mp
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ↑s →₀ R), (Finsupp.sum l fun i a => a • v ↑i) = 0 → l = 0
l : ι →₀ R
hl₁ : ∀ (x : ι), x ∈ l.support → x ∈ s
hl₂ : (Finsupp.sum l fun i a => a • v i) = 0
⊢ l = 0
case mp
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
⊢ (∀ (l : ↑s →₀ R), (Finsupp.sum l fun i a => a • v ↑i) = 0 → l = 0) →
    ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
intro h l hl₁ hl₂
case mp
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ↑s →₀ R), (Finsupp.sum l fun i a => a • v ↑i) = 0 → l = 0
l : ι →₀ R
hl₁ : ∀ (x : ι), x ∈ l.support → x ∈ s
hl₂ : (Finsupp.sum l fun i a => a • v i) = 0
this : Finsupp.subtypeDomain s l = 0
⊢ l = 0
case mp
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ↑s →₀ R), (Finsupp.sum l fun i a => a • v ↑i) = 0 → l = 0
l : ι →₀ R
hl₁ : ∀ (x : ι), x ∈ l.support → x ∈ s
hl₂ : (Finsupp.sum l fun i a => a • v i) = 0
⊢ l = 0
have := h (l.subtypeDomain s) ((Finsupp.sum_subtypeDomain_index hl₁).trans hl₂)
no goals
case mp
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ↑s →₀ R), (Finsupp.sum l fun i a => a • v ↑i) = 0 → l = 0
l : ι →₀ R
hl₁ : ∀ (x : ι), x ∈ l.support → x ∈ s
hl₂ : (Finsupp.sum l fun i a => a • v i) = 0
this : Finsupp.subtypeDomain s l = 0
⊢ l = 0
exact (Finsupp.subtypeDomain_eq_zero_iff hl₁).1 this
case mpr
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
l : ↑s →₀ R
hl : (Finsupp.sum l fun i a => a • v ↑i) = 0
⊢ l = 0
case mpr
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
⊢ (∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0) →
    ∀ (l : ↑s →₀ R), (Finsupp.sum l fun i a => a • v ↑i) = 0 → l = 0
intro h l hl
case mpr.refine'_1
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
l : ↑s →₀ R
hl : (Finsupp.sum l fun i a => a • v ↑i) = 0
⊢ ∀ (x : ι), x ∈ (Finsupp.embDomain (Embedding.subtype s) l).support → x ∈ s

case mpr.refine'_2
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
l : ↑s →₀ R
hl : (Finsupp.sum l fun i a => a • v ↑i) = 0
⊢ (Finsupp.sum (Finsupp.embDomain (Embedding.subtype s) l) fun i a => a • v i) = 0
case mpr
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
l : ↑s →₀ R
hl : (Finsupp.sum l fun i a => a • v ↑i) = 0
⊢ l = 0
refine' Finsupp.embDomain_eq_zero.1 (h (l.embDomain <| Function.Embedding.subtype s) _ _)
case mpr.refine'_1
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
l : ↑s →₀ R
hl : (Finsupp.sum l fun i a => a • v ↑i) = 0
⊢ ∀ (i : ι) (hi : i ∈ s), ¬↑l { val := i, property := hi } = 0 → i ∈ s
case mpr.refine'_1
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
l : ↑s →₀ R
hl : (Finsupp.sum l fun i a => a • v ↑i) = 0
⊢ ∀ (x : ι), x ∈ (Finsupp.embDomain (Embedding.subtype s) l).support → x ∈ s
suffices ∀ i hi, ¬l ⟨i, hi⟩ = 0 → i ∈ s by simpa
case mpr.refine'_1
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
l : ↑s →₀ R
hl : (Finsupp.sum l fun i a => a • v ↑i) = 0
i✝ : ι
hi✝ : i✝ ∈ s
a✝ : ¬↑l { val := i✝, property := hi✝ } = 0
⊢ i✝ ∈ s
case mpr.refine'_1
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
l : ↑s →₀ R
hl : (Finsupp.sum l fun i a => a • v ↑i) = 0
⊢ ∀ (i : ι) (hi : i ∈ s), ¬↑l { val := i, property := hi } = 0 → i ∈ s
intros
no goals
case mpr.refine'_1
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
l : ↑s →₀ R
hl : (Finsupp.sum l fun i a => a • v ↑i) = 0
i✝ : ι
hi✝ : i✝ ∈ s
a✝ : ¬↑l { val := i✝, property := hi✝ } = 0
⊢ i✝ ∈ s
assumption
no goals
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
l : ↑s →₀ R
hl : (Finsupp.sum l fun i a => a • v ↑i) = 0
this : ∀ (i : ι) (hi : i ∈ s), ¬↑l { val := i, property := hi } = 0 → i ∈ s
⊢ ∀ (x : ι), x ∈ (Finsupp.embDomain (Embedding.subtype s) l).support → x ∈ s
simpa
case mpr.refine'_2.h_zero
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
l : ↑s →₀ R
hl : (Finsupp.sum l fun i a => a • v ↑i) = 0
⊢ ∀ (b : ι), 0 • v b = 0

case mpr.refine'_2.h_add
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
l : ↑s →₀ R
hl : (Finsupp.sum l fun i a => a • v ↑i) = 0
⊢ ∀ (b : ι) (m₁ m₂ : R), (m₁ + m₂) • v b = m₁ • v b + m₂ • v b
case mpr.refine'_2
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
l : ↑s →₀ R
hl : (Finsupp.sum l fun i a => a • v ↑i) = 0
⊢ (Finsupp.sum (Finsupp.embDomain (Embedding.subtype s) l) fun i a => a • v i) = 0
rwa [Finsupp.embDomain_eq_mapDomain, Finsupp.sum_mapDomain_index]
no goals
case mpr.refine'_2.h_zero
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
l : ↑s →₀ R
hl : (Finsupp.sum l fun i a => a • v ↑i) = 0
⊢ ∀ (b : ι), 0 • v b = 0

case mpr.refine'_2.h_add
ι : Type u'
ι' : Type ?u.143047
R : Type u_1
K : Type ?u.143053
M : Type u_2
M' : Type ?u.143059
M'' : Type ?u.143062
V : Type u
V' : Type ?u.143067
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set ι
h : ∀ (l : ι →₀ R), (∀ (x : ι), x ∈ l.support → x ∈ s) → (Finsupp.sum l fun i a => a • v i) = 0 → l = 0
l : ↑s →₀ R
hl : (Finsupp.sum l fun i a => a • v ↑i) = 0
⊢ ∀ (b : ι) (m₁ m₂ : R), (m₁ + m₂) • v b = m₁ • v b + m₂ • v b
exacts [fun _ => zero_smul _ _, fun _ _ _ => add_smul _ _ _]