## Stream: general

### Topic: congr for unions

#### 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?

#### 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