From cb4e0ead26d54fd6e615dbc1a576fbd8bf7dcbef Mon Sep 17 00:00:00 2001 From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com> Date: Fri, 16 Jun 2023 13:16:46 -0700 Subject: [PATCH] trivial change --- CommAlg/final_poly_type.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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