mathlib3

4b1c83f1 - feat(data/pfun): tooling to help reasoning about pfun domains (#15313)

feat(data/pfun): tooling to help reasoning about pfun domains (#15313) Tooling to help reasoning about pfun domains. Helps solving problems such as: ```lean -- Informal: Find the domain of the function $g(x) = \sqrt{x-2}$. Express your answer using intervals notation. example : (pfun.sqrt.comp $ pfun.lift (λ x : ℝ, x - 2)).dom = set.Ici 2 := begin have h₀ : (pfun.sqrt).dom = set.Ici 0, { refl }, simp only [pfun.lift_eq_coe, pfun.dom_comp], rw [h₀, pfun.coe_preimage], ext, simp only [set.preimage_sub_const_Ici, zero_add], end ``` Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Stanislas Polu <spolu@openai.com>