Reassign variable value

Stream: new members

[rory]

I'm proving a theorem which uses subgoal as have p : k ∣ int.gcd a b ↔ k ∣ int.gcd b (a - n*b) , but I didn't impose any constraint on k, k is just a variable of type ℤ, is there a way to reassign k value, or to reassign k value, I have to prove have p : ∀ k : ℤ, k ∣ int.gcd a b ↔ k ∣ int.gcd b (a - n*b)

[Johan Commelin]

Can you give a bit more context?

[Johan Commelin]

I'm not sure I understand what the problem is

[rory]

I'm not sure I understand what the problem is

So this is the theorem I'm proving,

theorem prop4 (a b : ℤ) (h : a ≠ 0 ∧ b ≠ 0) (k : ℤ):
∀ n : ℤ, int.gcd a b = int.gcd b (a - n*b) :=
....stuff...
  have p₅ : k ∣ int.gcd a b ↔ k ∣ int.gcd b (a - n*b),
  ...stuff...
  have p₆ : int.gcd a b ∣ int.gcd b (a - n*b),

[rory]

I want to prove p6 using p5

[Johan Commelin]

Aha... yes, you can't change k. So you have to restate p₅ as \forall k : ℤ, ...

[Johan Commelin]

And so you should remove k from the hypotheses of prop4

[rory]

So there's no way for subgoals to share a \forall k generally

[Johan Commelin]

No... what you are asking for is an implicit universal quantifier. But how would Lean know if you want this or not

[Johan Commelin]

For all it knows, you might want to use the specific that you assumed something about somewhere else

[rory]

Okay, that makes sense

[Simon Hudon]

This might be an indication that you should write a separate lemma and use a variable declaration.