refactor: IndPredBelow: use apply_assumption (#4841)

when transforming the `match` statements in `IndPredBelow`, given a
local variable `x : T`, we need to search for `hx : T.below x`.
Previously this was done using the custom `backwardsChaining` method,
although my hypothesis is that we don’t need to chain anything here, and
can use `apply_assumption`.

src/Lean/Meta/IndPredBelow.lean

@@ -6,6 +6,7 @@ Authors: Dany Fabian
 prelude
 import Lean.Meta.Constructions.CasesOn
 import Lean.Meta.Match.Match
+import Lean.Meta.Tactic.SolveByElim
 
 namespace Lean.Meta.IndPredBelow
 open Match
@@ -569,7 +570,7 @@ def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat
       let below ← mkFreshExprSyntheticOpaqueMVar belowTy
       try
         trace[Meta.IndPredBelow.match] "{←Meta.ppGoal below.mvarId!}"
-        if (← backwardsChaining below.mvarId! 10) then
+        if (← below.mvarId!.applyRules { backtracking := false, maxDepth := 1 } []).isEmpty then
           trace[Meta.IndPredBelow.match] "Found below term in the local context: {below}"
           if (← xs.anyM (isDefEq below)) then pure none else pure (below, idx.val)
         else