diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index 831c7843b7..dd5edc9500 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -96,7 +96,8 @@ where
             if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then
                let some i  := ys.getIdx? lhs | unreachable!
                let ys      := ys.eraseIdx i
-               let mask    := mask.set! i false
+               let some j  := args.getIdx? lhs | unreachable!
+               let mask    := mask.set! j false
                let args    := args.map fun arg => if arg == lhs then rhs else arg
                let args    := args.push (← mkEqRefl rhs)
                let typeNew := typeNew.replaceFVar lhs rhs
diff --git a/tests/lean/run/eqThmWithMoreThanOneAsPattern.lean b/tests/lean/run/eqThmWithMoreThanOneAsPattern.lean
new file mode 100644
index 0000000000..d3103c9722
--- /dev/null
+++ b/tests/lean/run/eqThmWithMoreThanOneAsPattern.lean
@@ -0,0 +1,3 @@
+@[simp] def foo: Nat → Nat → Nat
+| p1@(t₁ + 1), p2@(t₂ + 1) => foo t₁ t₂
+| _, _ => 0