fix: equation theorem for match with more than one "as" pattern

see #1195
see #1179

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

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