From 1a28ab04c34939729fca9aecd67e32bf0c0aa9b8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Mon, 9 Sep 2024 01:17:52 -0400
Subject: [PATCH] feat: size lemma for `Array.set!` (#807)

---
 Batteries/Data/Array/Lemmas.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index c943533670..02293aa349 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -131,6 +131,11 @@ theorem size_shrink (a : Array α) (n) : (a.shrink n).size = min a.size n := by
   simp [shrink, size_shrink_loop]
   omega
 
+/-! ### set -/
+
+theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size := by
+  rw [set!_is_setD, size_setD]
+
 /-! ### map -/
 
 theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by