trouble with introv

Stream: new members

[Charlie Conneen]

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]

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]

only import is algebra.group.basic

[Alex J. Best]

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

[Charlie Conneen]

naturally

[Charlie Conneen]

well, {G : Type*}

[Alex J. Best]

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]

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]

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

[Alex J. Best]

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]

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.