Apply tactic to all side-conditions created by rw

Stream: Is there code for X?

[Joachim Breitner]

Is there a way to pass a discharger to rewrite or rw, i.e. a tactic to be run on all new goals created by rw? For example in

def overlap : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n+1 => overlap n

example : overlap 3 = 1 := by
  rewrite [overlap, overlap, overlap]
  rfl
  all_goals simp

I’d like to write something like

example : overlap 3 = 1 := by
  rewrite [overlap, overlap, overlap] using simp
  rfl

or in other cases maybe rewrite [… ] using assumption.

Or else a rw-independent good way of saying “run tactic x on all goals except the first”?

[Anand Rao Tadipatri]

There doesn't seem to be any relevant configuration option in docs#Lean.Meta.Rewrite.Config. Here's my attempt at writing a with_discharger tactic to operate on all side-goals created by the main tactic:

import Lean

open Lean Elab Meta Tactic

elab tac:tactic " with_discharger " disch:tactic : tactic => withMainContext do
  evalTactic tac
  let (_mainGoal :: sideGoals) ← getUnsolvedGoals | return -- (no goals to be solved)
  for sideGoal in sideGoals do
    let newSideGoals ← evalTacticAt disch sideGoal
    unless newSideGoals.isEmpty do
      throwError m!"Failed to close goal {sideGoal} with {disch}"

The example with this tactic looks like

def overlap : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n+1 => overlap n

example : overlap 3 = 1 := by
  rewrite [overlap, overlap, overlap] with_discharger simp
  rfl

[Joachim Breitner]

That’s neat! I wonder if this just doesn’t come up too often, or why it doesn’t exist already.