# Zulip Chat Archive

## Stream: new members

### Topic: Reassign variable value

#### rory (Nov 06 2019 at 10:06):

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 (Nov 06 2019 at 10:11):

Can you give a bit more context?

#### Johan Commelin (Nov 06 2019 at 10:11):

I'm not sure I understand what the problem is

#### rory (Nov 06 2019 at 10:13):

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 (Nov 06 2019 at 10:14):

I want to prove p6 using p5

#### Johan Commelin (Nov 06 2019 at 10:15):

Aha... yes, you can't change `k`

. So you have to restate `p₅`

as `\forall k : ℤ, ...`

#### Johan Commelin (Nov 06 2019 at 10:16):

And so you should remove `k`

from the hypotheses of `prop4`

#### rory (Nov 06 2019 at 10:18):

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

generally

#### Johan Commelin (Nov 06 2019 at 10:20):

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

#### Johan Commelin (Nov 06 2019 at 10:21):

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

#### rory (Nov 06 2019 at 10:21):

Okay, that makes sense

#### Simon Hudon (Nov 06 2019 at 14:40):

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

declaration.

Last updated: May 08 2021 at 10:12 UTC