whitespace

leanprover · Nov 20, 2024 · a428942 · a428942
1 parent 8f5d054
commit a428942
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
@@ -798,7 +798,7 @@ decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h
   induction a, i, h using Array.eraseIdx.induct with
   | @case1 a i h h' a' ih =>
     unfold eraseIdx
-    simp +zetaDelta[h', a', ih]
+    simp +zetaDelta [h', a', ih]
   | case2 a i h h' =>
     unfold eraseIdx
     simp [h']