diff --git a/Compfiles/Imo1978P1.lean b/Compfiles/Imo1978P1.lean index d0eef4c..ab6e5d7 100644 --- a/Compfiles/Imo1978P1.lean +++ b/Compfiles/Imo1978P1.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2024 The Compfiles Contributors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: InternLM-MATH LEAN Formalizer v0.1 +Authors: InternLM-MATH LEAN Formalizer v0.1, David Renshaw -/ import Mathlib.Tactic