feat: let get_elem_tactic_trivial handle [a]'h.2 (#3132)

The pattern
```
    for h : i in [:xs.size] do
      let x := xs[i]'h.2
```
is occassionally useful to iterate over an array with the index in
hand. This PR extends the `get_elem_tactic_trivial` so that one can
simply write
```
    for h : i in [:xs.size] do
      let x := xs[i]
```

fixes #3032.

src/Init/Data/Range.lean

@@ -76,10 +76,12 @@ macro_rules
 end Range
 end Std
 
-theorem Membership.mem.upper {i : Nat} {r : Std.Range} (h : i ∈ r) : i < r.stop := by
-  simp [Membership.mem] at h
-  exact h.2
+theorem Membership.mem.upper {i : Nat} {r : Std.Range} (h : i ∈ r) : i < r.stop := h.2
 
-theorem Membership.mem.lower {i : Nat} {r : Std.Range} (h : i ∈ r) : r.start ≤ i := by
-  simp [Membership.mem] at h
-  exact h.1
+theorem Membership.mem.lower {i : Nat} {r : Std.Range} (h : i ∈ r) : r.start ≤ i := h.1
+
+theorem Membership.get_elem_helper {i n : Nat} {r : Std.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) :
+    i < n := h₂ ▸ h₁.2
+
+macro_rules
+  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply Membership.get_elem_helper; assumption; rfl)

src/Lean/Data/Array.lean

@@ -28,8 +28,8 @@ def filterPairsM {m} [Monad m] {α} (a : Array α) (f : α → α → m (Bool ×
   let mut numRemoved := 0
   for h1 : i in [:a.size] do for h2 : j in [i+1:a.size] do
     unless removed[i]! || removed[j]! do
-      let xi := a[i]'h1.2
-      let xj := a[j]'h2.2
+      let xi := a[i]
+      let xj := a[j]
       let (keepi, keepj) ← f xi xj
       unless keepi do
         numRemoved := numRemoved + 1
@@ -40,7 +40,7 @@ def filterPairsM {m} [Monad m] {α} (a : Array α) (f : α → α → m (Bool ×
   let mut a' := Array.mkEmpty numRemoved
   for h : i in [:a.size] do
     unless removed[i]! do
-      a' := a'.push (a[i]'h.2)
+      a' := a'.push a[i]
   return a'
 
 end Array

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -89,7 +89,7 @@ def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array
     let xs := xs.extract fixedPrefixSize xs.size
     let mut ns : Array Name := #[]
     for h : i in [:xs.size] do
-      let n ← (xs[i]'h.2).fvarId!.getUserName
+      let n ← xs[i].fvarId!.getUserName
       let n := if n.hasMacroScopes then .mkSimple s!"x{i+1}" else n
       ns := ns.push (← freshen ns n)
     return ns
@@ -505,7 +505,7 @@ partial def solve {m} {α} [Monad m] (measures : Array α)
 
     -- Find the first measure that has at least one < and otherwise only = or <=
     for h : measureIdx in [:measures.size] do
-      let measure := measures[measureIdx]'h.2
+      let measure := measures[measureIdx]
       let mut has_lt := false
       let mut all_le := true
       let mut todo := #[]
@@ -542,10 +542,10 @@ def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name))
     (measures : Array MutualMeasure) : MetaM TerminationWF := do
   let mut termByElements := #[]
   for h : funIdx in [:varNamess.size] do
-    let vars := (varNamess[funIdx]'h.2).map mkIdent
+    let vars := varNamess[funIdx].map mkIdent
     let body ← mkTupleSyntax (← measures.mapM fun
       | .args varIdxs => do
-          let v := vars.get! (varIdxs[funIdx]!)
+          let v := vars.get! varIdxs[funIdx]!
           let sizeOfIdent := mkIdent (← unresolveNameGlobal ``sizeOf)
           `($sizeOfIdent $v)
       | .func funIdx' => if funIdx' == funIdx then `(1) else `(0)
@@ -567,14 +567,14 @@ Single space as column separator.
 -/
 def formatTable : Array (Array String) → String := fun xss => Id.run do
   let mut colWidths := xss[0]!.map (fun _ => 0)
-  for i in [:xss.size] do
-    for j in [:xss[i]!.size] do
-      if xss[i]![j]!.length > colWidths[j]! then
-        colWidths := colWidths.set! j xss[i]![j]!.length
+  for hi : i in [:xss.size] do
+    for hj : j in [:xss[i].size] do
+      if xss[i][j].length > colWidths[j]! then
+        colWidths := colWidths.set! j xss[i][j].length
   let mut str := ""
-  for i in [:xss.size] do
-    for j in [:xss[i]!.size] do
-      let s := xss[i]![j]!
+  for hi : i in [:xss.size] do
+    for hj : j in [:xss[i].size] do
+      let s := xss[i][j]
       if j > 0 then -- right-align
         for _ in [:colWidths[j]! - s.length] do
           str := str ++ " "
@@ -582,7 +582,7 @@ def formatTable : Array (Array String) → String := fun xss => Id.run do
       if j = 0 then -- left-align
         for _ in [:colWidths[j]! - s.length] do
           str := str ++ " "
-      if j + 1 < xss[i]!.size then
+      if j + 1 < xss[i].size then
         str := str ++ " "
     if i + 1 < xss.size then
       str := str ++ "\n"

src/Lean/Elab/PreDefinition/WF/Rel.lean

@@ -35,7 +35,7 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva
     if element.vars.size > varNames.size then
       throwErrorAt element.vars[varNames.size]! "too many variable names"
     for h : i in [:element.vars.size] do
-      let varStx := element.vars[i]'h.2
+      let varStx := element.vars[i]
       if let `($ident:ident) := varStx then
         varNames := varNames.set! (varNames.size - element.vars.size + i) ident.getId
     return varNames

tests/lean/getElem.lean

@@ -29,3 +29,16 @@ def f7 (i : Nat) :=
 #print f5
 #print f6
 #print f7
+
+def withRange (xs : Array Nat) : Option Nat := Id.run do
+  for h : i in [:xs.size] do
+    if i == xs[i] then
+      return i
+  return none
+
+def withTwoRanges (xs : Array Nat) : Option Nat := Id.run do
+  for h1 : i in [:xs.size] do
+    for h2 : j in [i + 1:xs.size] do
+      if xs[i] == xs[j] then
+        return i
+  return none