nCasesSum — Mathlib

Lean4
/-- Calls `cases` on `h` (assumed to be a binary sum) `n` times, and returns
the resulting subgoals and their corresponding new hypotheses.
-/
def nCasesSum (n : Nat) (mvar : MVarId) (h : FVarId) : MetaM (List (FVarId × MVarId)) :=
  match n with
  | 0 => pure [(h, mvar)]
  | n' + 1 => do
    let #[sg1, sg2] ← mvar.cases h |
      throwError"expected two case subgoals"
    let #[Expr.fvar fvar1] ← pure sg1.fields |
      throwError"expected fvar"
    let #[Expr.fvar fvar2] ← pure sg2.fields |
      throwError"expected fvar"
    let rest ← nCasesSum n' sg2.mvarId fvar2
    pure ((fvar1, sg1.mvarId) :: rest)
Похожие утверждения