congrImplies?'

Mathlib.Tactic.CongrExclamation

URI: https://scilib.ai/kg/mathlib#Lean.MVarId.congrImplies?'

Lean4

/-- A version of `Lean.MVarId.congrImplies?` that uses `implies_congr'`
instead of `implies_congr`. -/
def congrImplies?' (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
  observing?
    (do
      let [mvarId₁, mvarId₂] ← mvarId.apply (← mkConstWithFreshMVarLevels ``implies_congr') |
        throwError"unexpected number of goals"
      return [mvarId₁, mvarId₂])

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

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

Разделы

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

Аффилиация

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