A nice simp feature for conjunctions

Stream: lean4

[Kyle Miller]

I just learned about a feature in simp that I wasn't aware of, which didn't exist in Lean 3 (and which I had been wanting).

Simp will normalize lemmas you give it to produce some list of the actual simp lemmas. The following is the same as simp [h.1, h.2]:

example (h : x = 3 ∧ y = 4) : x + y = 7 := by
  simp [h]

Also when you add @[simp] to a conjunction, it gives you multiple simp lemmas:

axiom n : Nat
axiom m : Nat

@[simp]
axiom h : n = 3 ∧ m = 4

example : n + m = 7 := by simp

[Gabriel Ebner]

which didn't exist in Lean 3

Both of your examples work just fine in Lean 3 (after changing Nat to nat).

[Kyle Miller]

Huh, so they do. Let's downgrade this PSA to "here's a neat simp feature that you've wanted that's been there all along"