setrel in uniformity isrefl

Stream: Is there code for X?

[Aaron Liu]

I am updating an old PR which I haven't touched in a while. In there I use apply subset_comp_self. I see that

`subset_comp_self` has been deprecated: Use `SetRel.left_subset_comp` instead

Note: The updated constant has a different type:
  ∀ {α : Type u_1} {β : Type u_2} {S : SetRel β β} {R : SetRel α β} [S.IsRefl], R ⊆ R ○ S
instead of
  ∀ {α : Type ua} {s : SetRel α α}, idRel ⊆ s → s ⊆ s ○ s

so I do have : o₂.choose.IsRefl := sorry and exact SetRel.left_subset_comp instead.

Then I need to fill in the sorry. I can't find any lemmas mentioning both uniformity and SetRel.IsRefl. So basically I need

import Mathlib

theorem SetRel.IsRefl.of_mem_uniformity {α : Type ua} [UniformSpace α]
    {s : SetRel α α} (h : s ∈ uniformity α) : s.IsRefl where
  refl _ := refl_mem_uniformity h

[Aaron Liu]

More generally, how am I supposed to interact with SetRel.IsRefl and SetRel.IsSymm?

[Yaël Dillies]

Here's the typical fix: https://github.com/leanprover-community/mathlib4/pull/23181/files#diff-fdbc173f0c400ff3a4b371e3766122d99266ef7f7bb8fbeac6a87b38fe372e7dR71

[Yaël Dillies]

You could add a direct lemma if you want

[Aaron Liu]

yes that's great but I have another one

import Mathlib

example {α : Type u} (r s : SetRel α α) [hr : r.IsSymm] [hs : s.IsSymm] :
    (r.comp (s.comp r)).IsSymm := by
  -- this proof doesn't work anymore
  -- simp [IsSymm, compRel_assoc, prodSwap_preimage_compRel,
  --   hr.eq, hs.eq]
  sorry

[Yaël Dillies]

Maybe just do this one by hand? Your current proof is fiddly rewrites, and tauto should be your friend

[Aaron Liu]

It's using that IsSymmetricRel s is defined as Prod.swap ⁻¹' s = s and then push the Prod.swap ⁻¹' through the comp

[Aaron Liu]

I wouldn't really say it's "fiddly"

[Aaron Liu]

Oh I just found docs#SetRel.inv_eq_self_iff

[Aaron Liu]

ok I can probably do this proof the same way then