fix: split (for if-expressions) should work on non-propositional goals

[leodemoura]

Remark: when splitting an if-then-else term, the subgoals now have tags isTrue and isFalse instead of inl and inr.
closes #4313

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 28cf1cf5cfad0168d76d709a5e47fe4142a05fdc --onto 9d4696123693b2f0deee658b8021236e5168b4de. (2024-06-05 00:05:43)

[leodemoura]

@semorrison The split on if-then-else-terms now creates subgoals with tags isTrue and isFalse. Reason: it is internally performing cases on a Decidable p instead of an Or p (Not p). In principle, we could rename the tags to inl and inr, but I think the new tags are more informative than the old ones: inl and inr. Some proofs will break, but the impact on Mathlib should be small since they have their own split_if tactic.