Variable in goal gets renamed

Stream: new members

[Wojtek Wawrów]

Trying to solve the following tutorial exercise:

lemma near_cluster :
  cluster_point u a → ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
begin

I begin my solution with the following:

  intros h_clust ε ε_pos N,
  unfold cluster_point at h_clust,
  cases h_clust with φ hφ,
  cases hφ with hφ₁ hφ₂,
  specialize hφ₂ ε ε_pos,
  cases hφ₂ with N hN,
  use φ N,

but after doing this, the goal gets rewritten to φ N ≥ N_1 ∧ .... Why did the N get rewritten to N_1? I am meaning for it to be the exact same value as the N I introduced above. Not quite sure how to proceed with this one.

[Alex J. Best]

You have two things in your context called N, one from the first line introducing N and one from the second to last doing cases cases hφ₂ with N hN you get another, I'd suggest calling the second one M or something instead so that things don't get confusde

[Wojtek Wawrów]

Oh derp, didn't even realize. Thanks a lot