no goals
ι : Type u'
ι' : Type ?u.1252914
R : Type ?u.1252917
K : Type u_1
M : Type ?u.1252923
M' : Type ?u.1252926
M'' : Type ?u.1252929
V : Type u
V' : Type ?u.1252934
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
f : Fin 2 → V
⊢ LinearIndependent K f ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
rw [linearIndependent_fin_succ, linearIndependent_unique_iff, range_unique, mem_span_singleton,
  not_exists, show Fin.tail f default = f 1 by rw [← Fin.succ_zero_eq_one]; rfl]
ι : Type u'
ι' : Type ?u.1252914
R : Type ?u.1252917
K : Type u_1
M : Type ?u.1252923
M' : Type ?u.1252926
M'' : Type ?u.1252929
V : Type u
V' : Type ?u.1252934
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
f : Fin 2 → V
⊢ Fin.tail f default = f (Fin.succ 0)
ι : Type u'
ι' : Type ?u.1252914
R : Type ?u.1252917
K : Type u_1
M : Type ?u.1252923
M' : Type ?u.1252926
M'' : Type ?u.1252929
V : Type u
V' : Type ?u.1252934
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
f : Fin 2 → V
⊢ Fin.tail f default = f 1
rw [← Fin.succ_zero_eq_one]
no goals
ι : Type u'
ι' : Type ?u.1252914
R : Type ?u.1252917
K : Type u_1
M : Type ?u.1252923
M' : Type ?u.1252926
M'' : Type ?u.1252929
V : Type u
V' : Type ?u.1252934
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
f : Fin 2 → V
⊢ Fin.tail f default = f (Fin.succ 0)
rfl