existsAndEq

Mathlib.Tactic.Simproc.ExistsAndEq

URI: https://scilib.ai/kg/mathlib#existsAndEq

Lean4

/-- Triggers on goals of the form `∃ a, body` and checks whether `body` has the
form `... ∧ a = a' ∧ ...` or `... ∧ a' = a ∧ ...` for some `a'` that is independent of `a`.
If so, it replaces all occurrences of `a` with `a'` and removes the quantifier. -/
def existsAndEq : Lean.Meta.Simp.Simproc := fun e => do
  match e.getAppFnArgs with
  | (``Exists, #[_, p]) =>
    let some ⟨res, pf⟩ ← existsAndEq.findImpEqProof p |
      return .continue
    return .visit { expr := mkApp p res, proof? := pf }
  | _ =>
    return .continue

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

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

Разделы

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

Аффилиация

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