# Zulip Chat Archive

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

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

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