transfer

Mathlib.Data.Num.Lemmas

URI: https://scilib.ai/kg/mathlib#PosNum.transfer

Lean4

/-- This tactic tries to prove (in)equalities about `PosNum`s by transferring them to the `Nat` world
and then trying to call `simp`.
```lean
example (n : PosNum) (m : PosNum) : n ≤ n + m := by transfer
```
-/
@[scoped tactic_parser 1000]
public meta def transfer : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `PosNum.transfer 1024 (ParserDescr.nonReservedSymbol✝ "transfer" false✝)

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

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

Разделы

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

Аффилиация

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