From 489f8acd77068520da9344739f976061e947b323 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 17 Dec 2025 14:44:17 +0100
Subject: [PATCH] feat: get-elem tactic support for subarrays (#11710)

This PR extends the get-elem tactic for ranges so that it supports
subarrays. Example:
```lean
example {a : Array Nat} (h : a.size = 28) : Id Unit := do
  let mut x := 0
  for h : i in *...(3 : Nat) do
    x := a[1...4][i]
```
---
 src/Init/Data/Range/Polymorphic/GetElemTactic.lean | 8 +++++++-
 tests/lean/run/rangePolymorphic.lean               | 5 +++++
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/Range/Polymorphic/GetElemTactic.lean b/src/Init/Data/Range/Polymorphic/GetElemTactic.lean
index b2a4c9cfe0..211001498d 100644
--- a/src/Init/Data/Range/Polymorphic/GetElemTactic.lean
+++ b/src/Init/Data/Range/Polymorphic/GetElemTactic.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Vector.Basic
+public import Init.Data.Slice.Array.Lemmas
 
 public section
 
@@ -32,10 +33,15 @@ macro_rules
           try rw [Std.Ric.mem_iff] at *
           try rw [Std.Rio.mem_iff] at *
           try rw [Std.Rii.mem_iff] at *
-          dsimp +zetaDelta only [
+          try dsimp +zetaDelta only [
             -- `Vector.size` needs to be unfolded because for `xs : Vector α n`, one needs to prove
             -- `i < n` instead of `i < xs.size`. Although `Vector.size` is reducible, this is
             -- not enough for `omega`.
             Vector.size] at *
+          -- If we're accessing elements of a subarray, we need to calculate its size.
+          try simp only [
+            Array.size_mkSlice_rco, Array.size_mkSlice_rcc, Array.size_mkSlice_rci,
+            Array.size_mkSlice_roo, Array.size_mkSlice_roc, Array.size_mkSlice_roi,
+            Array.size_mkSlice_rio, Array.size_mkSlice_ric, Array.size_mkSlice_rii]
           omega
         | done)
diff --git a/tests/lean/run/rangePolymorphic.lean b/tests/lean/run/rangePolymorphic.lean
index 648da4130d..79477ce336 100644
--- a/tests/lean/run/rangePolymorphic.lean
+++ b/tests/lean/run/rangePolymorphic.lean
@@ -80,6 +80,11 @@ example (xs : Array Nat) : Id Unit := do
     for _h' : i' in *...<i do
       x := x + xs[i']
 
+example {a : Array Nat} (h : a.size = 28) : Id Unit := do
+  let mut x := 0
+  for h : i in *...(3 : Nat) do
+    x := a[1...4][i]
+
 /--
 info: i=0, j=2
 i=1, j=3