internlm/Lean-Github huggingface dataset:
Theorem: linearIndependent_restrict_iff
Proof 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
Proof 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
Theorem: linearIndependent_restrict_iff
Proof 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 ⊢
Proof 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
Theorem: linearIndependent_restrict_iff
Proof 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)⟩
Proof state after:
no goals
Theorem: linearIndependent_restrict_iff
Proof 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
Proof state after:
no goals
Theorem: linearIndependent_restrict_iff
Proof 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
Proof state after:
no goals
Theorem: linearIndependent_restrict_iff
Proof 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)⟩
Proof state after:
no goals
Theorem: linearIndependent_restrict_iff
Proof 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
Proof state after:
no goals
Theorem: linearIndependent_subsingleton_index
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
Tactic:
obtain (he | he) := isEmpty_or_nonempty ι
Proof state after:
case inl
α : 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : IsEmpty ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0

case inr
α : 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
Theorem: linearIndependent_subsingleton_index
Proof state before:
case inr
α : 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
Tactic:
obtain ⟨_⟩ := (unique_iff_subsingleton_and_nonempty (α := ι)).2 ⟨by assumption, he⟩
Proof state after:
case inr.intro
α : 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
val✝ : Unique ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
Theorem: linearIndependent_subsingleton_index
Proof state before:
case inr.intro
α : 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
val✝ : Unique ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
Tactic:
rw [linearIndependent_unique_iff]
Proof state after:
case inr.intro
α : 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
val✝ : Unique ι
⊢ f default ≠ 0 ↔ ∀ (i : ι), f i ≠ 0
Theorem: linearIndependent_subsingleton_index
Proof state before:
case inr.intro
α : 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
val✝ : Unique ι
⊢ f default ≠ 0 ↔ ∀ (i : ι), f i ≠ 0
Tactic:
exact ⟨fun h i ↦ by rwa [Unique.eq_default i], fun h ↦ h _⟩
Proof state after:
no goals
Theorem: linearIndependent_subsingleton_index
Proof state before:
case inl
α : 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : IsEmpty ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
Tactic:
simp [linearIndependent_empty_type]
Proof state after:
no goals
Theorem: linearIndependent_subsingleton_index
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
⊢ Subsingleton ι
Tactic:
assumption
Proof state after:
no goals
Theorem: linearIndependent_subsingleton_index
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
val✝ : Unique ι
h : f default ≠ 0
i : ι
⊢ f i ≠ 0
Tactic:
rwa [Unique.eq_default i]
Proof state after:
no goals
Theorem: linearIndependent_of_finite_index
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
⊢ LinearIndependent R f
Tactic:
have hinj : f.Injective := by
  intro x y hxy
  have hli := (h {x,y} (toFinite _))
  have h : (⟨x, by simp⟩ : ({x,y} : Set ι)) = ⟨y, by simp⟩ := by
    rw [← hli.injective.eq_iff]; simpa
  simpa using h
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
hinj : Injective f
⊢ LinearIndependent R f
Theorem: linearIndependent_of_finite_index
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
hinj : Injective f
⊢ LinearIndependent R f
Tactic:
rw [← linearIndependent_subtype_range hinj]
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
hinj : Injective f
⊢ LinearIndependent (ι := { x // x ∈ range f }) R Subtype.val
Theorem: linearIndependent_of_finite_index
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
hinj : Injective f
⊢ LinearIndependent (ι := { x // x ∈ range f }) R Subtype.val
Tactic:
refine linearIndependent_of_finite _ fun t ht htfin ↦ ?_
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
hinj : Injective f
t : Set M
ht : t ⊆ range f
htfin : t.Finite
⊢ LinearIndependent R fun (x : ↑t) => ↑x
Theorem: linearIndependent_of_finite_index
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
hinj : Injective f
t : Set M
ht : t ⊆ range f
htfin : t.Finite
⊢ LinearIndependent R fun (x : ↑t) => ↑x
Tactic:
obtain ⟨t, rfl⟩ := subset_range_iff_exists_image_eq.1 ht
Proof state after:
case intro
α : 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
hinj : Injective f
t : Set ι
ht : f '' t ⊆ range f
htfin : (f '' t).Finite
⊢ LinearIndependent R fun (x : ↑(f '' t)) => ↑x
Theorem: linearIndependent_of_finite_index
Proof state before:
case intro
α : 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
hinj : Injective f
t : Set ι
ht : f '' t ⊆ range f
htfin : (f '' t).Finite
⊢ LinearIndependent R fun (x : ↑(f '' t)) => ↑x
Tactic:
exact (linearIndependent_image (injOn_of_injective hinj)).1 <|
  h t (htfin.of_finite_image (injOn_of_injective hinj))
Proof state after:
no goals
Theorem: linearIndependent_of_finite_index
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
⊢ Injective f
Tactic:
intro x y hxy
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
x y : ι
hxy : f x = f y
⊢ x = y
Theorem: linearIndependent_of_finite_index
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
x y : ι
hxy : f x = f y
⊢ x = y
Tactic:
have hli := (h {x,y} (toFinite _))
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
x y : ι
hxy : f x = f y
hli : LinearIndependent (ι := ↑{x, y}) R ({x, y}.restrict f)
⊢ x = y
Theorem: linearIndependent_of_finite_index
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
x y : ι
hxy : f x = f y
hli : LinearIndependent (ι := ↑{x, y}) R ({x, y}.restrict f)
⊢ x = y
Tactic:
have h : (⟨x, by simp⟩ : ({x,y} : Set ι)) = ⟨y, by simp⟩ := by
  rw [← hli.injective.eq_iff]; simpa
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h✝ : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
x y : ι
hxy : f x = f y
hli : LinearIndependent (ι := ↑{x, y}) R ({x, y}.restrict f)
h : ⟨x, ⋯⟩ = ⟨y, ⋯⟩
⊢ x = y
Theorem: linearIndependent_of_finite_index
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h✝ : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
x y : ι
hxy : f x = f y
hli : LinearIndependent (ι := ↑{x, y}) R ({x, y}.restrict f)
h : ⟨x, ⋯⟩ = ⟨y, ⋯⟩
⊢ x = y
Tactic:
simpa using h
Proof state after:
no goals
Theorem: linearIndependent_of_finite_index
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
x y : ι
hxy : f x = f y
hli : LinearIndependent (ι := ↑{x, y}) R ({x, y}.restrict f)
⊢ x ∈ {x, y}
Tactic:
simp
Proof state after:
no goals
Theorem: linearIndependent_of_finite_index
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
x y : ι
hxy : f x = f y
hli : LinearIndependent (ι := ↑{x, y}) R ({x, y}.restrict f)
⊢ y ∈ {x, y}
Tactic:
simp
Proof state after:
no goals
Theorem: linearIndependent_of_finite_index
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
x y : ι
hxy : f x = f y
hli : LinearIndependent (ι := ↑{x, y}) R ({x, y}.restrict f)
⊢ ⟨x, ⋯⟩ = ⟨y, ⋯⟩
Tactic:
rw [← hli.injective.eq_iff]
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
x y : ι
hxy : f x = f y
hli : LinearIndependent (ι := ↑{x, y}) R ({x, y}.restrict f)
⊢ {x, y}.restrict f ⟨x, ⋯⟩ = {x, y}.restrict f ⟨y, ⋯⟩
Theorem: linearIndependent_of_finite_index
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
h : ∀ (t : Set ι), t.Finite → LinearIndependent (ι := ↑t) R (t.restrict f)
x y : ι
hxy : f x = f y
hli : LinearIndependent (ι := ↑{x, y}) R ({x, y}.restrict f)
⊢ {x, y}.restrict f ⟨x, ⋯⟩ = {x, y}.restrict f ⟨y, ⋯⟩
Tactic:
simpa
Proof state after:
no goals
Theorem: linearIndependent_iUnion_of_directed'
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
⊢ LinearIndependent (ι := ↑(⋃ j, s j)) R ((⋃ j, s j).restrict f)
Tactic:
obtain (h_empt | hne) := isEmpty_or_nonempty η
Proof state after:
case inl
α : 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'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
h_empt : IsEmpty η
⊢ LinearIndependent (ι := ↑(⋃ j, s j)) R ((⋃ j, s j).restrict f)

case inr
α : 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'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
⊢ LinearIndependent (ι := ↑(⋃ j, s j)) R ((⋃ j, s j).restrict f)
Theorem: linearIndependent_iUnion_of_directed'
Proof state before:
case inr
α : 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'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
⊢ LinearIndependent (ι := ↑(⋃ j, s j)) R ((⋃ j, s j).restrict f)
Tactic:
apply linearIndependent_of_finite_index _ (fun t ht ↦ ?_)
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
⊢ LinearIndependent (ι := ↑t) R (t.restrict ((⋃ j, s j).restrict f))
Theorem: linearIndependent_iUnion_of_directed'
Proof 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'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
⊢ LinearIndependent (ι := ↑t) R (t.restrict ((⋃ j, s j).restrict f))
Tactic:
obtain ⟨I,hIfin, hI⟩ :=
  finite_subset_iUnion (ht.image Subtype.val) (Subtype.coe_image_subset (⋃ j, s j) t)
Proof state after:
case intro.intro
α : 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'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
⊢ LinearIndependent (ι := ↑t) R (t.restrict ((⋃ j, s j).restrict f))