nCasesProd

Mathlib.Tactic.MkIffOfInductiveProp

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.MkIff.nCasesProd

Lean4

/-- Calls `cases` on `h` (assumed to be a binary product) `n` times, and returns
the resulting subgoal and the new hypotheses.
-/
def nCasesProd (n : Nat) (mvar : MVarId) (h : FVarId) : MetaM (MVarId × List FVarId) :=
  match n with
  | 0 => pure (mvar, [h])
  | n' + 1 => do
    let #[sg] ← mvar.cases h |
      throwError"expected one case subgoals"
    let #[Expr.fvar fvar1, Expr.fvar fvar2] ← pure sg.fields |
      throwError"expected fvar"
    let (mvar', rest) ← nCasesProd n' sg.mvarId fvar2
    pure (mvar', fvar1 :: rest)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru