rw not working

Stream: general

[Bernd Losert]

For some reason, the rw here is not working. What am I missing?

import tactic
import data.set.pointwise

open set
open_locale pointwise

example {α : Type*} (s t : set α) [has_inv α] : nat :=
begin
  have hsub : has_inv.inv '' t ⊆ s, sorry,
  have hsub' : t⁻¹ ⊆ s, by rw image_inv,
end

[Yaël Dillies]

Shouldn't it be rwa image_inv at hsub?

[Bernd Losert]

Let me try...

[Bernd Losert]

I changed it to:

  have hsub : has_inv.inv '' t ⊆ s, sorry,
  rwa image_inv at hsub,

but it still does not work.

[Yaël Dillies]

I meant

example {α : Type*} (s t : set α) [has_inv α] : nat :=
begin
  have hsub : has_inv.inv '' t ⊆ s, sorry,
  have hsub' : t⁻¹ ⊆ s, by rwa image_inv at hsub,
end

[Bernd Losert]

That does not work either.

[Yaël Dillies]

Yeah because docs#set.image_inv requires has_involutive_inv α, not just has_inv α.

[Bernd Losert]

Ah, I see. The error was confusing me. I didn't realize that was the problem.

[Bernd Losert]

What's the difference between rw and rwa?

[Yaël Dillies]

rwa is rw + assumption

[Bernd Losert]

Interesting. Thanks.

[Eric Wieser]

This fails because docs#set.has_inv is surprisingly defined in terms of the preimage not the image

[Eric Wieser]

They're equivalent when inv is involutive, but when it's not this definition is kind of weird

[Eric Wieser]

There's another thread about this I made a few months ago

[Yaël Dillies]

Yes I agree. I believe it should be change to the image because it would make all the set.image2 API work with it.

[Eric Wieser]

We'd probably want to change docs#submonoid.has_inv as well to remain defeq Nevermind, it's already defined in terms of the set operator

[Floris van Doorn]

My experience is that the preimage is nicer to work with than image (has better properties - e.g. topologically; has nicer definitional behavior). Therefore I defined docs#set.has_inv in terms of preimage.