Theorem: linearIndependent_of_finite_index (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'
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
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

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]
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

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 ↦ ?_
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

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

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))
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'
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
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

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 _))
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

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

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
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'
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
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'
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
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'
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]
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, ⋯⟩

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
State after:
no goals