diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean index 9388083..85e322f 100644 --- a/CommAlg/final_poly_type.lean +++ b/CommAlg/final_poly_type.lean @@ -5,7 +5,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic set_option maxHeartbeats 0 macro "ls" : tactic => `(tactic|library_search) --- New tactic "obviously" +-- From Kyle : New tactic "obviously" macro "obviously" : tactic => `(tactic| ( first