is this in mathlib?

Stream: general

[Scott Morrison]

Does

@[simp] lemma set.Union_range {α : Sort*} {β : Sort*} {γ : Sort*} (f : α → β) (g : β → set γ) :
  (⋃(b : β)(H : b ∈ range f), g b) = (⋃(a : α), g (f a)) := ...

exist in mathlib?

[Scott Morrison]

Relatedly, I want to add the following to measurable_space.lean:

@[simp] theorem is_measurable_sup {m₁ m₂ : measurable_space α} {s : set α} :
  @is_measurable _ (m₁ ⊔ m₂) s ↔ generate_measurable (m₁.is_measurable ∪ m₂.is_measurable) s := ...

@[simp] theorem is_measurable_Sup {ms : set (measurable_space α)} {s : set α} :
  @is_measurable _ (Sup ms) s ↔ generate_measurable (⋃₀ (measurable_space.is_measurable '' ms)) s := ...

@[simp] theorem is_measurable_supr {ι} {m : ι → measurable_space α} {s : set α} :
  @is_measurable _ (supr m) s ↔ generate_measurable (⋃i, (m i).is_measurable) s := ...

Do they seem reasonable? Or are lemmas that expose generate_measurable morally wrong for some reason?

[Yury G. Kudryashov]

Please enable syntax highlighting. Look at set.bUnion_range.

[Yury G. Kudryashov]

in data/set/lattice

[Scott Morrison]

Thanks. I will experiment to see if it can be given @[simp].

[Scott Morrison]

(I should remember to try library_search. :-)

[Yury G. Kudryashov]

Probably mem_range will come earlier.

[Scott Morrison]

What do you mean "come earlier"?

[Yury G. Kudryashov]

simp works inside out, so it will first try to rewrite b ∈ range f.

[Yury G. Kudryashov]

Though I'm not sure if simp can simplify inside binders.

[Scott Morrison]

Seems not. (Also: the linter that complains about LHS of simp lemmas not in simp-normal form doesn't complain.)