forall vs input

Stream: new members

[Dax Fohl]

I'm trying to prove

theorem test (n: Nat):
  ∀ (m : Fin n),
  Vector.get (Vector.replicate n 0) m = 0 := by
  rw [Vector.get_replicate] -- did not find instance of the pattern in the target expression

but it doesn't find the instance. However the following works fine, even though AFAICT it is the same thing.

theorem test1 (n: Nat) (m : Fin n):
  Vector.get (Vector.replicate n 0) m = 0 := by
  rw [Vector.get_replicate]

Why does it behave differently? How do I get the first one to compile?

[Martin Dvořák]

You must start the proof with intro m in the first one.