Simp hypothesis, then simp goal with hypothesis?

Stream: Is there code for X?

[Robert Maxton]

In the effort to avoid both non-terminal simps and messy/fragile long simp only [...]s, it'd be cool to be able to say in one command "simp at h; simp [h]" with h specifically. I know simp_all can do that, but afaik it tries _all_ hypotheses which is often not desired. Is there a config or secret tactic that already does this?

[Aaron Liu]

simp [by simpa using h]?

[Robert Maxton]

.... Guess that counts. Thanks!

[Kyle Miller]

Hmm, that's clever, but I'm not sure this counts as avoiding a non-terminal simp!

[Kyle Miller]

It's still fragile since there's not a checkpoint for the simplified type.

Best would be

have : theType := by simpa using h
simp [this]

but my opinion is that simp at h; simp [h] isn't any worse than simp_all.

[Jz Pan]

simp [show theType by simpa using h]

[Floris van Doorn]

In my opinion, I want to use simp at h; simp [h] quite often as a finishing tactic, and it seems pretty innocent to me. It's pretty maintainable, since most things that simplify h also simplify the goal.
It's often more useful than simpa using h, since it can use h to rewrite subterms of the goal. And unlike simpa using h, it doesn't do an assumption up to defeq, which itself is very brittle, and can break proofs by adding more simp-lemmas.

import Lean
-- simpa brittleness

def Foo (n : Nat) := n % 2 = 0

example {n : Nat} (h : Foo n) : n % 2 = 0 := by simpa using h -- works

@[simp] theorem foo_iff {n : Nat} : Foo n ↔ (n + 1) % 2 = 1 := sorry

example {n : Nat} (h : Foo n) : n % 2 = 0 := by simpa using h -- fails

[Ruben Van de Velde]

Maybe simp_all?