toCases — Mathlib

Lean4
/-- Proves the left to right direction of a generated iff theorem.
`shape` is the output of a call to `constrToProp`.
-/
def toCases (mvar : MVarId) (shape : List Shape) : MetaM Unit := do
  let ⟨h, mvar'⟩ ← mvar.intro1
  let subgoals ← mvar'.cases h
  let _ ←
    (shape.zip subgoals.toList).zipIdx.mapM fun ⟨⟨⟨shape, t⟩, subgoal⟩, p⟩ ↦ do
        let vars := subgoal.fields
        let si := (shape.zip vars.toList).filterMap (fun ⟨c, v⟩ ↦ if c then some v else none)
        let mvar'' ← select p (subgoals.size - 1) subgoal.mvarId
        match t with
        | none =>
          do
            let v := vars[shape.length - 1]!
            let mv ← mvar''.existsi (List.init si)
            mv.assign v
        | some n =>
          do
            let mv ← mvar''.existsi si
            splitThenConstructor mv (n - 1)
  pure ()
Похожие утверждения