Commit 2021-08-01 19:11 d3c943b7

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.,

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

@[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.