defeq

Mathlib.Tactic.TermCongr

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.TermCongr.CongrResult.defeq

Lean4

/-- Force the lhs and rhs to be defeq. For when `dsimp`-like congruence is necessary.
Clears the proof. -/
def defeq (res : CongrResult) : MetaM CongrResult := do
  if res.isRfl then
    return res
  else
    unless ← isDefEq res.lhs res.rhs do
      throwError "Cannot generate congruence because we need{(indentD res.lhs)}\n\
                  to be definitionally equal to{indentD res.rhs}"
    discard <| res.eq
    return { res with pf? := none }

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru