simplify `(a, b).fst` to `a`

Stream: general

[Yury G. Kudryashov]

Does Lean need a simp lemma for this?

[Kenny Lau]

I think it's one of the simp options (delta? iota?)

[Yury G. Kudryashov]

dsimp unfolds it, simp (sometimes?) fails.

[Yury G. Kudryashov]

The problem with all those "greek letter" reductions is that those who understand them probably don't understand why, e.g., wiki is not very helpful for others.

[Yury G. Kudryashov]

I hope someone will do #2102

[Reid Barton]

If simp fails when dsimp succeeds then I would guess it's because something else depends on this value and adding a simp lemma would make no difference.