case h.e'_4
ι : Type ?u.1148087
ι' : Type ?u.1148090
R : Type ?u.1148093
R₂ : Type ?u.1148096
K : Type u_1
M : Type ?u.1148102
M' : Type ?u.1148105
M'' : Type ?u.1148108
V : Type u
V' : Type ?u.1148113
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
⊢ Subtype.val = ↑(ofVectorSpace K V)
ι : Type ?u.1148087
ι' : Type ?u.1148090
R : Type ?u.1148093
R₂ : Type ?u.1148096
K : Type u_1
M : Type ?u.1148102
M' : Type ?u.1148105
M'' : Type ?u.1148108
V : Type u
V' : Type ?u.1148113
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
⊢ LinearIndependent K Subtype.val
convert (ofVectorSpace K V).linearIndependent
case h.e'_4.h
ι : Type ?u.1148087
ι' : Type ?u.1148090
R : Type ?u.1148093
R₂ : Type ?u.1148096
K : Type u_1
M : Type ?u.1148102
M' : Type ?u.1148105
M'' : Type ?u.1148108
V : Type u
V' : Type ?u.1148113
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
x : { x // x ∈ ofVectorSpaceIndex K V }
⊢ ↑x = ↑(ofVectorSpace K V) x
case h.e'_4
ι : Type ?u.1148087
ι' : Type ?u.1148090
R : Type ?u.1148093
R₂ : Type ?u.1148096
K : Type u_1
M : Type ?u.1148102
M' : Type ?u.1148105
M'' : Type ?u.1148108
V : Type u
V' : Type ?u.1148113
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
⊢ Subtype.val = ↑(ofVectorSpace K V)
ext x
no goals
case h.e'_4.h
ι : Type ?u.1148087
ι' : Type ?u.1148090
R : Type ?u.1148093
R₂ : Type ?u.1148096
K : Type u_1
M : Type ?u.1148102
M' : Type ?u.1148105
M'' : Type ?u.1148108
V : Type u
V' : Type ?u.1148113
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
x : { x // x ∈ ofVectorSpaceIndex K V }
⊢ ↑x = ↑(ofVectorSpace K V) x
rw [ofVectorSpace_apply_self]