instance in condition

Stream: new members

[Adrián Doña Mateo]

Hi. Trying to define an induction principle for finite groups I've run into the following problem. It seems like one cannot introduce an instance in the condition of a lemma. I believe this is to do with Lean not updating the instance cache inside a proof. Is there any way to get this to work (perhaps using some tactics from here)? I realise I could simply have (hα : has add α) and then provide it manually when it is needed, but I would like to avoid that.

example (h : Π (α : Type*) [has_add α] (a : α), a + a = a) : true := trivial
-- failed to synthesize type class instance for has_add α

[Kevin Buzzard]

import tactic
example (h : Π (α : Type*) [has_add α] (a : α), by exactI a + a = a) : true := trivial

[Adrián Doña Mateo]

Oh, never thought it'd be that easy. Thanks!