reassocExprHom — Mathlib

Lean4
/-- Given an equation `f = g` between morphisms `X ⟶ Y` in a category,
produce the equation `∀ {Z} (h : Y ⟶ Z), f ≫ h = g ≫ h`,
but with compositions fully right associated and identities removed.
Also returns the category `C` and any instance metavariables that need to be solved for.
-/
def reassocExprHom (e : Expr) : MetaM (Expr × Array MVarId) := do
  let lem₀ ← mkConstWithFreshMVarLevels ``eq_whisker'
  let (args, _, _) ← forallMetaBoundedTelescope (← inferType lem₀) 7
  let inst := args[1]!
  inst.mvarId!.setKind .synthetic
  let w := args[6]!
  w.mvarId!.assignIfDefEq e
  withEnsuringLocalInstance inst.mvarId!
      (do
        return (← simpType categorySimp (mkAppN lem₀ args), #[inst.mvarId!]))
Похожие утверждения