mathlib

d3c943b7 - refactor(data/set/lattice): add congr lemmas for `Prop`-indexed `Union` and `Inter` (#8260)

refactor(data/set/lattice): add congr lemmas for `Prop`-indexed `Union` and `Inter` (#8260) Thanks to new `@[congr]` lemmas `Union_congr_Prop` and `Inter_congr_Prop`, `simp` can simplify `p y` in `⋃ y (h : p y), f y`. As a result, LHS of many lemmas (e.g., `Union_image`) is no longer in `simp` normal form. E.g., ```lean lemma bUnion_range {f : ι → α} {g : α → set β} : (⋃x ∈ range f, g x) = (⋃y, g (f y)) := ``` can no longer be a `@[simp]` lemma because `simp` simplifies `⋃x ∈ range f, g x` to `⋃ (x : α) (h : ∃ i, f i = x), g x`, then to `⋃ (x : α) (i : α) (h : f i = x), g x`. So, we add ```lean @[simp] lemma Union_Union_eq' {f : ι → α} {g : α → set β} : (⋃ x y (h : f y = x), g x) = ⋃ y, g (f y) := ``` Also, `Union` and `Inter` are semireducible, so one has to explicitly convert between these operations and `supr`/`infi`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>