simp failures?

Stream: lean4

[Michael Stoll]

import Mathlib

example (P Q : Prop) : P ∧ (P → Q) := by simp; sorry -- "simp made no progress"

example (P Q : Prop) : P → (P ∨ Q) := by simp; sorry -- "simp made no progress"

I would expect simp to change the first to P ∧ Q and the second to True.
If simp does not do that (and similar things), is there a tactic that simplifies a propositional term as far as possible? (tauto does not do it unless the result is True, since it is a finishing tactic.)

Motivation: in a proof coming up in #9240, I have a complicated propositional expression (an equivalence) that tauto does not clear, since for each direction, there is one extra reasoning step that is necessary. It would be nice to be able to produce a simplified version, so that it is easier to focus on the actual content.

[Ruben Van de Velde]

Does contextual:=true work?

[Michael Stoll]

Yes for the second example (as expected, I guess), but no for the first.

[Michael Stoll]

However, this works:

example (P Q : Prop) : P ∧ (P → Q) ↔ P ∧ Q := by simp (config := {contextual := true})

(simp by itself reduces it to the second example...)