Lean4
/-- Split the goal `α ≫ η ≫ ηs = α' ≫ η' ≫ ηs'` into `α = α'`, `η = η'`, and `ηs = ηs'`. -/
def ofNormalizedEq (mvarId : MVarId) : MetaM (List MVarId) := do
mvarId.withContext
(do
let e ← instantiateMVars <| ← mvarId.getType
let some (_, e₁, e₂) := (← whnfR e).eq? |
throwError"requires an equality goal"
match (← whnfR e₁).getAppFnArgs, (← whnfR e₂).getAppFnArgs with
| (``CategoryStruct.comp, #[_, _, _, _, _, α, η]), (``CategoryStruct.comp, #[_, _, _, _, _, α', η']) =>
match (← whnfR η).getAppFnArgs, (← whnfR η').getAppFnArgs with
| (``CategoryStruct.comp, #[_, _, _, _, _, η, ηs]), (``CategoryStruct.comp, #[_, _, _, _, _, η', ηs']) =>
let e_α ← mkFreshExprMVar (← Meta.mkEq α α')
let e_η ← mkFreshExprMVar (← Meta.mkEq η η')
let e_ηs ← mkFreshExprMVar (← Meta.mkEq ηs ηs')
let x ← mvarId.apply (← mkAppM ``mk_eq_of_cons #[α, α', η, η', ηs, ηs', e_α, e_η, e_ηs])
return x
| _, _ =>
throwError "failed to make a normalized equality for {e}"
| _, _ =>
throwError "failed to make a normalized equality for {e}")
