## 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