Simp and structure projection problem

Stream: lean4

[Tomas Skrivan]

I have a simp lemma that behaves differently on projection Prod.fst : α × β → α and on a custom function my_fst : α × β → α.

The lemma is that an adjoint of composition is composition of adjoints: adjoint (λ x => f (g x)) = adjoint g ∘ adjoint f . Interestingly, the simplifier applies this lemma on adjoint Prod.fst with g = id but it does not apply this lemma on adjoint my_fst.

What is going on? Why is Prod.fst and my_fst treated by the simplifier differently? Is this an intended behavior? Is it an unfortunate consequence of another reasonable choice?

mwe:

variable {α β γ} [Inhabited α] [Inhabited β] [Inhabited γ]

constant adjoint : (α → β) → (β → α)

@[simp]
theorem adjoint_of_comp (f : β → γ) (g : α → β) :
  adjoint (λ x => f (g x)) = adjoint g ∘ adjoint f
  :=
  by sorry

@[simp]
theorem adjoint_of_fst :
  adjoint (Prod.fst : α × β → α) = fun x : α => (x, default)
  := by sorry

example : adjoint (Prod.fst : α × β → α) = fun x : α => (x, default)
  :=
by
  -- This applies `adjoint_of_comp` for some reason
  simp (config := { singlePass := true })

  simp -- infinite recursion
  done


constant my_fst : α × β → α

@[simp]
theorem adjoint_of_my_fst :
  adjoint (my_fst : α × β → α) = fun x : α => (x, default)
  := by sorry

example : adjoint (my_fst : α × β → α) = fun x : α => (x, default)
  :=
by
  simp
  done