mkNeOfNeOfEq

Mathlib.Tactic.CC.MkProof

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.CC.CCM.mkNeOfNeOfEq

Lean4

/-- Given `aNeB₁ : a ≠ b₁`, `b₁` and `b`, return a proof of `a ≠ b` if `b` and `b₁` are in the
same equivalence class. -/
def mkNeOfNeOfEq (aNeB₁ b₁ b : Expr) : CCM (Option Expr) := do
  guard (← isEqv b b₁)
  if b == b₁ then
    return some aNeB₁
  let b₁EqB ← getEqProof b b₁
  match b₁EqB with
  | none =>
    return none
  | some b₁EqB =>
    mkAppM ``ne_of_ne_of_eq #[aNeB₁, b₁EqB]

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

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

Разделы

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

Аффилиация

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