chore: bump quote4 (#5975)

Author: gebner

Mathlib/NumberTheory/LucasLehmer.lean

@@ -596,8 +596,7 @@ theorem isNat_not_lucasLehmerTest : {p np : ℕ} →
 @[norm_num LucasLehmer.LucasLehmerTest (_ : ℕ)]
 def evalLucasLehmerTest : NormNumExt where eval {u α} e := do
   let .app _ (p : Q(ℕ)) ← Meta.whnfR e | failure
-  let sℕ : Q(AddMonoidWithOne ℕ) := q(instAddMonoidWithOneNat)
-  let ⟨ep, hp⟩ ← deriveNat p
+  let ⟨ep, hp⟩ ← deriveNat p _
   let np := ep.natLit!
   unless 1 < np do
     failure

Mathlib/Tactic/ModCases.lean

@@ -60,13 +60,15 @@ and `b ≤ n`. Returns the list of subgoals `?gi : a ≡ i [ZMOD n] → p`.
 partial def proveOnModCases (n : Q(ℕ)) (a : Q(ℤ)) (b : Q(ℕ)) (p : Q(Sort u)) :
     MetaM (Q(OnModCases $n $a $b $p) × List MVarId) := do
   if n.natLit! ≤ b.natLit! then
-    pure ((q(onModCases_stop $p $n $a) : Expr), [])
+    haveI' : $b =Q $n := ⟨⟩
+    pure (q(onModCases_stop $p $n $a), [])
   else
     let ty := q($a ≡ OfNat.ofNat $b [ZMOD OfNat.ofNat $n] → $p)
-    let g : QQ ty ← mkFreshExprMVar ty
-    let ((pr : Q(OnModCases $n $a (Nat.add $b 1) $p)), acc) ←
-      proveOnModCases n a (mkRawNatLit (b.natLit! + 1)) p
-    pure ((q(onModCases_succ $b $g $pr) : Expr), g.mvarId! :: acc)
+    let g ← mkFreshExprMVarQ ty
+    have b1 : Q(ℕ) := mkRawNatLit (b.natLit! + 1)
+    haveI' : $b1 =Q ($b).succ := ⟨⟩
+    let (pr, acc) ← proveOnModCases n a b1 p
+    pure (q(onModCases_succ $b $g $pr), g.mvarId! :: acc)
 
 /--
 * The tactic `mod_cases h : e % 3` will perform a case disjunction on `e : ℤ` and yield subgoals

Mathlib/Tactic/NormNum/Basic.lean

@@ -105,51 +105,44 @@ lemma List.range_succ_eq_map' {n nn n' : ℕ} (pn : NormNum.IsNat n nn) (pn' : n
     List.range n = 0 :: List.map Nat.succ (List.range n') := by
   rw [pn.out, Nat.cast_id, pn', List.range_succ_eq_map]
 
+set_option linter.unusedVariables false in
 /-- Either show the expression `s : Q(List α)` is Nil, or remove one element from it.
 
 Fails if we cannot determine which of the alternatives apply to the expression.
 -/
-partial def List.proveNilOrCons {α : Q(Type u)} :
-  (s : Q(List $α)) → MetaM (List.ProveNilOrConsResult s) :=
-  fun s =>
+partial def List.proveNilOrCons {α : Q(Type u)} (s : Q(List $α)) :
+    MetaM (List.ProveNilOrConsResult s) :=
   s.withApp fun e a =>
   match (e, e.constName, a) with
-  | (_, `EmptyCollection.EmptyCollection, _) => pure (.nil (q(rfl) : Q((∅ : List $α) = [])))
-  | (_, `List.nil, _) => pure (.nil (q(rfl) : Q(([] : List $α) = [])))
-  | (_, `List.cons, #[_, a, s']) => pure (.cons a s' (q(rfl) : Q($s = $s)))
-  | (_, `List.range, #[(n : Q(ℕ))]) => do
-    let instAMO_nat : Q(AddMonoidWithOne ℕ) := q(AddCommMonoidWithOne.toAddMonoidWithOne)
-    let ⟨nn, pn⟩ ← NormNum.deriveNat n
+  | (_, ``EmptyCollection.emptyCollection, _) => haveI : $s =Q {} := ⟨⟩; pure (.nil q(.refl []))
+  | (_, ``List.nil, _) => haveI : $s =Q [] := ⟨⟩; pure (.nil q(rfl))
+  | (_, ``List.cons, #[_, (a : Q($α)), (s' : Q(List $α))]) =>
+    haveI : $s =Q $a :: $s' := ⟨⟩; pure (.cons a s' q(rfl))
+  | (_, ``List.range, #[(n : Q(ℕ))]) =>
+    have s : Q(List ℕ) := s; .uncheckedCast _ _ <$> show MetaM (ProveNilOrConsResult s) from do
+    let ⟨nn, pn⟩ ← NormNum.deriveNat n _
+    haveI' : $s =Q .range $n := ⟨⟩
     let nnL := nn.natLit!
     if nnL = 0 then
-      let pn : Q(@NormNum.IsNat _ _ $n 0) := pn
-      return .nil (q(List.range_zero' $pn) : Q(List.range $n = []))
+      haveI' : $nn =Q 0 := ⟨⟩
+      return .nil q(List.range_zero' $pn)
     else
       have n' : Q(ℕ) := mkRawNatLit (nnL - 1)
-      let pn' : Q($nn = Nat.succ $n') := (q(Eq.refl $nn) : Expr)
-      return (List.ProveNilOrConsResult.cons
-        q(0)
-        q(List.map Nat.succ (List.range $n'))
-        q(List.range_succ_eq_map' $pn $pn')).uncheckedCast (q(List.range ($n)) : Q(List ℕ)) s
-  | (_, `List.finRange, #[(n : Q(ℕ))]) => do
-    match ← Nat.unifyZeroOrSucc n with -- We want definitional equality on `n`.
-    | .zero _pf => do
-      pure (.nil (q(List.finRange_zero) : Q(List.finRange 0 = [])))
-    | .succ n' _pf => pure <| ((List.ProveNilOrConsResult.cons
-        q(0 : Fin (Nat.succ $n'))
-        (q(List.map Fin.succ (List.finRange $n')))
-        (q(List.finRange_succ_eq_map $n'))).uncheckedCast
-          (q(List.finRange (Nat.succ $n')) : Q(List (Fin (Nat.succ $n'))))
-          s)
-  | (.const `List.map [v, _], _, #[β, _, f, xxs]) => do
-    have β : Q(Type v) := β
-    have f : Q($β → $α) := f
-    have xxs : Q(List $β) := xxs
-    match ← List.proveNilOrCons xxs with
-    | .nil pf => pure <| (.nil
-      (q($pf ▸ List.map_nil) : Q(List.map $f $xxs = [])))
-    | .cons x xs pf => pure <| (.cons q($f $x) q(List.map $f $xs)
-      (q($pf ▸ List.map_cons $f $x $xs) : Q(List.map $f $xxs = $f $x :: List.map $f $xs)))
+      have : $nn =Q .succ $n' := ⟨⟩
+      return .cons _ _ q(List.range_succ_eq_map' $pn (.refl $nn))
+  | (_, ``List.finRange, #[(n : Q(ℕ))]) =>
+    have s : Q(List (Fin $n)) := s
+    .uncheckedCast _ _ <$> show MetaM (ProveNilOrConsResult s) from do
+    haveI' : $s =Q .finRange $n := ⟨⟩
+    return match ← Nat.unifyZeroOrSucc n with -- We want definitional equality on `n`.
+    | .zero _pf => .nil q(List.finRange_zero)
+    | .succ n' _pf => .cons _ _ q(List.finRange_succ_eq_map $n')
+  | (.const ``List.map [v, _], _, #[(β : Q(Type v)), _, (f : Q($β → $α)), (xxs : Q(List $β))]) => do
+    haveI' : $s =Q ($xxs).map $f := ⟨⟩
+    return match ← List.proveNilOrCons xxs with
+    | .nil pf => .nil q(($pf ▸ List.map_nil : List.map _ _ = _))
+    | .cons x xs pf => .cons q($f $x) q(($xs).map $f)
+      q(($pf ▸ List.map_cons $f $x $xs : List.map _ _ = _))
   | (_, fn, args) =>
     throwError "List.proveNilOrCons: unsupported List expression {s} ({fn}, {args})"
 
@@ -194,33 +187,31 @@ lemma Multiset.range_succ' {n nn n' : ℕ} (pn : NormNum.IsNat n nn) (pn' : nn =
 
 Fails if we cannot determine which of the alternatives apply to the expression.
 -/
-partial def Multiset.proveZeroOrCons {α : Q(Type u)} :
-  (s : Q(Multiset $α)) → MetaM (Multiset.ProveZeroOrConsResult s) :=
-  fun s =>
-  match Expr.getAppFnArgs s with
-  | (`EmptyCollection.EmptyCollection, _) => pure (.zero (q(rfl) : Q((∅ : Multiset $α) = 0)))
-  | (`Zero.zero, _) => pure (.zero (q(rfl) : Q((0 : Multiset $α) = 0)))
-  | (`Multiset.cons, #[_, a, s']) => pure (.cons a s' (q(rfl) : Q($s = $s)))
-  | (`Multiset.ofList, #[_, (val : Q(List $α))]) => do
-    match ← List.proveNilOrCons val with
-    | .nil pf => pure <| .zero (q($pf ▸ Multiset.coe_nil) : Q(($val : Multiset $α) = 0))
-    | .cons a s' pf => do
-      return (.cons a q($s')
-        (q($pf ▸ Multiset.cons_coe $a $s') : Q(↑$val = Multiset.cons $a $s')))
-  | (`Multiset.range, #[(n : Q(ℕ))]) => do
-    let instAMO_nat : Q(AddMonoidWithOne ℕ) := q(AddCommMonoidWithOne.toAddMonoidWithOne)
-    let ⟨nn, pn⟩ ← NormNum.deriveNat n
+partial def Multiset.proveZeroOrCons {α : Q(Type u)} (s : Q(Multiset $α)) :
+    MetaM (Multiset.ProveZeroOrConsResult s) :=
+  match s.getAppFnArgs with
+  | (``EmptyCollection.emptyCollection, _) => haveI : $s =Q {} := ⟨⟩; pure (.zero q(rfl))
+  | (``Zero.zero, _) => haveI : $s =Q 0 := ⟨⟩; pure (.zero q(rfl))
+  | (``Multiset.cons, #[_, (a : Q($α)), (s' : Q(Multiset $α))]) =>
+    haveI : $s =Q .cons $a $s' := ⟨⟩
+    pure (.cons a s' q(rfl))
+  | (``Multiset.ofList, #[_, (val : Q(List $α))]) => do
+    haveI : $s =Q .ofList $val := ⟨⟩
+    return match ← List.proveNilOrCons val with
+    | .nil pf => .zero q($pf ▸ Multiset.coe_nil : Multiset.ofList _ = _)
+    | .cons a s' pf => .cons a q($s') q($pf ▸ Multiset.cons_coe $a $s' : Multiset.ofList _ = _)
+  | (``Multiset.range, #[(n : Q(ℕ))]) => do
+    have s : Q(Multiset ℕ) := s; .uncheckedCast _ _ <$> show MetaM (ProveZeroOrConsResult s) from do
+    let ⟨nn, pn⟩ ← NormNum.deriveNat n _
+    haveI' : $s =Q .range $n := ⟨⟩
     let nnL := nn.natLit!
     if nnL = 0 then
-      let pn : Q(@NormNum.IsNat _ _ $n 0) := pn
-      return .zero (q(Multiset.range_zero' $pn) : Q(Multiset.range $n = 0))
+      haveI' : $nn =Q 0 := ⟨⟩
+      return .zero q(Multiset.range_zero' $pn)
     else
       have n' : Q(ℕ) := mkRawNatLit (nnL - 1)
-      let pn' : Q($nn = Nat.succ $n') := (q(Eq.refl $nn) : Expr)
-      return (Multiset.ProveZeroOrConsResult.cons
-        n'
-        q(Multiset.range $n')
-        q(Multiset.range_succ' $pn $pn')).uncheckedCast (q(Multiset.range ($n)) : Q(Multiset ℕ)) s
+      haveI' : $nn =Q ($n').succ := ⟨⟩
+      return .cons _ _ q(Multiset.range_succ' $pn rfl)
   | (fn, args) =>
     throwError "Multiset.proveZeroOrCons: unsupported multiset expression {s} ({fn}, {args})"
 
@@ -270,13 +261,14 @@ lemma Finset.univ_eq_elems {α : Type _} [Fintype α] (elems : Finset α)
 
 Fails if we cannot determine which of the alternatives apply to the expression.
 -/
-partial def Finset.proveEmptyOrCons {α : Q(Type u)} :
-  (s : Q(Finset $α)) → MetaM (Finset.ProveEmptyOrConsResult s) :=
-  fun s =>
-  match Expr.getAppFnArgs s with
-  | (`EmptyCollection.emptyCollection, _) => pure (.empty (q(rfl) : Q($s = $s)))
-  | (`Finset.cons, #[_, a, s', h]) => pure (.cons a s' h (q(rfl) : Q($s = $s)))
-  | (`Finset.mk, #[_, (val : Q(Multiset $α)), (nd : Q(Multiset.Nodup $val))]) => do
+partial def Finset.proveEmptyOrCons {α : Q(Type u)} (s : Q(Finset $α)) :
+    MetaM (ProveEmptyOrConsResult s) :=
+  match s.getAppFnArgs with
+  | (``EmptyCollection.emptyCollection, _) => haveI : $s =Q {} := ⟨⟩; pure (.empty q(rfl))
+  | (``Finset.cons, #[_, (a : Q($α)), (s' : Q(Finset $α)), (h : Q(¬ $a ∈ $s'))]) =>
+    haveI : $s =Q .cons $a $s' $h := ⟨⟩
+    pure (.cons a s' h q(.refl $s))
+  | (``Finset.mk, #[_, (val : Q(Multiset $α)), (nd : Q(Multiset.Nodup $val))]) => do
     match ← Multiset.proveZeroOrCons val with
     | .zero pf => pure <| .empty (q($pf ▸ Finset.mk_zero) : Q(Finset.mk $val $nd = ∅))
     | .cons a s' pf => do
@@ -285,29 +277,24 @@ partial def Finset.proveEmptyOrCons {α : Q(Type u)} :
       let h' : Q($a ∉ $s') := q((Multiset.nodup_cons.mp $h).1)
       return (.cons a q(Finset.mk $s' $nd') h'
         (q($pf ▸ Finset.mk_cons $h) : Q(Finset.mk $val $nd = Finset.cons $a ⟨$s', $nd'⟩ $h')))
-  | (`Finset.range, #[(n : Q(ℕ))]) => do
-    let instAMO_nat : Q(AddMonoidWithOne ℕ) := q(AddCommMonoidWithOne.toAddMonoidWithOne)
-    let ⟨nn, pn⟩ ← NormNum.deriveNat n
+  | (``Finset.range, #[(n : Q(ℕ))]) =>
+    have s : Q(Finset ℕ) := s; .uncheckedCast _ _ <$> show MetaM (ProveEmptyOrConsResult s) from do
+    let ⟨nn, pn⟩ ← NormNum.deriveNat n _
+    haveI' : $s =Q .range $n := ⟨⟩
     let nnL := nn.natLit!
     if nnL = 0 then
-      let pn : Q(@NormNum.IsNat _ _ $n 0) := pn
-      return .empty (q(Finset.range_zero' $pn) : Q(Finset.range $n = {}))
+      haveI : $nn =Q 0 := ⟨⟩
+      return .empty q(Finset.range_zero' $pn)
     else
       have n' : Q(ℕ) := mkRawNatLit (nnL - 1)
-      let pn' : Q($nn = Nat.succ $n') := (q(Eq.refl $nn) : Expr)
-      return (Finset.ProveEmptyOrConsResult.cons
-        n'
-        (q(Finset.range $n'))
-        (q(@Finset.not_mem_range_self $n'))
-        (q(Finset.range_succ' $pn $pn'))).uncheckedCast
-          (q(Finset.range $n) : Q(Finset ℕ))
-          s
-  | (`Finset.univ, #[_, instFT]) => do
-    match Expr.getAppFnArgs (← whnfI instFT) with
-    | (`Fintype.mk, #[_, (elems : Q(Finset $α)), (complete : Q(∀ x : $α, x ∈ $elems))]) => do
-      have _instFT : Q(Fintype $α) := instFT
+      haveI' : $nn =Q ($n').succ := ⟨⟩
+      return .cons n' _ _ q(Finset.range_succ' $pn (.refl $nn))
+  | (``Finset.univ, #[_, (instFT : Q(Fintype $α))]) => do
+    haveI' : $s =Q .univ := ⟨⟩
+    match (← whnfI instFT).getAppFnArgs with
+    | (``Fintype.mk, #[_, (elems : Q(Finset $α)), (complete : Q(∀ x : $α, x ∈ $elems))]) => do
       let res ← Finset.proveEmptyOrCons elems
-      pure <| res.eq_trans (q(Finset.univ_eq_elems $elems $complete) : Q(Finset.univ = $elems))
+      pure <| res.eq_trans q(Finset.univ_eq_elems $elems $complete)
     | e =>
       throwError "Finset.proveEmptyOrCons: could not determine elements of Fintype instance {e}"
   | (fn, args) =>
@@ -374,7 +361,7 @@ partial def evalFinsetProd : NormNumExt where eval {u β} e := do
   have α : Q(Type v) := α
   have s : Q(Finset $α) := s
   have f : Q($α → $β) := f
-  let instCS ← synthInstanceQ (q(CommSemiring $β) : Q(Type u)) <|>
+  let instCS : Q(CommSemiring $β) ← synthInstanceQ q(CommSemiring $β) <|>
     throwError "not a commutative semiring: {β}"
   let instS : Q(Semiring $β) := q(CommSemiring.toSemiring)
   -- Have to construct this expression manually, `q(1)` doesn't parse correctly:
@@ -384,7 +371,7 @@ partial def evalFinsetProd : NormNumExt where eval {u β} e := do
 
   evalFinsetBigop q(Finset.prod) f res_empty (fun {a s' h} res_fa res_prod_s' ↦ do
       let fa : Q($β) := Expr.app f a
-      let res : Result _ ← evalMul.core q($fa * Finset.prod $s' $f) q((· * ·)) _ _ instS res_fa
+      let res ← evalMul.core q($fa * Finset.prod $s' $f) q(HMul.hMul) _ _ instS res_fa
         res_prod_s'
       let eq : Q(Finset.prod (Finset.cons $a $s' $h) $f = $fa * Finset.prod $s' $f) :=
         q(Finset.prod_cons $h)
@@ -403,15 +390,15 @@ partial def evalFinsetSum : NormNumExt where eval {u β} e := do
   have α : Q(Type v) := α
   have s : Q(Finset $α) := s
   have f : Q($α → $β) := f
-  let instCS ← synthInstanceQ (q(CommSemiring $β) : Q(Type u)) <|>
+  let instCS : Q(CommSemiring $β) ← synthInstanceQ q(CommSemiring $β) <|>
     throwError "not a commutative semiring: {β}"
-  let n : Q(ℕ) := q(0)
+  let n : Q(ℕ) := mkRawNatLit 0
   let pf : Q(IsNat (Finset.sum ∅ $f) $n) := q(@Finset.sum_empty $β $α $instCS $f)
   let res_empty := Result.isNat _ n pf
 
   evalFinsetBigop q(Finset.sum) f res_empty (fun {a s' h} res_fa res_sum_s' ↦ do
       let fa : Q($β) := Expr.app f a
-      let res : Result _ ← evalAdd.core q($fa + Finset.sum $s' $f) q((· + ·)) _ _ res_fa res_sum_s'
+      let res ← evalAdd.core q($fa + Finset.sum $s' $f) q(HAdd.hAdd) _ _ res_fa res_sum_s'
       let eq : Q(Finset.sum (Finset.cons $a $s' $h) $f = $fa + Finset.sum $s' $f) :=
         q(Finset.sum_cons $h)
       pure <| res.eq_trans eq)

Mathlib/Tactic/NormNum/BigOperators.lean

@@ -98,10 +98,10 @@ def proveNatGCD (ex ey : Q(ℕ)) : (ed : Q(ℕ)) × Q(Nat.gcd $ex $ey = $ed) :=
   | x, y =>
     let (d, a, b) := Nat.xgcdAux x 1 0 y 0 1
     if d = x then
-      have pq : Q(Nat.mod $ey $ex = 0) := (q(@Eq.refl Nat 0) : Expr)
+      have pq : Q(Nat.mod $ey $ex = 0) := (q(Eq.refl (nat_lit 0)) : Expr)
       ⟨ex, q(nat_gcd_helper_dvd_left $ex $ey $pq)⟩
     else if d = y then
-      have pq : Q(Nat.mod $ex $ey = 0) := (q(@Eq.refl Nat 0) : Expr)
+      have pq : Q(Nat.mod $ex $ey = 0) := (q(Eq.refl (nat_lit 0)) : Expr)
       ⟨ey, q(nat_gcd_helper_dvd_right $ex $ey $pq)⟩
     else
       have ea' : Q(ℕ) := mkRawNatLit a.natAbs
@@ -115,8 +115,8 @@ def proveNatGCD (ex ey : Q(ℕ)) : (ed : Q(ℕ)) × Q(Nat.gcd $ex $ey = $ed) :=
           ⟨mkRawNatLit 1, q(nat_gcd_helper_1' $ex $ey $ea' $eb' $pt)⟩
       else
         have ed : Q(ℕ) := mkRawNatLit d
-        have pu : Q(Nat.mod $ex $ed = 0) := (q(@Eq.refl Nat 0) : Expr)
-        have pv : Q(Nat.mod $ey $ed = 0) := (q(@Eq.refl Nat 0) : Expr)
+        have pu : Q(Nat.mod $ex $ed = 0) := (q(Eq.refl (nat_lit 0)) : Expr)
+        have pv : Q(Nat.mod $ey $ed = 0) := (q(Eq.refl (nat_lit 0)) : Expr)
         if a ≥ 0 then
           have pt : Q($ex * $ea' = $ey * $eb' + $ed) := (q(Eq.refl ($ex * $ea')) : Expr)
           ⟨ed, q(nat_gcd_helper_2 $ed $ex $ey $ea' $eb' $pu $pv $pt)⟩
@@ -127,12 +127,13 @@ def proveNatGCD (ex ey : Q(ℕ)) : (ed : Q(ℕ)) × Q(Nat.gcd $ex $ey = $ed) :=
 @[norm_num Nat.gcd _ _]
 def evalNatGCD : NormNumExt where eval {u α} e := do
   let .app (.app _ (x : Q(ℕ))) (y : Q(ℕ)) ← Meta.whnfR e | failure
+  haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q ℕ := ⟨⟩
+  haveI' : $e =Q Nat.gcd $x $y := ⟨⟩
   let sℕ : Q(AddMonoidWithOne ℕ) := q(instAddMonoidWithOneNat)
   let ⟨ex, p⟩ ← deriveNat x sℕ
   let ⟨ey, q⟩ ← deriveNat y sℕ
   let ⟨ed, pf⟩ := proveNatGCD ex ey
-  let pf' : Q(IsNat (Nat.gcd $x $y) $ed) := q(isNat_gcd $p $q $pf)
-  return .isNat sℕ ed pf'
+  return .isNat sℕ ed q(isNat_gcd $p $q $pf)
 
 /-- Given natural number literals `ex` and `ey`, return their LCM as a natural number literal
 and an equality proof. Panics if `ex` or `ey` aren't natural number literals. -/
@@ -155,12 +156,13 @@ def proveNatLCM (ex ey : Q(ℕ)) : (ed : Q(ℕ)) × Q(Nat.lcm $ex $ey = $ed) :=
 @[norm_num Nat.lcm _ _]
 def evalNatLCM : NormNumExt where eval {u α} e := do
   let .app (.app _ (x : Q(ℕ))) (y : Q(ℕ)) ← Meta.whnfR e | failure
+  haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q ℕ := ⟨⟩
+  haveI' : $e =Q Nat.lcm $x $y := ⟨⟩
   let sℕ : Q(AddMonoidWithOne ℕ) := q(instAddMonoidWithOneNat)
   let ⟨ex, p⟩ ← deriveNat x sℕ
   let ⟨ey, q⟩ ← deriveNat y sℕ
   let ⟨ed, pf⟩ := proveNatLCM ex ey
-  let pf' : Q(IsNat (Nat.lcm $x $y) $ed) := q(isNat_lcm $p $q $pf)
-  return .isNat sℕ ed pf'
+  return .isNat sℕ ed q(isNat_lcm $p $q $pf)
 
 /-- Given two integers, return their GCD and an equality proof.
 Panics if `ex` or `ey` aren't integer literals. -/
@@ -174,14 +176,12 @@ def proveIntGCD (ex ey : Q(ℤ)) : (ed : Q(ℕ)) × Q(Int.gcd $ex $ey = $ed) :=
 @[norm_num Int.gcd _ _]
 def evalIntGCD : NormNumExt where eval {u α} e := do
   let .app (.app _ (x : Q(ℤ))) (y : Q(ℤ)) ← Meta.whnfR e | failure
-  let sℕ : Q(AddMonoidWithOne ℕ) := q(instAddMonoidWithOneNat)
-  let sℤ : Q(Ring ℤ) := q(Int.instRingInt)
-  let ⟨ex, p⟩ ← deriveInt x
-  let ⟨ey, q⟩ ← deriveInt y
+  let ⟨ex, p⟩ ← deriveInt x _
+  let ⟨ey, q⟩ ← deriveInt y _
+  haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q ℕ := ⟨⟩
+  haveI' : $e =Q Int.gcd $x $y := ⟨⟩
   let ⟨ed, pf⟩ := proveIntGCD ex ey
-  have pf : Q(Int.gcd $ex $ey = $ed) := pf
-  have pf' : Q(IsNat (Int.gcd $x $y) $ed) := q(isInt_gcd $p $q $pf)
-  return .isNat sℕ ed pf'
+  return .isNat _ ed q(isInt_gcd $p $q $pf)
 
 /-- Given two integers, return their LCM and an equality proof.
 Panics if `ex` or `ey` aren't integer literals. -/
@@ -195,14 +195,12 @@ def proveIntLCM (ex ey : Q(ℤ)) : (ed : Q(ℕ)) × Q(Int.lcm $ex $ey = $ed) :=
 @[norm_num Int.lcm _ _]
 def evalIntLCM : NormNumExt where eval {u α} e := do
   let .app (.app _ (x : Q(ℤ))) (y : Q(ℤ)) ← Meta.whnfR e | failure
-  let sℕ : Q(AddMonoidWithOne ℕ) := q(instAddMonoidWithOneNat)
-  let sℤ : Q(Ring ℤ) := q(Int.instRingInt)
-  let ⟨ex, p⟩ ← deriveInt x
-  let ⟨ey, q⟩ ← deriveInt y
+  let ⟨ex, p⟩ ← deriveInt x _
+  let ⟨ey, q⟩ ← deriveInt y _
+  haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q ℕ := ⟨⟩
+  haveI' : $e =Q Int.lcm $x $y := ⟨⟩
   let ⟨ed, pf⟩ := proveIntLCM ex ey
-  have pf : Q(Int.lcm $ex $ey = $ed) := pf
-  have pf' : Q(IsNat (Int.lcm $x $y) $ed) := q(isInt_lcm $p $q $pf)
-  return .isNat sℕ ed pf'
+  return .isNat _ ed q(isInt_lcm $p $q $pf)
 
 end NormNum
 

Mathlib/Tactic/NormNum/GCD.lean

@@ -48,9 +48,8 @@ def proveIntIsCoprime (ex ey : Q(ℤ)) : Q(IsCoprime $ex $ey) ⊕ Q(¬ IsCoprime
 @[norm_num IsCoprime (_ : ℤ) (_ : ℤ)]
 def evalIntIsCoprime : NormNumExt where eval {u α} e := do
   let .app (.app _ (x : Q(ℤ))) (y : Q(ℤ)) ← Meta.whnfR e | failure
-  let sℤ : Q(Ring ℤ) := q(Int.instRingInt)
-  let ⟨ex, p⟩ ← deriveInt x
-  let ⟨ey, q⟩ ← deriveInt y
+  let ⟨ex, p⟩ ← deriveInt x _
+  let ⟨ey, q⟩ ← deriveInt y _
   match proveIntIsCoprime ex ey with
   | .inl pf =>
     have pf' : Q(IsCoprime $x $y) := q(isInt_isCoprime $p $q $pf)