diff --git a/tests/lean/run/simp_int_arith.lean b/tests/lean/run/simp_int_arith.lean index 88195b727d..0bf7b72749 100644 --- a/tests/lean/run/simp_int_arith.lean +++ b/tests/lean/run/simp_int_arith.lean @@ -319,8 +319,8 @@ fun a b => (Expr.mulL 3 ((Expr.var 1).add (Expr.mulL 2 (Expr.var 0))))).sub (Expr.num 11)) 2 (Poly.add 1 1 (Poly.add 2 0 (Poly.num 0))) 3 (Eq.refl true))) - Init.Data.Int.DivMod.Lemmas._auxLemma.2)) - Init.Data.Int.DivMod.Lemmas._auxLemma.2) + _proof_2✝)) + _proof_2✝) (iff_self (2 ∣ a))) -/ #guard_msgs (info) in