feat: ring_exp tactic, subtraction in ring (#519)

Another complete rewrite. This implements one `ring` to rule them all: it incorporates both `ring_exp` and `ring` behaviors, now under the name `ring`. (`ring_exp` had some small (1.4x) performance issues that prevented it from being used by default; I'm hoping that those issues are fixed now, and we can revisit later if it becomes an issue.)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: digama0

Mathlib/Algebra/GroupPower/Basic.lean

@@ -27,6 +27,9 @@ theorem add_nsmul (a : M) (m n : ℕ) : (m + n) • a = m • a + n • a := by
   | zero => rw [Nat.zero_add, zero_nsmul, zero_add]
   | succ m ih => rw [Nat.succ_add, Nat.succ_eq_add_one, succ_nsmul, ih, succ_nsmul, add_assoc]
 
+theorem succ_nsmul' (a : M) (n : ℕ) : (n + 1) • a = n • a + a := by
+  rw [add_nsmul, one_nsmul]
+
 end AddMonoid
 
 section Monoid
@@ -57,6 +60,8 @@ theorem Commute.mul_pow {a b : M} (h : Commute a b) (n : ℕ) : (a * b) ^ n = a
   · rw [pow_zero, pow_zero, pow_zero, one_mul]
   · simp only [pow_succ, ih, ← mul_assoc, (h.pow_left n).right_comm]
 
+attribute [to_additive succ_nsmul'] pow_succ'
+
 end Monoid
 
 /-!

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
 import Mathlib.Data.Int.Cast
+import Mathlib.Algebra.GroupPower.Basic
 
 /-!
 # Lemmas about power operations on monoids and groups
@@ -18,3 +19,11 @@ theorem Int.cast_pow [Ring R] (n : ℤ) : ∀ m : ℕ, (↑(n ^ m) : R) = (n : R
   | n+1 => by rw [pow_succ, pow_succ, Int.cast_mul, Int.cast_pow _ n]
 
 @[simp] theorem pow_eq {m : ℤ} {n : ℕ} : m.pow n = m ^ n := rfl
+
+theorem nsmul_eq_mul' [Semiring R] (a : R) (n : ℕ) : n • a = a * n := by
+  induction' n with n ih
+  · rw [zero_nsmul, Nat.cast_zero, mul_zero]
+  · rw [succ_nsmul', ih, Nat.cast_succ, mul_add, mul_one]
+
+@[simp] theorem nsmul_eq_mul [Semiring R] (n : ℕ) (a : R) : n • a = n * a := by
+  rw [nsmul_eq_mul', (n.cast_commute a).eq]

Mathlib/Algebra/Ring/Basic.lean

@@ -34,6 +34,21 @@ class Semiring (R : Type u) extends NonUnitalSemiring R, NonAssocSemiring R, Mon
 
 section Semiring
 
+-- TODO: put these in the right place
+@[simp] theorem Commute.zero_right [Semiring R] (a : R) : Commute a 0 :=
+  (mul_zero _).trans (zero_mul _).symm
+
+@[simp] theorem Commute.zero_left [Semiring R] (a : R) : Commute 0 a :=
+  (zero_mul _).trans (mul_zero _).symm
+
+@[simp] theorem Commute.add_right [Semiring R] {a b c : R} (h : Commute a b) (h' : Commute a c) :
+    Commute a (b + c) := by
+  simp only [Commute, SemiconjBy, left_distrib, right_distrib, h.eq, h'.eq]
+
+@[simp] theorem Commute.add_left [Semiring R] {a b c : R} (h : Commute a c) (h' : Commute b c) :
+    Commute (a + b) c := by
+  simp only [Commute, SemiconjBy, left_distrib, right_distrib, h.eq, h'.eq]
+
 @[simp]
 lemma Nat.cast_mul [Semiring R] {m n : ℕ} : (m * n).cast = (m.cast * n.cast : R) := by
   induction n generalizing m <;> simp_all [mul_succ, mul_add]
@@ -42,6 +57,11 @@ lemma Nat.cast_mul [Semiring R] {m n : ℕ} : (m * n).cast = (m.cast * n.cast :
 lemma Nat.cast_pow [Semiring R] {m n : ℕ} : (m ^ n).cast = (m.cast ^ n : R) := by
   induction n generalizing m <;> simp_all [Nat.pow_succ', _root_.pow_succ'', pow_zero]
 
+theorem Nat.cast_commute [Semiring α] (n : ℕ) (x : α) : Commute (↑n) x := by
+  induction n with
+  | zero => rw [Nat.cast_zero]; exact Commute.zero_left x
+  | succ n ihn => rw [Nat.cast_succ] <;> exact ihn.add_left (Commute.one_left x)
+
 end Semiring
 
 class CommSemiring (R : Type u) extends Semiring R, CommMonoid R where
@@ -52,10 +72,13 @@ class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R
 
 example [Ring R] : HasInvolutiveNeg R := inferInstance
 
-theorem neg_mul_eq_neg_mul {R} [Ring R] (a b : R) : -(a * b) = (-a) * b :=
-  Eq.symm <| eq_of_sub_eq_zero' <| by
-    rw [sub_eq_add_neg, neg_neg (a * b) /- TODO: why is arg necessary? -/]
-    rw [← add_mul, neg_add_self a /- TODO: why is arg necessary? -/, zero_mul]
+@[simp] theorem neg_mul {R} [Ring R] (a b : R) : (-a) * b = -(a * b) :=
+  eq_of_sub_eq_zero' <| by rw [sub_eq_add_neg, neg_neg, ← add_mul, neg_add_self, zero_mul]
+
+@[simp] lemma mul_neg [Ring R] (a b : R) : a * -b = - (a * b) :=
+  eq_of_sub_eq_zero' <| by rw [sub_eq_add_neg, neg_neg, ← mul_add, neg_add_self, mul_zero]
+
+theorem neg_mul_eq_neg_mul {R} [Ring R] (a b : R) : -(a * b) = (-a) * b := (neg_mul ..).symm
 
 theorem mul_sub_right_distrib [Ring R] (a b c : R) : (a - b) * c = a * c - b * c := by
   simpa only [sub_eq_add_neg, neg_mul_eq_neg_mul] using add_mul a (-b) c

Mathlib/Mathport/Syntax.lean

@@ -332,18 +332,9 @@ syntax termList := " [" term,* "]"
 /- B -/ syntax (name := abel) "abel" (ppSpace (&"raw" <|> &"term"))? (ppSpace location)? : tactic
 /- B -/ syntax (name := abel!) "abel!" (ppSpace (&"raw" <|> &"term"))? (ppSpace location)? : tactic
 
-/- E -/ syntax (name := ring1) "ring1" : tactic
-/- E -/ syntax (name := ring1!) "ring1!" : tactic
-
 syntax ringMode := &"SOP" <|> &"raw" <|> &"horner"
 /- E -/ syntax (name := ringNF) "ring_nf" (ppSpace ringMode)? (ppSpace location)? : tactic
 /- E -/ syntax (name := ringNF!) "ring_nf!" (ppSpace ringMode)? (ppSpace location)? : tactic
-/- E -/ syntax (name := ring!) "ring!" : tactic
-
-/- B -/ syntax (name := ringExpEq) "ring_exp_eq" : tactic
-/- B -/ syntax (name := ringExpEq!) "ring_exp_eq!" : tactic
-/- B -/ syntax (name := ringExp) "ring_exp" (ppSpace location)? : tactic
-/- B -/ syntax (name := ringExp!) "ring_exp!" (ppSpace location)? : tactic
 
 /- E -/ syntax (name := noncommRing) "noncomm_ring" : tactic
 

Mathlib/Tactic/NormNum/Basic.lean

@@ -109,28 +109,41 @@ theorem isInt_add {α} [Ring α] : {a b : α} → {a' b' c : ℤ} →
     IsInt a a' → IsInt b b' → Int.add a' b' = c → IsInt (a + b) c
   | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨(Int.cast_add ..).symm⟩
 
+instance : MonadLift Option MetaM where
+  monadLift
+  | none => failure
+  | some e => pure e
+
 /-- The `norm_num` extension which identifies expressions of the form `a + b`,
 such that `norm_num` successfully recognises both `a` and `b`. -/
 @[norm_num _ + _, Add.add _ _] def evalAdd : NormNumExt where eval {u α} e := do
   let .app (.app f (a : Q($α))) (b : Q($α)) ← withReducible (whnf e) | failure
   let ra ← derive a; let rb ← derive b
-  let intArm (rα : Q(Ring $α)) := do
-    let ⟨za, na, pa⟩ ← ra.toInt; let ⟨zb, nb, pb⟩ ← rb.toInt
-    let zc := za + zb
-    have c := mkRawIntLit zc
-    let r : Q(Int.add $na $nb = $c) := (q(Eq.refl $c) : Expr)
-    return (.isInt rα zc q(isInt_add $pa $pb $r) : Result q($a + $b))
   match ra, rb with
-  | .isNat _ na pa, .isNat sα nb pb =>
-    have pa : Q(IsNat $a $na) := pa
+  | .isNat _ .., .isNat _ .. | .isNat _ .., .isNegNat _ ..
+  | .isNegNat _ .., .isNat _ .. | .isNegNat _ .., .isNegNat _ .. =>
     guard <|← withNewMCtxDepth <| isDefEq f q(HAdd.hAdd (α := $α))
-    have c : Q(ℕ) := mkRawNatLit (na.natLit! + nb.natLit!)
-    let r : Q(Nat.add $na $nb = $c) := (q(Eq.refl $c) : Expr)
-    return (.isNat sα c q(isNat_add $pa $pb $r) : Result q($a + $b))
-  | .isNat _ .., .isNegNat rα ..
-  | .isNegNat rα .., .isNat _ ..
-  | .isNegNat _ .., .isNegNat rα .. => intArm rα
   | _, _ => failure
+  let rec
+  /-- Main part of `evalAdd`. -/
+  core : Option (Result e) := do
+    let intArm (rα : Q(Ring $α)) := do
+      let ⟨za, na, pa⟩ ← ra.toInt; let ⟨zb, nb, pb⟩ ← rb.toInt
+      let zc := za + zb
+      have c := mkRawIntLit zc
+      let r : Q(Int.add $na $nb = $c) := (q(Eq.refl $c) : Expr)
+      return (.isInt rα zc q(isInt_add $pa $pb $r) : Result q($a + $b))
+    match ra, rb with
+    | .isNat _ na pa, .isNat sα nb pb =>
+      have pa : Q(IsNat $a $na) := pa
+      have c : Q(ℕ) := mkRawNatLit (na.natLit! + nb.natLit!)
+      let r : Q(Nat.add $na $nb = $c) := (q(Eq.refl $c) : Expr)
+      return (.isNat sα c q(isNat_add $pa $pb $r) : Result q($a + $b))
+    | .isNat _ .., .isNegNat rα ..
+    | .isNegNat rα .., .isNat _ ..
+    | .isNegNat _ .., .isNegNat rα .. => intArm rα
+    | _, _ => failure
+  core
 
 theorem isInt_neg {α} [Ring α] : {a : α} → {a' b : ℤ} →
     IsInt a a' → Int.neg a' = b → IsInt (-a) b
@@ -177,24 +190,31 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
 @[norm_num _ * _, Mul.mul _ _] def evalMul : NormNumExt where eval {u α} e := do
   let .app (.app f (a : Q($α))) (b : Q($α)) ← withReducible (whnf e) | failure
   let ra ← derive a; let rb ← derive b
-  let intArm (rα : Q(Ring $α)) := do
-    guard <|← withNewMCtxDepth <| isDefEq f q(HMul.hMul (α := $α))
-    let ⟨za, na, pa⟩ ← ra.toInt; let ⟨zb, nb, pb⟩ ← rb.toInt
-    let zc := za * zb
-    have c := mkRawIntLit zc
-    let r : Q(Int.mul $na $nb = $c) := (q(Eq.refl $c) : Expr)
-    return (.isInt rα zc q(isInt_mul $pa $pb $r) : Result q($a * $b))
   match ra, rb with
-  | .isNat _ na pa, .isNat sα nb pb =>
-    have pa : Q(IsNat $a $na) := pa
+  | .isNat _ .., .isNat _ .. | .isNat _ .., .isNegNat _ ..
+  | .isNegNat _ .., .isNat _ .. | .isNegNat _ .., .isNegNat _ .. =>
     guard <|← withNewMCtxDepth <| isDefEq f q(HMul.hMul (α := $α))
-    have c : Q(ℕ) := mkRawNatLit (na.natLit! * nb.natLit!)
-    let r : Q(Nat.mul $na $nb = $c) := (q(Eq.refl $c) : Expr)
-    return (.isNat sα c q(isNat_mul $pa $pb $r) : Result q($a * $b))
-  | .isNat _ .., .isNegNat rα ..
-  | .isNegNat rα .., .isNat _ ..
-  | .isNegNat _ .., .isNegNat rα .. => intArm rα
   | _, _ => failure
+  let rec
+  /-- Main part of `evalMul`. -/
+  core : Option (Result e) := do
+    let intArm (rα : Q(Ring $α)) := do
+      let ⟨za, na, pa⟩ ← ra.toInt; let ⟨zb, nb, pb⟩ ← rb.toInt
+      let zc := za * zb
+      have c := mkRawIntLit zc
+      let r : Q(Int.mul $na $nb = $c) := (q(Eq.refl $c) : Expr)
+      return (.isInt rα zc q(isInt_mul $pa $pb $r) : Result q($a * $b))
+    match ra, rb with
+    | .isNat _ na pa, .isNat sα nb pb =>
+      have pa : Q(IsNat $a $na) := pa
+      have c : Q(ℕ) := mkRawNatLit (na.natLit! * nb.natLit!)
+      let r : Q(Nat.mul $na $nb = $c) := (q(Eq.refl $c) : Expr)
+      return (.isNat sα c q(isNat_mul $pa $pb $r) : Result q($a * $b))
+    | .isNat _ .., .isNegNat rα ..
+    | .isNegNat rα .., .isNat _ ..
+    | .isNegNat _ .., .isNegNat rα .. => intArm rα
+    | _, _ => failure
+  core
 
 theorem isNat_pow {α} [Semiring α] : {a : α} → {b a' b' c : ℕ} →
     IsNat a a' → IsNat b b' → Nat.pow a' b' = c → IsNat (a ^ b) c
@@ -212,17 +232,23 @@ def evalPow : NormNumExt where eval {u α} e := do
   let ⟨nb, pb⟩ ← deriveNat b q(instSemiringNat)
   let ra ← derive a
   match ra with
-  | .isNat sα na pa =>
+  | .isNat _ .. | .isNegNat _ .. =>
     guard <|← withDefault <| withNewMCtxDepth <| isDefEq f q(HPow.hPow (α := $α))
-    have c : Q(ℕ) := mkRawNatLit (na.natLit! ^ nb.natLit!)
-    let r : Q(Nat.pow $na $nb = $c) := (q(Eq.refl $c) : Expr)
-    let pb : Q(IsNat $b $nb) := pb
-    return (.isNat sα c q(isNat_pow $pa $pb $r) : Result q($a ^ $b))
-  | .isNegNat rα .. =>
-    guard <|← withDefault <| withNewMCtxDepth <| isDefEq f q(HPow.hPow (α := $α))
-    let ⟨za, na, pa⟩ ← ra.toInt
-    let zc := za ^ nb.natLit!
-    let c := mkRawIntLit zc
-    let r : Q(Int.pow $na $nb = $c) := (q(Eq.refl $c) : Expr)
-    return (.isInt rα zc (z := c) q(isInt_pow $pa $pb $r) : Result q($a ^ $b))
   | _ => failure
+  let rec
+  /-- Main part of `evalPow`. -/
+  core : Option (Result e) := do
+    match ra with
+    | .isNat sα na pa =>
+      have c : Q(ℕ) := mkRawNatLit (na.natLit! ^ nb.natLit!)
+      let r : Q(Nat.pow $na $nb = $c) := (q(Eq.refl $c) : Expr)
+      let pb : Q(IsNat $b $nb) := pb
+      return (.isNat sα c q(isNat_pow $pa $pb $r) : Result q($a ^ $b))
+    | .isNegNat rα .. =>
+      let ⟨za, na, pa⟩ ← ra.toInt
+      let zc := za ^ nb.natLit!
+      let c := mkRawIntLit zc
+      let r : Q(Int.pow $na $nb = $c) := (q(Eq.refl $c) : Expr)
+      return (.isInt rα zc (z := c) q(isInt_pow $pa $pb $r) : Result q($a ^ $b))
+    | _ => failure
+  core

Mathlib/Tactic/NormNum/Core.lean

@@ -34,6 +34,13 @@ structure IsNat [Semiring α] (a : α) (n : ℕ) : Prop where
 
 theorem IsNat.raw_refl (n : ℕ) : IsNat n n := ⟨rfl⟩
 
+/--
+A "raw nat cast" is an expression of the form `(Nat.rawCast lit : α)` where `lit` is a raw
+natural number literal. These expressions are used by tactics like `ring` to decrease the number
+of typeclass arguments required in each use of a number literal at type `α`.
+-/
+@[simp] def _root_.Nat.rawCast [Semiring α] (n : ℕ) : α := n
+
 /-- Asserting that the `OfNat α n` instance provides the same value as the coercion. -/
 class LawfulOfNat (α) [Semiring α] (n) [OfNat α n] : Prop where
   /-- Assert `n = (OfNat.ofNat n α)`, with the parametrising instance. -/
@@ -45,21 +52,43 @@ instance (α) [Semiring α] : LawfulOfNat α (nat_lit 1) := ⟨Nat.cast_one⟩
 instance : LawfulOfNat ℕ n := ⟨show n = Nat.cast n by simp⟩
 instance : LawfulOfNat ℤ n := ⟨show Int.ofNat n = Nat.cast n by simp⟩
 
-theorem IsNat.to_eq {α} [Semiring α] (n) [OfNat α n] [LawfulOfNat α n] :
+theorem IsNat.to_eq [Semiring α] (n) [OfNat α n] [LawfulOfNat α n] :
     (a : α) → IsNat a n → a = OfNat.ofNat n
   | _, ⟨rfl⟩ => LawfulOfNat.eq_ofNat
 
+theorem IsNat.to_raw_eq [Semiring α] : IsNat (a : α) n → a = n.rawCast
+  | ⟨e⟩ => e
+
+theorem IsNat.of_raw (α) [Semiring α] (n : ℕ) : IsNat (n.rawCast : α) n := ⟨rfl⟩
+
 /-- Assert that an element of a ring is equal to the coercion of some integer. -/
 structure IsInt [Ring α] (a : α) (n : ℤ) : Prop where
   /-- The element is equal to the coercion of the integer. -/
   out : a = n
 
+/--
+A "raw int cast" is an expression of the form:
+
+* `(Nat.rawCast lit : α)` where `lit` is a raw natural number literal
+* `(Int.rawCast (Int.negOfNat lit) : α)` where `lit` is a nonzero raw natural number literal
+
+(That is, we only actually use this function for negative integers.) This representation is used by
+tactics like `ring` to decrease the number of typeclass arguments required in each use of a number
+literal at type `α`.
+-/
+@[simp] def _root_.Int.rawCast [Ring α] (n : ℤ) : α := n
+
 theorem IsInt.to_isNat {α} [Ring α] : ∀ {a : α} {n}, IsInt a (.ofNat n) → IsNat a n
   | _, _, ⟨rfl⟩ => ⟨by simp⟩
 
 theorem IsNat.to_isInt {α} [Ring α] : ∀ {a : α} {n}, IsNat a n → IsInt a (.ofNat n)
   | _, _, ⟨rfl⟩ => ⟨by simp⟩
 
+theorem IsInt.to_raw_eq [Ring α] : IsInt (a : α) n → a = n.rawCast
+  | ⟨e⟩ => e
+
+theorem IsInt.of_raw (α) [Ring α] (n : ℤ) : IsInt (n.rawCast : α) n := ⟨rfl⟩
+
 theorem IsInt.neg_to_eq {α} [Ring α] (n) [OfNat α n] [LawfulOfNat α n] :
     (a : α) → IsInt a (.negOfNat n) → a = -OfNat.ofNat n
   | _, ⟨rfl⟩ => by simp [Int.negOfNat_eq, Int.cast_neg]; apply LawfulOfNat.eq_ofNat
@@ -113,13 +142,16 @@ inductive Result' where
   | isNegNat (inst lit proof : Expr)
   /-- Untyped version of `Result.isRat`. -/
   | isRat (inst : Expr) (q : Rat) (n d proof : Expr)
+  deriving Inhabited
 
 section
 set_option linter.unusedVariables false
 
 /-- The result of `norm_num` running on an expression `x` of type `α`. -/
 @[nolint unusedArguments] def Result {α : Q(Type u)} (x : Q($α)) := Result'
 
+instance : Inhabited (Result x) := inferInstanceAs (Inhabited Result')
+
 /-- The result is `lit : ℕ` (a raw nat literal) and `proof : isNat x lit`. -/
 @[match_pattern, inline] def Result.isNat {α : Q(Type u)} {x : Q($α)} :
     ∀ (inst : Q(Semiring $α) := by assumption) (lit : Q(ℕ)) (proof : Q(IsNat $x $lit)),
@@ -165,7 +197,7 @@ Extract from a `Result` the integer value (as both a term and an expression),
 and the proof that the original expression is equal to this integer.
 -/
 def Result.toInt {α : Q(Type u)} {e : Q($α)} (_i : Q(Ring $α) := by with_reducible assumption) :
-    Result e → MetaM (ℤ × (lit : Q(ℤ)) × Q(IsInt $e $lit))
+    Result e → Option (ℤ × (lit : Q(ℤ)) × Q(IsInt $e $lit))
   | .isNat _ lit proof => do
     have proof : Q(@IsNat _ Ring.toSemiring $e $lit) := proof
     pure ⟨lit.natLit!, q(.ofNat $lit), q(($proof).to_isInt)⟩
@@ -178,17 +210,39 @@ instance : ToMessageData (Result x) where
   | .isNegNat _ lit proof => m!"isNegNat {lit} ({proof})"
   | .isRat _ q _ _ proof => m!"isRat {q} ({proof})"
 
+/--
+Given a `NormNum.Result e` (which uses `IsNat` or `IsInt` to express equality to an integer
+numeral), converts it to an equality `e = Nat.rawCast n` or `e = Int.rawCast n` to a raw cast
+expression, so it can be used for rewriting.
+-/
+def Result.toRawEq {α : Q(Type u)} {e : Q($α)} : Result e → (ℤ × (e' : Q($α)) × Q($e = $e'))
+  | .isNat _ lit p => ⟨lit.natLit!, q(Nat.rawCast $lit), q(IsNat.to_raw_eq $p)⟩
+  | .isNegNat _ lit p => ⟨-lit.natLit!, q(Int.rawCast (.negOfNat $lit)), q(IsInt.to_raw_eq $p)⟩
+  | .isRat _ .. => ⟨0, (default : Expr), (default : Expr)⟩ -- TODO
+
+/-- Constructs a `Result` out of a raw nat cast. Assumes `e` is a raw nat cast expression. -/
+def Result.ofRawNat {α : Q(Type u)} (e : Q($α)) : Result e := Id.run do
+  let .app (.app _ (sα : Q(Semiring $α))) (lit : Q(ℕ)) := e | panic! "not a raw nat cast"
+  .isNat sα lit (q(IsNat.of_raw $α $lit) : Expr)
+
+/-- Constructs a `Result` out of a raw int cast.
+Assumes `e` is a raw int cast expression denoting `n`. -/
+def Result.ofRawInt {α : Q(Type u)} (n : ℤ) (e : Q($α)) : Result e :=
+  if 0 ≤ n then
+    Result.ofRawNat e
+  else Id.run do
+    let .app (.app _ (rα : Q(Ring $α))) (.app _ (lit : Q(ℕ))) := e | panic! "not a raw int cast"
+    .isNegNat rα lit (q(IsInt.of_raw $α (.negOfNat $lit)) : Expr)
+
 /--
 Convert a `Result` to a `Simp.Result`.
 -/
 def Result.toSimpResult {α : Q(Type u)} {e : Q($α)} : Result e → MetaM Simp.Result
   | .isNat _sα lit p => do
-    let p : Q(IsNat $e $lit) := p
     let _ofNatInst ← synthInstanceQ (q(OfNat $α $lit) : Q(Type u))
     let _lawfulInst ← synthInstanceQ (q(LawfulOfNat $α $lit) : Q(Prop))
     return { expr := q((OfNat.ofNat $lit : $α)), proof? := q(IsNat.to_eq $lit $e $p) }
   | .isNegNat _rα lit p => do
-    let p : Q(IsInt $e (.negOfNat $lit)) := p
     let _ofNatInst ← synthInstanceQ (q(OfNat $α $lit) : Q(Type u))
     let _lawfulInst ← synthInstanceQ (q(LawfulOfNat $α $lit) : Q(Prop))
     return { expr := q(-(OfNat.ofNat $lit : $α)), proof? := q(IsInt.neg_to_eq $lit $e $p) }
@@ -267,7 +321,7 @@ returning a typed expression `lit : ℤ`, and a proof of `isInt e lit`. -/
 def deriveInt {α : Q(Type u)} (e : Q($α))
     (_inst : Q(Ring $α) := by with_reducible assumption) :
     MetaM ((lit : Q(ℤ)) × Q(IsInt $e $lit)) := do
-  let ⟨_, lit, proof⟩ ← (← derive e).toInt
+  let some ⟨_, lit, proof⟩ := (← derive e).toInt | failure
   pure ⟨lit, proof⟩
 
 /-- Extract the natural number `n` if the expression is of the form `OfNat.ofNat n`. -/