traversableLawStarter — Mathlib

Lean4
/-- Run the following tactic:
```lean
intro _ .. x
dsimp only [Traversable.traverse, Functor.map]
induction x <;> (the simp tactic corresponding to s) <;> (tac)
```
-/
def traversableLawStarter (m : MVarId) (n : Name) (s : MetaM Simp.Context)
    (tac : Array FVarId → InductionSubgoal → MVarId → MetaM Unit) : MetaM Unit := do
  let s' ← [``Traversable.traverse, ``Functor.map].foldlM (fun s n => s.addDeclToUnfold n) ({ } : SimpTheorems)
  let (fi, m) ← m.intros
  m.withContext do
      if let (some m, _)← dsimpGoal m (← Simp.mkContext (simpTheorems := #[s'])) then
        let ma ← m.induction fi.back! (mkRecName n)
        ma.forM fun is =>
            is.mvarId.withContext do
              if let (some (_, m), _)← simpFunctorGoal is.mvarId (← s) then
                tac fi is m
Похожие утверждения