trans

Mathlib.Tactic.TermCongr

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

Lean4

/-- Combine two congruence proofs using transitivity.
Does not check that `res1.rhs` is defeq to `res2.lhs`.
If both `res1` and `res2` are trivial then the result is trivial. -/
def trans (res1 res2 : CongrResult) : CongrResult
    where
  lhs := res1.lhs
  rhs := res2.rhs
  pf? :=
    if res1.isRfl then res2.pf?
    else
      if res2.isRfl then res1.pf?
      else
        some fun
          | .eq => do
            mkEqTrans (← res1.eq) (← res2.eq)
          | .heq => do
            mkHEqTrans (← res1.heq) (← res2.heq)

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

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

Разделы

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

Аффилиация

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