Get rid of annoying ring warning

PatrickMassot · Feb 26, 2025 · c309d09 · c309d09
1 parent 6c6a4f3
commit c309d09
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/GlimpseOfLean/Library/Short.lean b/GlimpseOfLean/Library/Short.lean
@@ -2,6 +2,10 @@ import Mathlib.Tactic
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Complex.Trigonometric
 
+@[inherit_doc Mathlib.Tactic.RingNF.ring]
+macro "ring" : tactic =>
+  `(tactic| first | ring1 | ring_nf)
+
 lemma ge_max_iff {α : Type*} [LinearOrder α] {p q r : α} : r ≥ max p q  ↔ r ≥ p ∧ r ≥ q :=
   max_le_iff