splitThenConstructor — Mathlib

Lean4
/-- Splits the goal `n` times via `refine ⟨?_,?_⟩`, and then applies `constructor` to
close the resulting subgoals.
-/
def splitThenConstructor (mvar : MVarId) (n : Nat) : MetaM Unit :=
  match n with
  | 0 => do
    let (subgoals', _) ←
      Term.TermElabM.run <|
          Tactic.run mvar do
            Tactic.evalTactic (← `(tactic| constructor))
    let [] := subgoals' |
      throwError"expected no subgoals"
    pure ()
  | n + 1 => do
    let (subgoals, _) ←
      Term.TermElabM.run <|
          Tactic.run mvar do
            Tactic.evalTactic (← `(tactic| refine ⟨?_, ?_⟩))
    let [sg1, sg2] := subgoals |
      throwError"expected two subgoals"
    let (subgoals', _) ←
      Term.TermElabM.run <|
          Tactic.run sg1 do
            Tactic.evalTactic (← `(tactic| constructor))
    let [] := subgoals' |
      throwError"expected no subgoals"
    splitThenConstructor sg2 n
Похожие утверждения