From d883f18709a4f286ec084905c6c2a82ad094b6aa Mon Sep 17 00:00:00 2001
From: s1m7u <z5476255@ad.unsw.edu.au>
Date: Mon, 29 Jan 2024 16:54:51 +0000
Subject: [PATCH] chore(Data/List/Rotate): add `@[simp]` to `rotate_replicate`
 (#10106)

---
 Mathlib/Data/List/Rotate.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/List/Rotate.lean b/Mathlib/Data/List/Rotate.lean
index 88c80f3799d79..2a5f5d5271b26 100644
--- a/Mathlib/Data/List/Rotate.lean
+++ b/Mathlib/Data/List/Rotate.lean
@@ -130,7 +130,7 @@ theorem length_rotate (l : List α) (n : ℕ) : (l.rotate n).length = l.length :
   rw [rotate_eq_rotate', length_rotate']
 #align list.length_rotate List.length_rotate
 
--- porting note: todo: add `@[simp]`
+@[simp]
 theorem rotate_replicate (a : α) (n : ℕ) (k : ℕ) : (replicate n a).rotate k = replicate n a :=
   eq_replicate.2 ⟨by rw [length_rotate, length_replicate], fun b hb =>
     eq_of_mem_replicate <| mem_rotate.1 hb⟩