Simp with funext and propext

Stream: general

[Patrick Johnson]

In Lean 4, when a theorem is marked as @[simp], does the elaborator automatically apply funext and propext before adding the theorem to the simp set? For example, does the following statement:

∀ (P Q : Prop), ¬(P ∧ Q) ↔ ¬P ∨ ¬Q

get transformed to

(λ (P Q : Prop) => ¬(P ∧ Q)) = (λ (P Q : Prop) => ¬P ∨ ¬Q)

and the new proof (proved implicitly) gets added to the simp set? Or does simp store the theorem as is, and apply funext and propext ad-hoc on the place of simplification?

[Floris van Doorn]

propext gets automatically added, so having ∀ (P Q : Prop), ¬(P ∧ Q) ↔ ¬P ∨ ¬Q as a simp lemma will/should be the same as having ∀ (P Q : Prop), ¬(P ∧ Q) = ¬P ∨ ¬Q. However, funext doesn't get automatically applied. If your simp lemma states f x = g x, then f '' s won't be simplified to g '' s. If you want that, you need to reformulate your lemma to f = g.
At least, that it my understanding of it.

[Praneeth Kolichala]

I believe that there is a higher_order attribute that does this automatically:

def f : ℕ → ℕ := sorry
def g : ℕ → ℕ := sorry

@[simp, higher_order] lemma f_eq_g (x : ℕ) : f x = g x := sorry

/- Without `higher_order` on f_eq_g, this does not work -/
example : f ∘ (+1) = g ∘ (+1) := by simp

[Eric Wieser]

docs#tactic.higher_order_attr