dsimp cannot reduce structure projection

Stream: lean4

[Eric Wieser]

Why is dsimp not able to reduce the structure projection here?

import Mathlib.Init.Data.List.Instances

example {A : Type} (a : A) (l : List {a : A // True}) : a ∈ (l : List A) := by
  -- nasty unfolding, this probably shouldn't be necessary
  unfold Lean.Internal.coeM instCoeT instCoeHTCT_1 instCoeHTC_1 instCoeOTC instCoeOTC_2
  unfold subtypeCoe CoeOTC.coe CoeT.coe CoeHTCT.coe CoeHTC.coe CoeOut.coe
  -- this doesn't make progress
  dsimp only
  sorry

[Eric Wieser]

The goal is

A: Type
a: A
l: List { a // True }
⊢ a ∈ do
  let a ← l
  pure
      {
          coe :=
            {
                  coe := fun a =>
                    { coe := fun a => { coe := fun a => { coe := fun a => a }.1 ({ coe := fun v => ↑v }.1 a) }.1 a }.1
                      a }.1
              a }.1

where I would very much hope the .1s cancel with the constructors

[Eric Wieser]

It seems simp only can make progress, but it's not clear to me why dsimp cannot

[Joachim Breitner]

Me neither. I tried dsimp (config := {proj := true}) only but same effect. Probably worth reporting as an issue!

[Eric Wieser]

lean4#3395