reassocExprIso — Mathlib

Lean4
/-- Given an equation `f = g` between isomorphisms `X ≅ Y` in a category,
produce the equation `∀ {Z} (h : Y ≅ Z), f ≪≫ h = g ≪≫ h`,
but with compositions fully right associated, identities removed, and functors applied.
-/
def reassocExprIso (e : Expr) : MetaM (Expr × Array MVarId) := do
  let lem₀ ← mkConstWithFreshMVarLevels ``Iso.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 categoryIsoSimp (mkAppN lem₀ args), #[inst.mvarId!]))
Похожие утверждения