Theorem: linearIndependent_restrict_iff (Matroid/ForMathlib/LinearAlgebra/LinearIndependent.lean)

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
⊢ LinearIndependent (ι := ↑s) R (s.restrict f) ↔ ∀ (l : ι →₀ R), (Finsupp.total ι M R f) l = 0 → ↑l.support ⊆ s → l = 0
Tactic:
rw [linearIndependent_iff]
State after:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
⊢ (∀ (l : ↑s →₀ R), (Finsupp.total (↑s) M R (s.restrict f)) l = 0 → l = 0) ↔
    ∀ (l : ι →₀ R), (Finsupp.total ι M R f) l = 0 → ↑l.support ⊆ s → l = 0

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
⊢ (∀ (l : ↑s →₀ R), (Finsupp.total (↑s) M R (s.restrict f)) l = 0 → l = 0) ↔
    ∀ (l : ι →₀ R), (Finsupp.total ι M R f) l = 0 → ↑l.support ⊆ s → l = 0
Tactic:
refine ⟨fun h l hl0 hls ↦ ?_, fun h l hl0 ↦ ?_⟩
State after:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
h : ∀ (l : ↑s →₀ R), (Finsupp.total (↑s) M R (s.restrict f)) l = 0 → l = 0
l : ι →₀ R
hl0 : (Finsupp.total ι M R f) l = 0
hls : ↑l.support ⊆ s
⊢ l = 0

case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
h : ∀ (l : ι →₀ R), (Finsupp.total ι M R f) l = 0 → ↑l.support ⊆ s → l = 0
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
⊢ l = 0

State before:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
h : ∀ (l : ι →₀ R), (Finsupp.total ι M R f) l = 0 → ↑l.support ⊆ s → l = 0
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
⊢ l = 0
Tactic:
specialize h l.extendDomain
State after:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
h : (Finsupp.total ι M R f) l.extendDomain = 0 → ↑l.extendDomain.support ⊆ s → l.extendDomain = 0
⊢ l = 0

State before:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
h : (Finsupp.total ι M R f) l.extendDomain = 0 → ↑l.extendDomain.support ⊆ s → l.extendDomain = 0
⊢ l = 0
Tactic:
rw [Finsupp.extendDomain_eq_embDomain_subtype, Finsupp.total_embDomain] at h
State after:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
h :
  (Finsupp.total { x // x ∈ s } M R (f ∘ ⇑(Embedding.subtype fun x => x ∈ s))) l = 0 →
    ↑(Finsupp.embDomain (Embedding.subtype fun x => x ∈ s) l).support ⊆ s →
      Finsupp.embDomain (Embedding.subtype fun x => x ∈ s) l = 0
⊢ l = 0

State before:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
h :
  (Finsupp.total { x // x ∈ s } M R (f ∘ ⇑(Embedding.subtype fun x => x ∈ s))) l = 0 →
    ↑(Finsupp.embDomain (Embedding.subtype fun x => x ∈ s) l).support ⊆ s →
      Finsupp.embDomain (Embedding.subtype fun x => x ∈ s) l = 0
⊢ l = 0
Tactic:
simp only [Embedding.coe_subtype, Finsupp.support_embDomain, Finset.coe_map, image_subset_iff,
  Subtype.coe_preimage_self, subset_univ, Finsupp.embDomain_eq_zero, forall_true_left] at h
State after:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
h : (Finsupp.total { x // x ∈ s } M R (f ∘ Subtype.val)) l = 0 → l = 0
⊢ l = 0

State before:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ↑s →₀ R
hl0 : (Finsupp.total (↑s) M R (s.restrict f)) l = 0
h : (Finsupp.total { x // x ∈ s } M R (f ∘ Subtype.val)) l = 0 → l = 0
⊢ l = 0
Tactic:
exact h hl0
State after:
no goals

State before:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
h : ∀ (l : ↑s →₀ R), (Finsupp.total (↑s) M R (s.restrict f)) l = 0 → l = 0
l : ι →₀ R
hl0 : (Finsupp.total ι M R f) l = 0
hls : ↑l.support ⊆ s
⊢ l = 0
Tactic:
rw [Finsupp.total_apply, Finsupp.sum_of_support_subset _ Subset.rfl _ (by simp)] at hl0
State after:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
h : ∀ (l : ↑s →₀ R), (Finsupp.total (↑s) M R (s.restrict f)) l = 0 → l = 0
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
⊢ l = 0

State before:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
h : ∀ (l : ↑s →₀ R), (Finsupp.total (↑s) M R (s.restrict f)) l = 0 → l = 0
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
⊢ l = 0
Tactic:
specialize h (Finsupp.comapDomain ((↑) : s → ι) l Subtype.val_injective.injOn)
State after:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h :
  (Finsupp.total (↑s) M R (s.restrict f)) (Finsupp.comapDomain Subtype.val l ⋯) = 0 →
    Finsupp.comapDomain Subtype.val l ⋯ = 0
⊢ l = 0

State before:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h :
  (Finsupp.total (↑s) M R (s.restrict f)) (Finsupp.comapDomain Subtype.val l ⋯) = 0 →
    Finsupp.comapDomain Subtype.val l ⋯ = 0
⊢ l = 0
Tactic:
simp only [Finsupp.total_comapDomain, restrict_apply] at h
State after:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h : ∑ x ∈ l.support.preimage Subtype.val ⋯, l ↑x • f ↑x = 0 → Finsupp.comapDomain Subtype.val l ⋯ = 0
⊢ l = 0

State before:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h : ∑ x ∈ l.support.preimage Subtype.val ⋯, l ↑x • f ↑x = 0 → Finsupp.comapDomain Subtype.val l ⋯ = 0
⊢ l = 0
Tactic:
rw [Finset.sum_preimage _ _ _ (fun x ↦ l x • f x)
  (fun x hx hx' ↦ (hx' (by simpa using hls hx)).elim )] at h
State after:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h : ∑ x ∈ l.support, l x • f x = 0 → Finsupp.comapDomain Subtype.val l ⋯ = 0
⊢ l = 0

State before:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h : ∑ x ∈ l.support, l x • f x = 0 → Finsupp.comapDomain Subtype.val l ⋯ = 0
⊢ l = 0
Tactic:
simp_rw [DFunLike.ext_iff] at h ⊢
State after:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h : ∑ x ∈ l.support, l x • f x = 0 → ∀ (x : ↑s), (Finsupp.comapDomain Subtype.val l ⋯) x = 0 x
⊢ ∀ (x : ι), l x = 0 x

State before:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h : ∑ x ∈ l.support, l x • f x = 0 → ∀ (x : ↑s), (Finsupp.comapDomain Subtype.val l ⋯) x = 0 x
⊢ ∀ (x : ι), l x = 0 x
Tactic:
exact fun i ↦ by_contra fun hi ↦ hi <|
  by simpa using (h hl0) ⟨i, hls (show i ∈ l.support by simpa using hi)⟩
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
h : ∀ (l : ↑s →₀ R), (Finsupp.total (↑s) M R (s.restrict f)) l = 0 → l = 0
l : ι →₀ R
hl0 : (l.sum fun i a => a • f i) = 0
hls : ↑l.support ⊆ s
⊢ ∀ i ∈ l.support, 0 • f i = 0
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h : ∑ x ∈ l.support.preimage Subtype.val ⋯, l ↑x • f ↑x = 0 → Finsupp.comapDomain Subtype.val l ⋯ = 0
x : ι
hx : x ∈ l.support
hx' : x ∉ range Subtype.val
⊢ x ∈ range Subtype.val
Tactic:
simpa using hls hx
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h : ∑ x ∈ l.support, l x • f x = 0 → ∀ (x : ↑s), (Finsupp.comapDomain Subtype.val l ⋯) x = 0 x
i : ι
hi : ¬l i = 0 i
⊢ l i = 0 i
Tactic:
simpa using (h hl0) ⟨i, hls (show i ∈ l.support by simpa using hi)⟩
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set ι
f : ι → M
l : ι →₀ R
hl0 : ∑ x ∈ l.support, l x • f x = 0
hls : ↑l.support ⊆ s
h : ∑ x ∈ l.support, l x • f x = 0 → ∀ (x : ↑s), (Finsupp.comapDomain Subtype.val l ⋯) x = 0 x
i : ι
hi : ¬l i = 0 i
⊢ i ∈ l.support
Tactic:
simpa using hi
State after:
no goals