rewrite only one occurrence

Stream: new members

[Vasily Ilin]

I have a goal with two occurrences of v, and would like to rewrite only one of them. Can I do that?

example (α : Type) (n : ℕ) (v : fin n → α) (w : α) : fin.tail (matrix.vec_cons w v) = v :=
begin
  rw ← @fin.tail_cons _ (λ_,α) w v,
end

I need it for this proof:

variables (k : Type) (V : Type) [field k] [add_comm_group V] [module k V]

example (n : ℕ) (v : fin n → V) (lin_indep : linear_independent k v) (w : V) : linear_independent k (matrix.vec_cons w v) ↔ w ∉ submodule.span k (set.range v)
:=
begin
  rw linear_independent_fin_succ,
  have : fin.tail (matrix.vec_cons w v) = v,
  sorry,
  sorry,
end

[Adam Topaz]

tactic#nth_rewrite

[Vasily Ilin]

Is it intentional that example (α : Type) (n : ℕ) (v : fin n → α) (w : α) : fin.tail (matrix.vec_cons w v) = v and similar variants do not exist in matrix but do exist in fin? It seems that translating between them is quite tedious (mostly because fin.cons w v does not work for (α : Type) (n : ℕ) (v : fin n → α) (w : α))

[Eric Wieser]

Do we have docs#matrix.vec_tail?

[Eric Wieser]

Yes; so you're not supposed to mix the two APIs it seems