using multiplication halfway through constructing a monoid

Stream: new members

[Jack J Garzella]

I'm attempting to prove one_mul to show that my type of interest is a monoid, and though the goal involves multiplication, i.e.

M: Type u
a: M
⊢ 1 * a = a

when I try to multiply two elements of M, Lean cannot deduce that the type M satisfies has_mul. Here is my #mwe:

import algebra.category.Mon

noncomputable theory

universes u v

variables (M : Type u)

lemma M_is_monoid : monoid M
:= {
  mul := sorry,
  one := sorry,
  one_mul :=
  begin
    intro a,
    have my_goal : (a = 1 * a),
      by sorry,
    exact my_goal,
  end,
  mul_one := sorry,
  mul_assoc := sorry,
}

How can I prove an equality like a = 1 * a with out using *? Alternatively, how do I get Lean to realize that * means apply the mul function I gave it earlier?

[Jack J Garzella]

^^ I've noticed I'm missing an eq.symm, but including it doesn't fix the issue.

[Eric Wieser]

One easy way out is to define has_mul first separately

[Calvin Lee]

this one is really throwing me through a loop because it's giving me an error even if has_mul and has_one are defined...

import algebra.category.Mon

noncomputable theory

universes u

variables (M : Type u)

def M_has_mul : has_mul M := { mul := sorry }
def M_has_one : has_one M := { one := sorry }

def M_is_monoid : monoid M :=
{
  one_mul := begin
    intro a,
    have : has_mul M := M_has_mul M,
    have my_goal : (a = (1 : M) * a),
      by sorry,
    exact my_goal,
  end,
  mul_one := sorry,
  mul_assoc := sorry,
  ..(M_has_mul M),
  ..(M_has_one M),
}

[Eric Wieser]

The have is harmful there

[Eric Wieser]

You should use letI instead

[Eric Wieser]

Although this looks possibly overly minimized; are you really trying to show every type is a monoid?

[Jack J Garzella]

I was able to get @Eric Wieser 's suggestion to work by using the instance instead of def.

[Jack J Garzella]

It doesn't feel great to have the extra boilerplate, but idk what else to do.

[Jack J Garzella]

And no, this was a toy #mwe extracted from another situation where the statement I'm trying to prove is actually true.

[Eric Wieser]

Can you adjust your mwe to use def M : Type := sorry instead?

[Eric Wieser]

Because using a variable is weird enough that you need lots of workarounds that wouldn't be needed by the original code