chore: Use the nat_lit elaborator more (#28666)

Also replace some `show`s working around Qq with `=Q`.

This code was already using Qq, so we may as well use the consistent spelling here.

Author: eric-wieser

Mathlib/Tactic/ModCases.lean

@@ -81,7 +81,7 @@ def modCases (h : TSyntax `Lean.binderIdent) (e : Q(ℤ)) (n : ℕ) : TacticM Un
   let ⟨u, p, g⟩ ← inferTypeQ (.mvar (← getMainGoal))
   have lit : Q(ℕ) := mkRawNatLit n
   have p₁ : Nat.ble 1 $lit =Q true := ⟨⟩
-  let (p₂, gs) ← proveOnModCases lit e (mkRawNatLit 0) p
+  let (p₂, gs) ← proveOnModCases lit e q(nat_lit 0) p
   let gs ← gs.mapM fun g => do
     let (fvar, g) ← match h with
     | `(binderIdent| $n:ident) => g.intro n.getId
@@ -156,7 +156,7 @@ def modCases (h : TSyntax `Lean.binderIdent) (e : Q(ℕ)) (n : ℕ) : TacticM Un
   let ⟨u, p, g⟩ ← inferTypeQ (.mvar (← getMainGoal))
   have lit : Q(ℕ) := mkRawNatLit n
   let p₁ : Q(Nat.ble 1 $lit = true) := (q(Eq.refl true) : Expr)
-  let (p₂, gs) ← proveOnModCases lit e (mkRawNatLit 0) p
+  let (p₂, gs) ← proveOnModCases lit e q(nat_lit 0) p
   let gs ← gs.mapM fun g => do
     let (fvar, g) ← match h with
     | `(binderIdent| $n:ident) => g.intro n.getId

Mathlib/Tactic/NormNum/Basic.lean

@@ -43,15 +43,15 @@ theorem isNat_zero (α) [AddMonoidWithOne α] : IsNat (Zero.zero : α) (nat_lit
 @[norm_num Zero.zero] def evalZero : NormNumExt where eval {u α} e := do
   let sα ← inferAddMonoidWithOne α
   match e with
-  | ~q(Zero.zero) => return .isNat sα (mkRawNatLit 0) q(isNat_zero $α)
+  | ~q(Zero.zero) => return .isNat sα q(nat_lit 0) q(isNat_zero $α)
 
 theorem isNat_one (α) [AddMonoidWithOne α] : IsNat (One.one : α) (nat_lit 1) := ⟨Nat.cast_one.symm⟩
 
 /-- The `norm_num` extension which identifies the expression `One.one`, returning `1`. -/
 @[norm_num One.one] def evalOne : NormNumExt where eval {u α} e := do
   let sα ← inferAddMonoidWithOne α
   match e with
-  | ~q(One.one) => return .isNat sα (mkRawNatLit 1) q(isNat_one $α)
+  | ~q(One.one) => return .isNat sα q(nat_lit 1) q(isNat_one $α)
 
 theorem isNat_ofNat (α : Type u) [AddMonoidWithOne α] {a : α} {n : ℕ}
     (h : n = a) : IsNat a n := ⟨h.symm⟩

Mathlib/Tactic/NormNum/BigOperators.lean

@@ -392,9 +392,8 @@ partial def evalFinsetSum : NormNumExt where eval {u β} e := do
   have f : Q($α → $β) := f
   let instCS : Q(CommSemiring $β) ← synthInstanceQ q(CommSemiring $β) <|>
     throwError "not a commutative semiring: {β}"
-  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
+  let pf : Q(IsNat (Finset.sum ∅ $f) (nat_lit 0)) := q(@Finset.sum_empty $β $α $instCS $f)
+  let res_empty := Result.isNat _ _ q($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

Mathlib/Tactic/NormNum/GCD.lean

@@ -92,10 +92,10 @@ theorem isInt_lcm : {x y nx ny : ℤ} → {z : ℕ} →
 and an equality proof. Panics if `ex` or `ey` aren't natural number literals. -/
 def proveNatGCD (ex ey : Q(ℕ)) : (ed : Q(ℕ)) × Q(Nat.gcd $ex $ey = $ed) :=
   match ex.natLit!, ey.natLit! with
-  | 0, _ => show (ed : Q(ℕ)) × Q(Nat.gcd 0 $ey = $ed) from ⟨ey, q(Nat.gcd_zero_left $ey)⟩
-  | _, 0 => show (ed : Q(ℕ)) × Q(Nat.gcd $ex 0 = $ed) from ⟨ex, q(Nat.gcd_zero_right $ex)⟩
-  | 1, _ => show (ed : Q(ℕ)) × Q(Nat.gcd 1 $ey = $ed) from ⟨mkRawNatLit 1, q(Nat.gcd_one_left $ey)⟩
-  | _, 1 => show (ed : Q(ℕ)) × Q(Nat.gcd $ex 1 = $ed) from ⟨mkRawNatLit 1, q(Nat.gcd_one_right $ex)⟩
+  | 0, _ => have : $ex =Q nat_lit 0 := ⟨⟩; ⟨ey, q(Nat.gcd_zero_left $ey)⟩
+  | _, 0 => have : $ey =Q nat_lit 0 := ⟨⟩; ⟨ex, q(Nat.gcd_zero_right $ex)⟩
+  | 1, _ => have : $ex =Q nat_lit 1 := ⟨⟩; ⟨q(nat_lit 1), q(Nat.gcd_one_left $ey)⟩
+  | _, 1 => have : $ey =Q nat_lit 1 := ⟨⟩; ⟨q(nat_lit 1), q(Nat.gcd_one_right $ex)⟩
   | x, y =>
     let (d, a, b) := Nat.xgcdAux x 1 0 y 0 1
     if d = x then
@@ -110,10 +110,10 @@ def proveNatGCD (ex ey : Q(ℕ)) : (ed : Q(ℕ)) × Q(Nat.gcd $ex $ey = $ed) :=
       if d = 1 then
         if a ≥ 0 then
           have pt : Q($ex * $ea' = $ey * $eb' + 1) := (q(Eq.refl ($ex * $ea')) : Expr)
-          ⟨mkRawNatLit 1, q(nat_gcd_helper_2' $ex $ey $ea' $eb' $pt)⟩
+          ⟨q(nat_lit 1), q(nat_gcd_helper_2' $ex $ey $ea' $eb' $pt)⟩
         else
           have pt : Q($ey * $eb' = $ex * $ea' + 1) := (q(Eq.refl ($ey * $eb')) : Expr)
-          ⟨mkRawNatLit 1, q(nat_gcd_helper_1' $ex $ey $ea' $eb' $pt)⟩
+          ⟨q(nat_lit 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_lit 0)) : Expr)
@@ -142,9 +142,9 @@ and an equality proof. Panics if `ex` or `ey` aren't natural number literals. -/
 def proveNatLCM (ex ey : Q(ℕ)) : (ed : Q(ℕ)) × Q(Nat.lcm $ex $ey = $ed) :=
   match ex.natLit!, ey.natLit! with
   | 0, _ =>
-    show (ed : Q(ℕ)) × Q(Nat.lcm 0 $ey = $ed) from ⟨mkRawNatLit 0, q(Nat.lcm_zero_left $ey)⟩
+    show (ed : Q(ℕ)) × Q(Nat.lcm 0 $ey = $ed) from ⟨q(nat_lit 0), q(Nat.lcm_zero_left $ey)⟩
   | _, 0 =>
-    show (ed : Q(ℕ)) × Q(Nat.lcm $ex 0 = $ed) from ⟨mkRawNatLit 0, q(Nat.lcm_zero_right $ex)⟩
+    show (ed : Q(ℕ)) × Q(Nat.lcm $ex 0 = $ed) from ⟨q(nat_lit 0), q(Nat.lcm_zero_right $ex)⟩
   | 1, _ => show (ed : Q(ℕ)) × Q(Nat.lcm 1 $ey = $ed) from ⟨ey, q(Nat.lcm_one_left $ey)⟩
   | _, 1 => show (ed : Q(ℕ)) × Q(Nat.lcm $ex 1 = $ed) from ⟨ex, q(Nat.lcm_one_right $ex)⟩
   | x, y =>

Mathlib/Tactic/NormNum/NatFib.lean

@@ -42,11 +42,11 @@ theorem isFibAux_two_mul_add_one {n a b n' a' b' : ℕ} (H : IsFibAux n a b)
 partial def proveNatFibAux (en' : Q(ℕ)) : (ea' eb' : Q(ℕ)) × Q(IsFibAux $en' $ea' $eb') :=
   match en'.natLit! with
   | 0 =>
-    show (ea' eb' : Q(ℕ)) × Q(IsFibAux 0 $ea' $eb') from
-    ⟨mkRawNatLit 0, mkRawNatLit 1, q(isFibAux_zero)⟩
+    have : $en' =Q nat_lit 0 := ⟨⟩;
+    ⟨q(nat_lit 0), q(nat_lit 1), q(isFibAux_zero)⟩
   | 1 =>
-    show (ea' eb' : Q(ℕ)) × Q(IsFibAux 1 $ea' $eb') from
-    ⟨mkRawNatLit 1, mkRawNatLit 1, q(isFibAux_one)⟩
+    have : $en' =Q nat_lit 1 := ⟨⟩;
+    ⟨q(nat_lit 1), q(nat_lit 1), q(isFibAux_one)⟩
   | n' =>
     have en : Q(ℕ) := mkRawNatLit <| n' / 2
     let ⟨ea, eb, H⟩ := proveNatFibAux en
@@ -79,9 +79,9 @@ theorem isFibAux_two_mul_add_one_done {n a b n' a' : ℕ} (H : IsFibAux n a b)
 and an equality proof. Panics if `ex` isn't a natural number literal. -/
 def proveNatFib (en' : Q(ℕ)) : (em : Q(ℕ)) × Q(Nat.fib $en' = $em) :=
   match en'.natLit! with
-  | 0 => show (em : Q(ℕ)) × Q(Nat.fib 0 = $em) from ⟨mkRawNatLit 0, q(Nat.fib_zero)⟩
-  | 1 => show (em : Q(ℕ)) × Q(Nat.fib 1 = $em) from ⟨mkRawNatLit 1, q(Nat.fib_one)⟩
-  | 2 => show (em : Q(ℕ)) × Q(Nat.fib 2 = $em) from ⟨mkRawNatLit 1, q(Nat.fib_two)⟩
+  | 0 => have : $en' =Q nat_lit 0 := ⟨⟩; ⟨q(nat_lit 0), q(Nat.fib_zero)⟩
+  | 1 => have : $en' =Q nat_lit 1 := ⟨⟩; ⟨q(nat_lit 1), q(Nat.fib_one)⟩
+  | 2 => have : $en' =Q nat_lit 2 := ⟨⟩; ⟨q(nat_lit 1), q(Nat.fib_two)⟩
   | n' =>
     have en : Q(ℕ) := mkRawNatLit <| n' / 2
     let ⟨ea, eb, H⟩ := proveNatFibAux en

Mathlib/Tactic/NormNum/NatLog.lean

@@ -39,12 +39,12 @@ Panics if `ex` or `en` aren't natural number literals.
 -/
 def proveNatLog (eb en : Q(ℕ)) : (ek : Q(ℕ)) × Q(Nat.log $eb $en = $ek) :=
   match eb.natLit!, en.natLit! with
-  | 0, _ => show (ek : Q(ℕ)) × Q(Nat.log 0 $en = $ek) from ⟨mkRawNatLit 0, q(nat_log_zero $en)⟩
-  | 1, _ => show (ek : Q(ℕ)) × Q(Nat.log 1 $en = $ek) from ⟨mkRawNatLit 0, q(nat_log_one $en)⟩
+  | 0, _ => have : $eb =Q nat_lit 0 := ⟨⟩; ⟨q(nat_lit 0), q(nat_log_zero $en)⟩
+  | 1, _ => have : $eb =Q nat_lit 1 := ⟨⟩; ⟨q(nat_lit 0), q(nat_log_one $en)⟩
   | b, n =>
     if n < b then
       have hh : Q(Nat.blt $en $eb = true) := (q(Eq.refl true) : Expr)
-      ⟨mkRawNatLit 0, q(nat_log_helper0 $eb $en $hh)⟩
+      ⟨q(nat_lit 0), q(nat_log_helper0 $eb $en $hh)⟩
     else
       let k := Nat.log b n
       have ek : Q(ℕ) := mkRawNatLit k
@@ -92,10 +92,10 @@ def proveNatClog (eb en : Q(ℕ)) : (ek : Q(ℕ)) × Q(Nat.clog $eb $en = $ek) :
   let n := en.natLit!
   if _ : b ≤ 1 then
     have h : Q(Nat.ble $eb 1 = true) := reflBoolTrue
-    ⟨mkRawNatLit 0, q(nat_clog_zero_left $eb $en $h)⟩
+    ⟨q(nat_lit 0), q(nat_clog_zero_left $eb $en $h)⟩
   else if _ : n ≤ 1 then
     have h : Q(Nat.ble $en 1 = true) := reflBoolTrue
-    ⟨mkRawNatLit 0, q(nat_clog_zero_right $eb $en $h)⟩
+    ⟨q(nat_lit 0), q(nat_clog_zero_right $eb $en $h)⟩
   else
     match h : Nat.clog b n with
     | 0 => False.elim <|

Mathlib/Tactic/NormNum/NatSqrt.lean

@@ -29,8 +29,8 @@ theorem isNat_sqrt : {x nx z : ℕ} → IsNat x nx → Nat.sqrt nx = z → IsNat
 and an equality proof. Panics if `ex` isn't a natural number literal. -/
 def proveNatSqrt (ex : Q(ℕ)) : (ey : Q(ℕ)) × Q(Nat.sqrt $ex = $ey) :=
   match ex.natLit! with
-  | 0 => show (ey : Q(ℕ)) × Q(Nat.sqrt 0 = $ey) from ⟨mkRawNatLit 0, q(Nat.sqrt_zero)⟩
-  | 1 => show (ey : Q(ℕ)) × Q(Nat.sqrt 1 = $ey) from ⟨mkRawNatLit 1, q(Nat.sqrt_one)⟩
+  | 0 => have : $ex =Q nat_lit 0 := ⟨⟩; ⟨q(nat_lit 0), q(Nat.sqrt_zero)⟩
+  | 1 => have : $ex =Q nat_lit 1 := ⟨⟩; ⟨q(nat_lit 1), q(Nat.sqrt_one)⟩
   | x =>
     let y := Nat.sqrt x
     have ey : Q(ℕ) := mkRawNatLit y

Mathlib/Tactic/NormNum/Pow.lean

@@ -75,7 +75,7 @@ partial def evalNatPow (a b : Q(ℕ)) : (c : Q(ℕ)) × Q(Nat.pow $a $b = $c) :=
     haveI : $b =Q 1 := ⟨⟩
     ⟨a, q(natPow_one)⟩
   else
-    let ⟨c, p⟩ := go b.natLit!.log2 a (mkRawNatLit 1) a b _ .rfl
+    let ⟨c, p⟩ := go b.natLit!.log2 a q(nat_lit 1) a b _ .rfl
     ⟨c, q(($p).run)⟩
 where
   /-- Invariants: `a ^ b₀ = c₀`, `depth > 0`, `b >>> depth = b₀`, `p := Nat.pow $a $b₀ = $c₀` -/

Mathlib/Tactic/NormNum/PowMod.lean

@@ -94,7 +94,7 @@ partial def evalNatPowMod (a b m : Q(ℕ)) : (c : Q(ℕ)) × Q(Nat.mod (Nat.pow
   else
     have c₀ : Q(ℕ) := mkRawNatLit (a.natLit! % m.natLit!)
     haveI : $c₀ =Q Nat.mod $a $m := ⟨⟩
-    let ⟨c, p⟩ := go b.natLit!.log2 a m (mkRawNatLit 1) c₀ b _ .rfl
+    let ⟨c, p⟩ := go b.natLit!.log2 a m q(nat_lit 1) c₀ b _ .rfl
     ⟨c, q(($p).run)⟩
 where
   /-- Invariants: `a ^ b₀ % m = c₀`, `depth > 0`, `b >>> depth = b₀` -/

Mathlib/Tactic/Ring/Basic.lean

@@ -596,9 +596,8 @@ def evalNegProd {a : Q($α)} (rα : Q(Ring $α)) (va : ExProd sα a) :
   Lean.Core.checkSystem decl_name%.toString
   match va with
   | .const za ha =>
-    let lit : Q(ℕ) := mkRawNatLit 1
     let ⟨m1, _⟩ := ExProd.mkNegNat sα rα 1
-    let rm := Result.isNegNat rα lit (q(IsInt.of_raw $α (.negOfNat $lit)) : Expr)
+    let rm := Result.isNegNat rα q(nat_lit 1) (q(IsInt.of_raw $α (.negOfNat (nat_lit 1))) : Expr)
     let ra := Result.ofRawRat za a ha
     let rb ← NormNum.evalMul.core q($m1 * $a) q(HMul.hMul) _ _
       q(CommSemiring.toSemiring) rm ra