ι : Type u'
ι' : Type ?u.1312198
R : Type ?u.1312201
K : Type u_1
M : Type ?u.1312207
M' : Type ?u.1312210
M'' : Type ?u.1312213
V : Type u
V' : Type ?u.1312218
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
ht : Set.Finite t
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K t)
⊢ s ⊆ ↑(span K t)
ι : Type u'
ι' : Type ?u.1312198
R : Type ?u.1312201
K : Type u_1
M : Type ?u.1312207
M' : Type ?u.1312210
M'' : Type ?u.1312213
V : Type u
V' : Type ?u.1312218
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
ht : Set.Finite t
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K t)
⊢ s ⊆ ↑(span K ↑(Finite.toFinset ht))
simp
no goals
ι : Type u'
ι' : Type ?u.1312198
R : Type ?u.1312201
K : Type u_1
M : Type ?u.1312207
M' : Type ?u.1312210
M'' : Type ?u.1312213
V : Type u
V' : Type ?u.1312218
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
ht : Set.Finite t
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K t)
⊢ s ⊆ ↑(span K t)
assumption
ι : Type u'
ι' : Type ?u.1312198
R : Type ?u.1312201
K : Type u_1
M : Type ?u.1312207
M' : Type ?u.1312210
M'' : Type ?u.1312213
V : Type u
V' : Type ?u.1312218
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
ht : Set.Finite t
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑(Finite.toFinset ht))
u : Finset V
_hust : ↑u ⊆ s ∪ ↑(Finite.toFinset ht)
hsu : s ⊆ ↑u
Eq : Finset.card u = Finset.card (Finite.toFinset ht)
this : Set.Finite s
⊢ Finset.card (Finite.toFinset this) ≤ Finset.card u
ι : Type u'
ι' : Type ?u.1312198
R : Type ?u.1312201
K : Type u_1
M : Type ?u.1312207
M' : Type ?u.1312210
M'' : Type ?u.1312213
V : Type u
V' : Type ?u.1312218
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
ht : Set.Finite t
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑(Finite.toFinset ht))
u : Finset V
_hust : ↑u ⊆ s ∪ ↑(Finite.toFinset ht)
hsu : s ⊆ ↑u
Eq : Finset.card u = Finset.card (Finite.toFinset ht)
this : Set.Finite s
⊢ Finset.card (Finite.toFinset this) ≤ Finset.card (Finite.toFinset ht)
rw [← Eq]
no goals
ι : Type u'
ι' : Type ?u.1312198
R : Type ?u.1312201
K : Type u_1
M : Type ?u.1312207
M' : Type ?u.1312210
M'' : Type ?u.1312213
V : Type u
V' : Type ?u.1312218
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
ht : Set.Finite t
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑(Finite.toFinset ht))
u : Finset V
_hust : ↑u ⊆ s ∪ ↑(Finite.toFinset ht)
hsu : s ⊆ ↑u
Eq : Finset.card u = Finset.card (Finite.toFinset ht)
this : Set.Finite s
⊢ Finset.card (Finite.toFinset this) ≤ Finset.card u
exact Finset.card_le_of_subset <| Finset.coe_subset.mp <| by simp [hsu]
no goals
ι : Type u'
ι' : Type ?u.1312198
R : Type ?u.1312201
K : Type u_1
M : Type ?u.1312207
M' : Type ?u.1312210
M'' : Type ?u.1312213
V : Type u
V' : Type ?u.1312218
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
ht : Set.Finite t
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑(Finite.toFinset ht))
u : Finset V
_hust : ↑u ⊆ s ∪ ↑(Finite.toFinset ht)
hsu : s ⊆ ↑u
Eq : Finset.card u = Finset.card (Finite.toFinset ht)
this : Set.Finite s
⊢ ↑(Finite.toFinset this) ⊆ ↑u
simp [hsu]