Zulip Chat Archive

Stream: general

Topic: congr for unions


view this post on Zulip Yury G. Kudryashov (May 08 2020 at 01:20):

The following example fails:

import data.set.lattice

example (α β : Type*) (p q : α  Prop) (h :  x, p x  q x) (s : α  set β) :
  ( (x : α) (hx : p x), s x) =  (x : α) (hx : q x), s x :=
by simp [h]

How can we make it work?

view this post on Zulip Yury G. Kudryashov (May 08 2020 at 01:22):

I guess that we need some congr lemma for Union but I'm not sure how exactly should it look like.


Last updated: May 13 2021 at 22:15 UTC