interactive

name	interactive
description	Fill a sorry one step at a time, directed by the user.

Interactive Mode

Work through a proof one step at a time, with the user directing each move.

Target: $ARGUMENTS

How this differs from /fill-sorry

/fill-sorry is autonomous — the agent tries tactics, searches Mathlib, and drives the proof to completion. /interactive is user-driven — the agent executes exactly what the user asks, shows the result, and waits.

Procedure

1. Read the target lemma and show the initial goal state via lean_goal at the sorry.
2. Wait for the user's instruction. The user will say something like "apply Functor.map_comp" or "simplify with simp" or "rewrite using h".
3. Convert the user's instruction into clean Lean tactic(s). Write the minimal code needed — nothing extra.
4. Edit the file, then check lean_diagnostic_messages with severity="error" on the edited line(s) (start_line/end_line) to confirm no errors, then show the new goal state with lean_goal. Use severity="error" to avoid linter warnings and infos bloating the output. A tactic can fail (e.g., "simp made no progress") while lean_goal on the next line still shows a goal (the unchanged one) — diagnostics catch this.
5. If diagnostics show an error, report it and revert. Do not attempt a fix unless the user asks.
6. Stop and wait. Do not attempt the next step, suggest tactics, or continue the proof unprompted.

Rules

• One step per turn. Only do what the user asked. No speculative next steps, no "while we're here" additions.