A purer version of `try` or `any_goals`?

Stream: new members

[Dan Plyukhin]

I have a proof where a lot of cases can be solved by simp_all, but there's one case where simp_all does too much simplification and the goal becomes unreadable.

/-- A function mapping elements of `ps` to elements of `qs`.
  It's injective over `ps`. -/
def listMap [DecidableEq α] : (ps : List α) → (qs : List α) → α → α
  | p::ps, q::qs, r =>
    if p = r then q else listMap ps qs r
  | _, _, r => r

lemma listMap.inj_on [DecidableEq α] (ps : List α) (ps_nodup: ps.Nodup)
  (qs : List α) (qs_nodup: qs.Nodup) (length_eq : ps.length = qs.length) :
  let σ := listMap ps qs
  ∀ p₁ ∈ ps, ∀ p₂ ∈ ps, σ p₁ = σ p₂ → p₁ = p₂
:= by
  -- The proof follows by induction on ps and pattern matching on qs.
  induction ps generalizing qs <;> cases qs
  -- Most cases are trivial.
  any_goals simp_all
  -- The interesting case is when ps=p::ps' and qs=q::qs'.
  case cons q qs' p ps' ih =>
    admit -- Oh no: The goal looks too complicated now!

Is there a version of try or any_goals that reverts the effects of simp_all in the last case?

[Yaël Dillies]

What about any_goals simp_all; done?

[Dan Plyukhin]

Beautiful, thanks!