Quantifiers and type classes

Stream: new members

[Justin Pearson]

What is the correct way of using type classes and quantifiers? Randomly poking around mathlib didn't give me any help. I know that I can use theorems/lemma with parameters to do what I want, but please humour me.

How would I for example write a first order formula corresponding to (this is not valid Lean syntax) :
\forall M : Monoid, \forall N : Monoid, \forall f : M ->* N, blah

[Johan Commelin]

example : \forall {M N : Type*} [hM : monoid M] [hN : monoid N],
  by exactI \forall (f : M ->* N), blah

[Justin Pearson]

Great thanks. The exactI was the trick that I was missing.

[Johan Commelin]

@Justin Pearson What it does is resetting the instance cache, which gets frozen after example :