mathlib3

51667657 - chore(order/filter/pointwise): Better definitional unfolding (#13941)

chore(order/filter/pointwise): Better definitional unfolding (#13941) Tweak pointwise operation definitions to make them easier to work with: * `1` is now `pure 1` instead of `principal 1`. This changes defeq. * Binary operations unfold to the set operation instead exposing a bare `set.image2` (`obtain ⟨t₁, t₂, h₁, h₂, h⟩ : s ∈ f * g` now gives `h : t₁ * t₂ ⊆ s` instead of `h : set.image2 (*) t₁ t₂ ⊆ s`. This does not change defeq.