## Stream: new members

### Topic: trouble with introv

#### Charlie Conneen (Oct 19 2020 at 21:24):

As I understand it, introv is supposed to automatically introduce variables in a theorem. Looking over examples, it seems it should be able to simplify the forall in my hypothesis in the following example, but it doesn't:

import algebra.group.basic
universe u
variables {G : Type u} [group G]

lemma id_unique : ∃! e : G, ∀ x : G, e * x = x ∧ x * e = x :=
begin
apply exists_unique.intro (1 : G),
intros,
split,
exact one_mul x,
exact mul_one x,
introv h,
sorry
end


any ideas as to what's going on here? I thought applying introv where I did would produce 3 hypotheses, y : G, x : G and h : y * x = x ∧ x * y = x. But that's not quite what happens.

#### Alex J. Best (Oct 19 2020 at 21:26):

Can you include all the imports and defs in your #mwe so we can try it out and see what the goal state is?

#### Charlie Conneen (Oct 19 2020 at 21:26):

only import is algebra.group.basic

#### Alex J. Best (Oct 19 2020 at 21:27):

and variables {G : Type} [ group G] i'm guessing?

naturally

#### Charlie Conneen (Oct 19 2020 at 21:27):

well, {G : Type*}

#### Alex J. Best (Oct 19 2020 at 21:28):

Right but it helps people reading your question if you include those lines so we don't have to guess and type them out to see it in vscode!

#### Bryan Gin-ge Chen (Oct 19 2020 at 21:30):

Including all the imports, variable declarations, etc. also makes it so that your snippet will immediately work in the Lean playground (hover over the snippet and click one of the buttons that appears in the top right).

#### Charlie Conneen (Oct 19 2020 at 21:31):

I'm well aware, thank you, just forgot to include them when pasting in. I've edited the mwe

#### Alex J. Best (Oct 19 2020 at 21:33):

To answer your question anyway, introv is doing what it should, its introducing the hypothesis that ∀ (x : G), y * x = x ∧ x * y = x, there is an important difference between

∀ (y : G), (∀ (x : G), y * x = x ∧ x * y = x) → y = 1


and

∀ (y : G), ∀ (x : G), y * x = x ∧ x * y = x → y = 1


to proceed from where you are you can specialize h 1 to "evaluate the hypothesis" at a useful point.

#### Charlie Conneen (Oct 19 2020 at 21:36):

I see. The examples baked into Lean were a bit misleading at first glance, because this

example : ∀ a b : nat, a = b → ∀ c, b = c → a = c :=
begin
introv h₁ h₂,
exact h₁.trans h₂
end


initially seemed to be analogous to the context of the above lemma. Thanks for clarifying.

Last updated: May 13 2021 at 05:21 UTC