ι : Type u'
ι' : Type ?u.142157
R : Type u_2
K : Type ?u.142163
M : Type u_1
M' : Type ?u.142169
M'' : Type ?u.142172
V : Type u
V' : Type ?u.142177
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
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set M
li : LinearIndependent R Subtype.val
⊢ (#↑s) ≤ ↑n
ι : Type u'
ι' : Type ?u.142157
R : Type u_2
K : Type ?u.142163
M : Type u_1
M' : Type ?u.142169
M'' : Type ?u.142172
V : Type u
V' : Type ?u.142177
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
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
⊢ ∀ (s : Set M), LinearIndependent R Subtype.val → (#↑s) ≤ ↑n
intro s li
case H
ι : Type u'
ι' : Type ?u.142157
R : Type u_2
K : Type ?u.142163
M : Type u_1
M' : Type ?u.142169
M'' : Type ?u.142172
V : Type u
V' : Type ?u.142177
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
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set M
li : LinearIndependent R Subtype.val
⊢ ∀ (s_1 : Finset ↑s), Finset.card s_1 ≤ n
ι : Type u'
ι' : Type ?u.142157
R : Type u_2
K : Type ?u.142163
M : Type u_1
M' : Type ?u.142169
M'' : Type ?u.142172
V : Type u
V' : Type ?u.142177
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
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set M
li : LinearIndependent R Subtype.val
⊢ (#↑s) ≤ ↑n
apply Cardinal.card_le_of
case H
ι : Type u'
ι' : Type ?u.142157
R : Type u_2
K : Type ?u.142163
M : Type u_1
M' : Type ?u.142169
M'' : Type ?u.142172
V : Type u
V' : Type ?u.142177
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
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ Finset.card t ≤ n
case H
ι : Type u'
ι' : Type ?u.142157
R : Type u_2
K : Type ?u.142163
M : Type u_1
M' : Type ?u.142169
M'' : Type ?u.142172
V : Type u
V' : Type ?u.142177
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
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set M
li : LinearIndependent R Subtype.val
⊢ ∀ (s_1 : Finset ↑s), Finset.card s_1 ≤ n
intro t
case H
ι : Type u'
ι' : Type ?u.142157
R : Type u_2
K : Type ?u.142163
M : Type u_1
M' : Type ?u.142169
M'' : Type ?u.142172
V : Type u
V' : Type ?u.142177
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
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ Finset.card (Finset.map (Embedding.subtype s) t) ≤ n
case H
ι : Type u'
ι' : Type ?u.142157
R : Type u_2
K : Type ?u.142163
M : Type u_1
M' : Type ?u.142169
M'' : Type ?u.142172
V : Type u
V' : Type ?u.142177
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
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ Finset.card t ≤ n
rw [← Finset.card_map (Embedding.subtype s)]
case H.a
ι : Type u'
ι' : Type ?u.142157
R : Type u_2
K : Type ?u.142163
M : Type u_1
M' : Type ?u.142169
M'' : Type ?u.142172
V : Type u
V' : Type ?u.142177
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
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ LinearIndependent R fun i => ↑i
case H
ι : Type u'
ι' : Type ?u.142157
R : Type u_2
K : Type ?u.142163
M : Type u_1
M' : Type ?u.142169
M'' : Type ?u.142172
V : Type u
V' : Type ?u.142177
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
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ Finset.card (Finset.map (Embedding.subtype s) t) ≤ n
apply H
no goals
case H.a
ι : Type u'
ι' : Type ?u.142157
R : Type u_2
K : Type ?u.142163
M : Type u_1
M' : Type ?u.142169
M'' : Type ?u.142172
V : Type u
V' : Type ?u.142177
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
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → Finset.card s ≤ n
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ LinearIndependent R fun i => ↑i
apply linearIndependent_finset_map_embedding_subtype _ li