mem ofDual iff

Stream: Is there code for X?

[Xavier Roblot]

Today, I needed the following result:

import Mathlib

example {G : Type*} [Group G] (H : Subgroup G) (x : G) :
    x ∈ OrderDual.ofDual H ↔ x ∈ H := Iff.of_eq rfl

It is of course very easy to prove (well, the proof is included :wink:) but I thought it could be a useful result to generalize and to add to Mathlib as a simp lemma but I am having a hard time finding out what would be the right generalization. The obvious thing:

import Mathlib

example {α : Type*} (s : Set α) (x : α) :
    x ∈ OrderDual.ofDual s ↔ x ∈ s :=

doesn't even typecheck.

[Yaël Dillies]

ofDual H doesn't make sense already: you don't have H : ?αᵒᵈ for some ?α.

[Xavier Roblot]

So basically what you're saying is that I should not be in a position to need this lemma in this first place...

[Xavier Roblot]

Oh, I see my mistake. Thanks!

[Yaël Dillies]

One day, OrderDual will be made a one-field structure and these confusions will disappear. But for now it is simply too practical