From dadfebc218f792393d6c7a5a82799bea167124ed Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 21 Nov 2024 08:57:24 +1100 Subject: [PATCH] eraseIdxIfInBounds --- Mathlib/Tactic/Linarith/Frontend.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Tactic/Linarith/Frontend.lean b/Mathlib/Tactic/Linarith/Frontend.lean index 552a10b4b0159..a63112c459aff 100644 --- a/Mathlib/Tactic/Linarith/Frontend.lean +++ b/Mathlib/Tactic/Linarith/Frontend.lean @@ -277,7 +277,7 @@ def runLinarith (cfg : LinarithConfig) (prefType : Option Expr) (g : MVarId) if let some t := prefType then let (i, vs) ← hyp_set.find t proveFalseByLinarith cfg.transparency cfg.oracle cfg.discharger g vs <|> - findLinarithContradiction cfg g ((hyp_set.eraseIdx! i).toList.map (·.2)) + findLinarithContradiction cfg g ((hyp_set.eraseIdxIfInBounds i).toList.map (·.2)) else findLinarithContradiction cfg g (hyp_set.toList.map (·.2)) let mut preprocessors := cfg.preprocessors if cfg.splitNe then