squeeze_simp oddity

Stream: general

[Chase Meadors]

MWE:

example {α : Type} [complete_lattice α] {s : finset α} (x : α) (h : x = ⨆ x ∈ (↑s : set α), x) :
  Prop :=
begin
  simp at h,                        -- Works
  simp only [finset.mem_coe] at h,  -- squeeze_simp suggestion, doesn't work
end

The context is

h: x = ⨆ (x : α) (H : x ∈ ↑s), x

And I simply want to remove the coe. Simp can do it, but the squeeze_simp suggestion fails. Any idea why? rw finset.mem_coe at h doesn't want to do anything either.

[Bryan Gin-ge Chen]

Hmm, I can't say I know what's going on here either. With set_option trace.simplify true before the example, the relevant part of the output of simp at h is this:

[simplify] eq: x = ⨆ (x : α) (H : x ∈ ↑s), x
[simplify] eq: x
[simplify] eq: ⨆ (x : α) (H : x ∈ ↑s), x
[simplify.canonize]
complete_lattice.to_has_Sup α
==>
complete_lattice.to_has_Sup α
[simplify] eq: λ (x : α), ⨆ (H : x ∈ ↑s), x
[simplify] eq: ⨆ (H : x ∈ ↑s), x
[simplify.canonize]
complete_lattice.to_has_Sup α
==>
complete_lattice.to_has_Sup α
[simplify] iff: x ∈ ↑s
[simplify.canonize]
set.has_mem
==>
set.has_mem
... lots of failures skipped ...
5. [simplify.rewrite] [finset.mem_coe]: x ∈ ↑s ==> x ∈ s
[simplify.canonize]
finset.has_mem
==>
finset.has_mem
... lots of failures skipped ...

The full output of simp only [finset.mem_coe] at h seems to be missing the [simplify] iff: x ∈ ↑s, [simplify.canonize], set.has_mem part but I don't know enough about simp to know what can be done:

[simplify] eq: x = ⨆ (x : α) (H : x ∈ ↑s), x
[simplify] eq: x
[simplify] eq: ⨆ (x : α) (H : x ∈ ↑s), x
[simplify.canonize]
complete_lattice.to_has_Sup α
==>
complete_lattice.to_has_Sup α
[simplify] eq: λ (x : α), ⨆ (H : x ∈ ↑s), x
[simplify] eq: ⨆ (H : x ∈ ↑s), x
[simplify.canonize]
complete_lattice.to_has_Sup α
==>
complete_lattice.to_has_Sup α
[simplify] eq: λ (H : x ∈ ↑s), x
[simplify] eq: x
[simplify] eq: supr
[simplify] eq: supr
[simplify] eq: eq

(By the way, it's not a MWE unless I can copy and paste it into my editor completely mindlessly. In this case the example is missing imports, but import tactic works.)

[Chase Meadors]

It's worth noting that a fairly inoffensive solution here would be something change x ∈ ↑s with x ∈ s at h, I don't know if it's possible to use change under binders like that (i.e., without copy-pasting the whole of h and changeing that).

[Eric Wieser]

Does dsimp behave any differently here?

[Bryan Gin-ge Chen]

I couldn't get dsimp to work at all with the example above.