mathlib

43519fc7 - feat(tactic/lint/misc): unused arguments checks for more sorry's (#10431)

feat(tactic/lint/misc): unused arguments checks for more sorry's (#10431) * The `unused_arguments` linter now checks whether `sorry` occurs in any of the `_proof_i` declarations and will not raise an error if this is the case * Two minor changes: `open tactic` in all of `meta.expr` and fix a typo. * I cannot add a test without adding a `sorry` to the test suite, but this succeeds without linter warning: ```lean import tactic.lint /-- dummy doc -/ def one (h : 0 < 1) : {n : ℕ // 0 < n} := ⟨1, sorry⟩ #lint ``` Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>