The `conv` tactic tries to close “trivial” goals after itself. As of
now, it uses
`try rfl`, which means it can close goals that are only trivial after
reducing with
default transparency. This is suboptimal
* this can require a fair amount of unfolding, and possibly slow down
the proof
a lot. And the user cannot even prevent it.
* it does not match what `rw` does, and a user might expect the two to
behave the
same.
So this PR changes it to `with_reducible rfl`, matching `rw`’s behavior.
I considered `with_reducible eq_refl` to only solve trivial goals that
involve equality,
but not other relations (e.g. `Perm xs xs`), but a discussion on mathlib
pointed out
that it’s expected and desirable to solve more general reflexive goals:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Closing.20after.20.60rw.60.2C.20.60conv.60.3A.20.60eq_refl.60.20instead.20of.20.60rfl.60/near/429851605
[Before](https://github.com/leanprover/lean4/files/14772220/oi.pdf) and
[after](https://github.com/leanprover/lean4/files/14772226/oi2.pdf).
This gets `ByteArray`, `String.Extra`, `ToString.Macro` and `RCases` out
of the imports of `omega`. I'd hoped to get `Array.Subarray` too, but
it's tangled up in the list literal syntax. Further progress could come
from make `split` use available `Decidable` instances, so we could pull
out `Classical` (and possibly some of `PropLemmas`).
