Strange term creation error

Stream: general

[Bhavik Mehta]

MWE:

import category_theory.types
import category_theory.monad.basic

open category_theory monad

@[simps]
def P : Type ⥤ Type :=
{ obj := λ X, set X,
  map := λ X Y, set.image }

def P_monad : monad P :=
{ η :=
  { app := λ Y x, ({x} : set Y),
    naturality' := by tidy },
  μ :=
  { app := λ Y x, set.sUnion x,
    naturality' := by tidy },
  left_unit' := by tidy,
  right_unit' := by tidy,
  assoc' := by tidy }

Each of the tidy seem to succeed, but the monad structure gives me this error:

type mismatch at application
  a_h_left_w a
term
  a
has type
  X_1
but is expected to have type
  X
types contain aliased name(s): X
remark: the tactic `dedup` can be used to rename aliases

[Bhavik Mehta]

Is something strange happening inside the tidy?

[Bhavik Mehta]

Replacing the tidy with the tactic script tidy? tells me gives the same error

[Markus Himmel]

Maybe it's https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20and.20dedup again?

[Bhavik Mehta]

Yeah that seems like the same problem

[Reid Barton]

I also just encountered this.

[Bhavik Mehta]

I think it should be fixed here: https://github.com/leanprover-community/lean/issues/236