[Usa2019P1] simplification found by 'tryTacticAtEachStep exact?'

dwrensha · dwrensha · commit 22eaf558bd43 · 2024-02-29T08:08:15.000-05:00
diff --git a/Compfiles/Usa2019P1.lean b/Compfiles/Usa2019P1.lean
@@ -70,10 +70,7 @@ lemma lemma_1
     (fab1 : f^[r] b = a)
     (fab2 : f a = a) :
     b = a := by
-  have h1 : ∀ s, f^[s] a = a := fun s ↦ by
-    induction' s with s ih
-    · dsimp
-    · aesop
+  have h1 : ∀ s, f^[s] a = a := fun s ↦ Function.iterate_fixed fab2 s
 
   have h2 := calc f^[r] b
       = a := fab1
