RFC: include RHS of implication in discrimination tree key for `simp`

Proposal

Right now, some useful lemmas about implications have a very general discrimination tree key:

theorem forall_eq_or_imp₀ {P Q : α → Prop} :
    (∀ a, a = a' ∨ Q a → P a) ↔ P a' ∧ ∀ a, Q a → P a := by
  simp only [or_imp, forall_and, forall_eq]

/-- info: ∀  _ -/
#guard_msgs in
#discr_tree_simp_key forall_eq_or_imp₀

This remains true for non-dependent arrows:

theorem imp_or_left_iff_true₀ {P Q : Prop} : (P → P ∨ Q) ↔ True := by
  simpa using Or.inl

/-- info: ∀  _ -/
#guard_msgs in
#discr_tree_simp_key imp_or_left_iff_true₀

Right now, some of these lemmas, like forall_eq_or_imp, forall_const, forall_self_imp, and so on, are part of the simp set and are tried very very often.

There are more lemmas which we would like to be in the simp set, but which we don't put in there in order to not make the situation even worse, cf. #12977.

It would be great to have simp key a lemma like forall_eq_or_imp by something like ∀ _ (Or _ _) or even ∀ _ (Or (Eq _ _) _).

From the numbers at #12949, which don't remove all offending simp annotations, only those which can be removed without touching many files, it seems likely that improving the discimination tree key of all of the relevant lemmas could improve the core build instructions by something like 1%, and likely more for mathlib.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by locating the implementation of the #discr_tree_simp_key command and the discrimination-tree key generation used by simp. Reproduce the guarded examples for forall_eq_or_imp₀ and imp_or_left_iff_true₀, then investigate how implication and disjunction RHS structure is represented. Done means the relevant keys include that structure without regressions in the existing simp behavior.