finCasesAt — Mathlib

Lean4
/-- Implementation of the `fin_cases` tactic. -/
partial def finCasesAt (g : MVarId) (hyp : FVarId) : MetaM (List MVarId) :=
  g.withContext
    (do
      let type ← hyp.getType >>= instantiateMVars
      match ← getMemType type with
      | some _ =>
        unfoldCases g hyp (userNamePre := ← g.getTag)
      | none =>
        -- Deal with `x : A`, where `[Fintype A]` is available:

        let inst ← synthInstance (← mkAppM ``Fintype #[type])
        let elems ← mkAppOptM ``Fintype.elems #[type, inst]
        let t ← mkAppM ``Membership.mem #[elems, .fvar hyp]
        let v ← mkAppOptM ``Fintype.complete #[type, inst, Expr.fvar hyp]
        let (fvar, g) ← (← g.assert `this t v).intro1P
        finCasesAt g fvar)
Похожие утверждения