monoid_hom type class error

Stream: new members

[Carlos Silva]

I have a monoid Y. I want to say that there is a monoid X such that a homomorphism f:X → Y exists and has some property. Here is how I tried to do that.

universes u v
variables {X : Type u} {Y : Type v}
def mon_recognizes [N : monoid Y] (Y : Type v) (L : set X) :=
∃ (M : monoid X) (f : X →* Y), L = f ⁻¹' (f '' L)

The problem appears at (f : X →* Y) and lean says it can't synthesize a type class instance for mul_one_class X. How do I fix this? I thought maybe I had to spell everything out.

∃ (M : monoid X) (f : X → Y),  @monoid_hom X Y
{one := M.one, mul := M.mul, one_mul := M.one_mul, mul_one := M.mul_one}
{one := N.one, mul := N.mul, one_mul := N.one_mul, mul_one := N.mul_one}

That didn't work. Maybe writing it all out will work and I'm just doing it wrong. Thanks for your help.

[Kevin Buzzard]

The X should be after the exists I guess, but your main problem can be solved by writing "by exactI" in an appropriate place. \exists M : monoid X, by exactI \exists f, ... or something like that should work (unchecked)