projections of structure instances?

Stream: mathlib4

[Kim Morrison]

When I'm looking at a goal like

x : SemigroupCat
y : ↑({ obj := fun S ↦ of (WithOne ↑S), map := fun {X Y} ↦ WithOne.map }.obj x)
⊢ (WithOne.map (𝟙 x)) y = y

I want to start by reducing the { obj := ..., ... }.obj in the type of y to the value of the obj field.

I feel like I'm going crazy --- doesn't simp (or dsimp) usually do this out of the box?

[Eric Wieser]

When I've seen this fail in the past it's due to a semireducible type synonym being partially unfolded somewhere in the statement.

[Kim Morrison]

I can use simp only [Prefunctor.mk_obj] at y, but I can't make Prefunctor.mk_obj a simp lemma, because its head is a variable (after whnfR)!

[Kim Morrison]

Hmm, so far failing to see anything wrong even with pp.all.

Here's the code:

import Mathlib

open CategoryTheory

def adjoinOne' : SemigroupCat.{u} ⥤ MonCat.{u} where
  obj S := MonCat.of (WithOne S)
  map := WithOne.map
  map_id x := by ext y; dsimp at *; simp only [Prefunctor.mk_obj] at y; sorry
  map_comp := WithOne.map_comp

[Kim Morrison]

The simp only shouldn't be needed, I hope.

[Eric Wieser]

simp only at y works here (but only after the dsimp)

[Eric Wieser]

In fact, dsimp at y ⊢ works too, it's dsimp at * that fails

[Kim Morrison]

Okay, that is a bit weird.

[Kim Morrison]

Just simp at y seems fine too.

[Eric Wieser]

Well, this wouldn't be the first time that * behaves weirdly