transfer_rw

Mathlib.Data.Num.Lemmas

URI: https://scilib.ai/kg/mathlib#Num.transfer_rw

Lean4

/-- This tactic tries to turn an (in)equality about `Num`s to one about `Nat`s by rewriting.
```lean
example (n : Num) (m : Num) : n ≤ n + m := by
  transfer_rw
  exact Nat.le_add_right _ _
```
-/
@[scoped tactic_parser 1000]
public meta def transfer_rw : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Num.transfer_rw 1024 (ParserDescr.nonReservedSymbol✝ "transfer_rw" false✝)

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

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

Разделы

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

Аффилиация

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