cancelDenoms — Mathlib

Lean4
/-- `cancel_denoms` attempts to remove numerals from the denominators of fractions.
It works on propositions that are field-valued inequalities.

```lean
variable [LinearOrderedField α] (a b c : α)

example (h : a / 5 + b / 4 < c) : 4*a + 5*b < 20*c := by
  cancel_denoms at h
  exact h

example (h : a > 0) : a / 5 > 0 := by
  cancel_denoms
  exact h
```
-/
@[tactic_parser 1000]
public meta def cancelDenoms : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `cancelDenoms 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "cancel_denoms" false✝)
      (ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
Похожие утверждения