mathlib3

b9fbef82 - feat(tactic/observe): have a claim proved by library_search under the hood (#10878)