Exists and simp_rw

Stream: mathlib4

[Winston Yin]

In this part of Data.Set.Basic, simp_rw seems to have lost functionality from mathlib3.

simp_rw [th] in mathlib3 can rewrite ∃ h : p, ..., where p can be proven using theorem th, into ∃ h : true, ..., but is unable to do so in mathlib4.

On a separate note, Exists is not rendered as ∃ h : p, ... in the infoview but as Exists fun h ↦ ..., making it difficult to see the type of each quantity that exists.

[Kevin Buzzard]

I think that both of these issues have already been raised as issues in lean 4 or mathlib 4 (but am not in a position to check right now)

[Heather Macbeth]

Winston Yin said:

On a separate note, Exists is not rendered as ∃ h : p, ... in the infoview but as Exists fun h ↦ ..., making it difficult to see the type of each quantity that exists.

@Winston Yin Here is a previous discussion of this point:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Pretty.20printing.20of.20existential.20quantifier.20broken

It comes from an over-hasty implementation of the ↦ notation. Medium-term we would like these notations not to conflict, short-term (until someone has the energy to write a more principled implementation, probably in core rather than just mathlib) we need to pick one.

[Heather Macbeth]

Winston Yin said:

simp_rw [th] in mathlib3 can rewrite ∃ h : p, ..., where p can be proven using theorem th, into ∃ h : true, ..., but is unable to do so in mathlib4.

I don't remember seeing this one discussed elsewhere but maybe someone else can point you to it.

[Kevin Buzzard]

Sorry -- I wrote that comment when I was away from Lean and then forgot about it. this was what I was referrring to with simp not being able to rewrite p to true even with h : p <-> true. To be honest I'm still not entirely sure I understand what's going on properly here. I'm hoping that the issue here is covered either by https://github.com/leanprover/lean4/issues/1937 or https://github.com/leanprover/lean4/issues/1926 .