data.set.image

Stream: mathlib4

[Scott Morrison]

In mathlib4#949 we have lots of theorems that look like:

theorem preimage_coe_compl' (s : Set α) :
  (Subtype.val : (sᶜ : Set α) → α) ⁻¹' s = ∅ :=
  preimage_coe_eq_empty.2 (compl_inter_self s)

that previously were written using coe. For now I've just left a porting note about this, and may merge soon, but I want to discuss what we should be doing here.

Options:

1. use Subtype.val as in the current statements.
2. write fun x : s => (x : α) (which Lean will compile to Subtype.val anyway!)
3. introduce a new def synonym of Subtype.val for this purpose.

[Scott Morrison]

I think my inclination is: go with 1. while porting, but consider when we might switch to 3.

[Winston Yin]

Currently there are copies of theorems in both 1 and 2

[Mario Carneiro]

I don't see why to have a synonym for Subtype.val

[Mario Carneiro]

it seems like a perfectly good normal form

[Scott Morrison]

We've talked about breaking the defeq of Set and ⬝ → Prop, after which presumably it wouldn't be Subtype.val anymore, but still would be fun x : s => (x : α).