toLex fst snd simp

Stream: mathlib4

[Eric Paul]

Should mathlib have the following simp lemmas?

import Mathlib

@[simp]
theorem toLex_fst (a : A) (b : B) : (toLex (a,b)).1 = a := rfl

@[simp]
theorem toLex_snd (a : A) (b : B) : (toLex (a,b)).2 = b := rfl

I came across wanting these when I was talking about the linear order {x : ℕ ×ₗ A | x.1 = n} for some n and linear order A and wanted to say that some specific pair toLex (n, a) was in the set.

[Yaël Dillies]

These .1 and .2 are not well-typed (they have domain _ × _), so I would say "no"

[Eric Paul]

Oh right, thanks! I keep making this mistake. The solution is instead to define the set I care about as {x : ℕ ×ₗ A | (ofLex x).1 = n} and then everything works.

[Eric Paul]

I wish that the definition of Lex was sealed or something so that I could not accidentally use the defeq.

[Yaël Dillies]

We might do that eventually :slight_smile:

[Eric Paul]

Following up on this, I've been adding the following to my files.

seal OrderDual
seal Lex

However, I now encountered an issue when doing that. The following simp call gives an error saying there is an invalid projection only when I have seal OrderDual.

import Mathlib

seal OrderDual

def mwe [LinearOrder α] (A : Set α) : α ≤i Aᵒᵈ where
  toFun x := sorry
  inj' := sorry
  map_rel_iff' := sorry
  mem_range_of_rel' := by
    simp

Interestingly, if I replace the simp call with what simp? returns without the seal OrderDual, then it does work:

import Mathlib

seal OrderDual

def mwe [LinearOrder α] (A : Set α) : α ≤i Aᵒᵈ where
  toFun x := sorry
  inj' := sorry
  map_rel_iff' := sorry
  mem_range_of_rel' := by
    simp only [RelEmbedding.coe_mk, Function.Embedding.coeFn_mk, Set.mem_range, exists_const_iff,
      OrderDual.forall, Subtype.forall]

[Eric Paul]

In a less minimized mwe, the error does not go away when replacing simp with simp?. It appears the error is coming from using RelEmbedding.coe_mk

import Mathlib

seal OrderDual

def mwe [LinearOrder α] (A B : Set α) : (A ∩ B : Set α)ᵒᵈ ≤i Aᵒᵈ where
  toFun x := OrderDual.toDual
    ⟨(OrderDual.ofDual x).val, (OrderDual.ofDual x).prop.1⟩
  inj' := by simp [Function.Injective]
  map_rel_iff' := by simp
  mem_range_of_rel' := by
    rw [RelEmbedding.coe_mk]