diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean
index 83ff48a926..50c3c87521 100644
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -29,13 +29,16 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
    exact Nat.add_lt_of_lt_sub this
   s.as[s.start + i.val, this]
 
-@[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
-  if h : i < s.size then s[i, h] else v₀
+abbrev getOp (self : Subarray α) (idx : Fin self.size) : α :=
+  self.get idx
 
-def get! [Inhabited α] (s : Subarray α) (i : Nat) : α :=
+@[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
+  if h : i < s.size then s.get ⟨i, h⟩ else v₀
+
+abbrev get! [Inhabited α] (s : Subarray α) (i : Nat) : α :=
   getD s i default
 
-def getOp [Inhabited α] (self : Subarray α) (idx : Nat) : α :=
+abbrev getOp! [Inhabited α] (self : Subarray α) (idx : Nat) : α :=
   self.get! idx
 
 def popFront (s : Subarray α) : Subarray α :=
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index adb66fa3ec..fb4ed8dfde 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -633,7 +633,7 @@ private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
       let altNonEqNumParams := altNumParams - numDiscrEqs
       let thmName := baseName ++ ((`eq).appendIndexAfter idx)
       eqnNames := eqnNames.push thmName
-      let (notAlt, splitterAltType, splitterAltNumParam, argMask) ← forallAltTelescope (← inferType alts[i]) altNonEqNumParams fun ys eqs rhsArgs argMask altResultType => do
+      let (notAlt, splitterAltType, splitterAltNumParam, argMask) ← forallAltTelescope (← inferType alts[i]!) altNonEqNumParams fun ys eqs rhsArgs argMask altResultType => do
         let patterns := altResultType.getAppArgs
         let mut hs := #[]
         for notAlt in notAlts do