[Merged by Bors] - chore: remove import alls by making some norm_num components public

Mathlib/Tactic/NormNum/DivMod.lean

@@ -100,37 +100,23 @@ lemma isInt_emod {a b q m a' : ℤ} {b' r : ℕ}
 lemma isInt_emod_neg {a b : ℤ} {r : ℕ} (h : IsNat (a % -b) r) : IsNat (a % b) r :=
   ⟨by rw [← Int.emod_neg, h.out]⟩
 
-attribute [local instance] monadLiftOptionMetaM in
-/-- The `norm_num` extension which identifies expressions of the form `Int.emod a b`,
-such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num (_ : ℤ) % _, Int.emod _ _]
-partial def evalIntMod : NormNumExt where eval {u α} e := do
-  let .app (.app f (a : Q(ℤ))) (b : Q(ℤ)) ← whnfR e | failure
-  -- We assert that the default instance for `HMod` is `Int.mod` when the first parameter is `ℤ`.
-  guard <|← withNewMCtxDepth <| isDefEq f q(HMod.hMod (α := ℤ))
-  haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q ℤ := ⟨⟩
-  haveI' : $e =Q ($a % $b) := ⟨⟩
-  let rℤ : Q(Ring ℤ) := q(Int.instRing)
-  let some ⟨za, na, pa⟩ := (← derive a).toInt rℤ | failure
-  go a na za pa b (← derive (u := .zero) b)
+/-- Given a result for evaluating `a b` in `ℤ`, evaluate `a % b`. -/
+def evalIntMod.go (a na : Q(ℤ)) (za : ℤ) (pa : Q(IsInt $a $na))
+    (b : Q(ℤ)) : Result (u := .zero) b → Option (Result q($a % $b))
+  | .isNat _ nb pb => do
+    assumeInstancesCommute
+    if nb.natLit! == 0 then
+      have _ : $nb =Q nat_lit 0 := ⟨⟩
+      return .isInt q(Int.instRing) na za q(isInt_emod_zero $pa $pb)
+    else
+      let ⟨r, p⟩ := core a na za pa b nb pb
+      return .isNat q(instAddMonoidWithOne) r p
+  | .isNegNat _ nb pb => do
+    assumeInstancesCommute
+    let ⟨r, p⟩ := core a na za pa q(-$b) nb q(isNat_neg_of_isNegNat $pb)
+    return .isNat q(instAddMonoidWithOne) r q(isInt_emod_neg $p)
+  | _ => none
 where
-  /-- Given a result for evaluating `a b` in `ℤ`, evaluate `a % b`. -/
-  go (a na : Q(ℤ)) (za : ℤ) (pa : Q(IsInt $a $na))
-      (b : Q(ℤ)) : Result b → Option (Result q($a % $b))
-    | .isNat inst nb pb => do
-      assumeInstancesCommute
-      if nb.natLit! == 0 then
-        have _ : $nb =Q nat_lit 0 := ⟨⟩
-        return .isInt q(Int.instRing) na za q(isInt_emod_zero $pa $pb)
-      else
-        let ⟨r, p⟩ := core a na za pa b nb pb
-        return .isNat q(instAddMonoidWithOne) r p
-    | .isNegNat _ nb pb => do
-      assumeInstancesCommute
-      let ⟨r, p⟩ := core a na za pa q(-$b) nb q(isNat_neg_of_isNegNat $pb)
-      return .isNat q(instAddMonoidWithOne) r q(isInt_emod_neg $p)
-    | _ => none
-
   /-- Given a result for evaluating `a b` in `ℤ` where `b > 0`, evaluate `a % b`. -/
   core (a na : Q(ℤ)) (za : ℤ) (pa : Q(IsInt $a $na))
       (b : Q(ℤ)) (nb : Q(ℕ)) (pb : Q(IsNat $b $nb)) :
@@ -147,6 +133,20 @@ where
     have pf₃ : Q(Nat.blt $nr $nb = true) := (q(Eq.refl true) :)
     ⟨nr, q(isInt_emod $pa $pb $pf₁ $pf₂ $pf₃)⟩
 
+attribute [local instance] monadLiftOptionMetaM in
+/-- The `norm_num` extension which identifies expressions of the form `Int.emod a b`,
+such that `norm_num` successfully recognises both `a` and `b`. -/
+@[norm_num (_ : ℤ) % _, Int.emod _ _]
+partial def evalIntMod : NormNumExt where eval {u α} e := do
+  let .app (.app f (a : Q(ℤ))) (b : Q(ℤ)) ← whnfR e | failure
+  -- We assert that the default instance for `HMod` is `Int.mod` when the first parameter is `ℤ`.
+  guard <|← withNewMCtxDepth <| isDefEq f q(HMod.hMod (α := ℤ))
+  haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q ℤ := ⟨⟩
+  haveI' : $e =Q ($a % $b) := ⟨⟩
+  let rℤ : Q(Ring ℤ) := q(Int.instRing)
+  let some ⟨za, na, pa⟩ := (← derive a).toInt rℤ | failure
+  evalIntMod.go a na za pa b (← derive (u := .zero) b)
+
 theorem isInt_dvd_true : {a b : ℤ} → {a' b' c : ℤ} →
     IsInt a a' → IsInt b b' → Int.mul a' c = b' → a ∣ b
   | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨_, rfl⟩

Mathlib/Tactic/NormNum/Ineq.lean

@@ -179,21 +179,9 @@ theorem isInt_lt_false [Ring α] [PartialOrder α] [IsOrderedRing α] {a b : α}
   not_lt_of_ge (isInt_le_true hb ha h)
 
 attribute [local instance] monadLiftOptionMetaM in
-/-- The `norm_num` extension which identifies expressions of the form `a ≤ b`,
-such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num _ ≤ _] def evalLE : NormNumExt where eval {v β} e := do
-  haveI' : v =QL 0 := ⟨⟩; haveI' : $β =Q Prop := ⟨⟩
-  let .app (.app f a) b ← whnfR e | failure
-  let ⟨u, α, a⟩ ← inferTypeQ' a
-  have b : Q($α) := b
-  let ra ← derive a; let rb ← derive b
-  let lα ← synthInstanceQ q(LE $α)
-  guard <|← withNewMCtxDepth <| isDefEq f q(LE.le (α := $α))
-  core lα ra rb
-where
-  /-- Identify (as `true` or `false`) expressions of the form `a ≤ b`, where `a` and `b` are numeric
-  expressions whose evaluations to `NormNum.Result` have already been computed. -/
-  core {u : Level} {α : Q(Type u)} (lα : Q(LE $α)) {a b : Q($α)}
+/-- Identify (as `true` or `false`) expressions of the form `a ≤ b`, where `a` and `b` are numeric
+expressions whose evaluations to `NormNum.Result` have already been computed. -/
+def evalLE.core {u : Level} {α : Q(Type u)} (lα : Q(LE $α)) {a b : Q($α)}
     (ra : NormNum.Result a) (rb : NormNum.Result b) : MetaM (NormNum.Result q($a ≤ $b)) := do
   let e := q($a ≤ $b)
   let rec intArm : MetaM (Result e) := do
@@ -243,22 +231,22 @@ where
     else -- Nats can appear in an ordered ring without `CharZero`.
       intArm
 
-attribute [local instance] monadLiftOptionMetaM in
-/-- The `norm_num` extension which identifies expressions of the form `a < b`,
+/-- The `norm_num` extension which identifies expressions of the form `a ≤ b`,
 such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num _ < _] def evalLT : NormNumExt where eval {v β} e := do
+@[norm_num _ ≤ _] def evalLE : NormNumExt where eval {v β} e := do
   haveI' : v =QL 0 := ⟨⟩; haveI' : $β =Q Prop := ⟨⟩
   let .app (.app f a) b ← whnfR e | failure
   let ⟨u, α, a⟩ ← inferTypeQ' a
   have b : Q($α) := b
   let ra ← derive a; let rb ← derive b
-  let lα ← synthInstanceQ q(LT $α)
-  guard <|← withNewMCtxDepth <| isDefEq f q(LT.lt (α := $α))
-  core lα ra rb
-where
-  /-- Identify (as `true` or `false`) expressions of the form `a < b`, where `a` and `b` are numeric
-  expressions whose evaluations to `NormNum.Result` have already been computed. -/
-  core {u : Level} {α : Q(Type u)} (lα : Q(LT $α)) {a b : Q($α)}
+  let lα ← synthInstanceQ q(LE $α)
+  guard <|← withNewMCtxDepth <| isDefEq f q(LE.le (α := $α))
+  evalLE.core lα ra rb
+
+attribute [local instance] monadLiftOptionMetaM in
+/-- Identify (as `true` or `false`) expressions of the form `a < b`, where `a` and `b` are numeric
+expressions whose evaluations to `NormNum.Result` have already been computed. -/
+def evalLT.core {u : Level} {α : Q(Type u)} (lα : Q(LT $α)) {a b : Q($α)}
     (ra : NormNum.Result a) (rb : NormNum.Result b) : MetaM (NormNum.Result q($a < $b)) := do
   let e := q($a < $b)
   let rec intArm : MetaM (Result e) := do
@@ -323,4 +311,16 @@ where
       let r : Q(Nat.ble $nb $na = true) := (q(Eq.refl true) : Expr)
       return .isFalse q(isNat_lt_false $pa $pb $r)
 
+/-- The `norm_num` extension which identifies expressions of the form `a < b`,
+such that `norm_num` successfully recognises both `a` and `b`. -/
+@[norm_num _ < _] def evalLT : NormNumExt where eval {v β} e := do
+  haveI' : v =QL 0 := ⟨⟩; haveI' : $β =Q Prop := ⟨⟩
+  let .app (.app f a) b ← whnfR e | failure
+  let ⟨u, α, a⟩ ← inferTypeQ' a
+  have b : Q($α) := b
+  let ra ← derive a; let rb ← derive b
+  let lα ← synthInstanceQ q(LT $α)
+  guard <|← withNewMCtxDepth <| isDefEq f q(LT.lt (α := $α))
+  evalLT.core lα ra rb
+
 end Mathlib.Meta.NormNum

Mathlib/Tactic/NormNum/Prime.lean

@@ -119,12 +119,11 @@ theorem isNat_minFac_4 : {n n' k : ℕ} →
       _ ≤ n.minFac := h1.2.2
       _ ≤ m        := Nat.minFac_le_of_dvd hm h2mn
 
-/-- The `norm_num` extension which identifies expressions of the form `minFac n`. -/
-@[norm_num Nat.minFac _] partial def evalMinFac : NormNumExt where eval {_ _} e := do
-  let .app (.const ``Nat.minFac _) (n : Q(ℕ)) ← whnfR e | failure
+/-- The core of the `norm_num` extension which normalizes expressions of the form `minFac n`.
+This is public for use in the `Nat.primeFactorsList_ofNat` simproc. -/
+partial def evalMinFac.core (n : Q(ℕ)) (nn : Q(ℕ)) (pn : Q(IsNat $n $nn))
+    (n' : ℕ) : MetaM (Result q(Nat.minFac $n)) := do
   let sℕ : Q(AddMonoidWithOne ℕ) := q(Nat.instAddMonoidWithOne)
-  let ⟨nn, pn⟩ ← deriveNat n sℕ
-  let n' := nn.natLit!
   let rec aux (ek : Q(ℕ)) (prf : Q(MinFacHelper $nn $ek)) :
       (c : Q(ℕ)) × Q(IsNat (Nat.minFac $n) $c) :=
     let k := ek.natLit!
@@ -151,18 +150,22 @@ theorem isNat_minFac_4 : {n n' k : ℕ} →
         have ek' : Q(ℕ) := mkRawNatLit <| k + 2
         let pk' : Q($ek + 2 = $ek') := (q(Eq.refl $ek') : Expr)
         aux ek' q(minFacHelper_3 $pk' $r $prf)
-  let rec core : MetaM <| Result q(Nat.minFac $n) := do
-    if n' = 1 then
-      let pn : Q(IsNat $n (nat_lit 1)) := pn
-      return .isNat sℕ q(nat_lit 1) q(isNat_minFac_1 $pn)
-    if n' % 2 = 0 then
-      let pq : Q($nn % 2 = 0) := (q(Eq.refl 0) : Expr)
-      return .isNat sℕ q(nat_lit 2) q(isNat_minFac_2 $pn $pq)
-    let pp : Q(Nat.ble 2 $nn = true) := (q(Eq.refl true) : Expr)
-    let pq : Q(1 = $nn % 2) := (q(Eq.refl (nat_lit 1)) : Expr)
-    let ⟨c, pc⟩ := aux q(nat_lit 3) q(minFacHelper_0 $nn $pp $pq)
-    return .isNat sℕ c pc
-  core
+  if n' = 1 then
+    let pn : Q(IsNat $n (nat_lit 1)) := pn
+    return .isNat sℕ q(nat_lit 1) q(isNat_minFac_1 $pn)
+  if n' % 2 = 0 then
+    let pq : Q($nn % 2 = 0) := (q(Eq.refl 0) : Expr)
+    return .isNat sℕ q(nat_lit 2) q(isNat_minFac_2 $pn $pq)
+  let pp : Q(Nat.ble 2 $nn = true) := (q(Eq.refl true) : Expr)
+  let pq : Q(1 = $nn % 2) := (q(Eq.refl (nat_lit 1)) : Expr)
+  let ⟨c, pc⟩ := aux q(nat_lit 3) q(minFacHelper_0 $nn $pp $pq)
+  return .isNat sℕ c pc
+
+/-- The `norm_num` extension which identifies expressions of the form `minFac n`. -/
+@[norm_num Nat.minFac _] partial def evalMinFac : NormNumExt where eval {_ _} e := do
+  let .app (.const ``Nat.minFac _) (n : Q(ℕ)) ← whnfR e | failure
+  let ⟨nn, pn⟩ ← deriveNat n q(Nat.instAddMonoidWithOne)
+  evalMinFac.core n nn pn nn.natLit!
 
 theorem isNat_prime_0 : {n : ℕ} → IsNat n (nat_lit 0) → ¬ n.Prime
   | _, ⟨rfl⟩ => not_prime_zero
@@ -179,7 +182,7 @@ theorem isNat_not_prime {n n' : ℕ} (h : IsNat n n') : ¬n'.Prime → ¬n.Prime
 /-- The `norm_num` extension which identifies expressions of the form `Nat.Prime n`. -/
 @[norm_num Nat.Prime _] def evalNatPrime : NormNumExt where eval {_ _} e := do
   let .app (.const `Nat.Prime _) (n : Q(ℕ)) ← whnfR e | failure
-  let ⟨nn, pn⟩ ← deriveNat n _
+  let ⟨nn, pn⟩ ← deriveNat n q(Nat.instAddMonoidWithOne)
   let n' := nn.natLit!
   -- note: if `n` is not prime, we don't have to verify the calculation of `n.minFac`, we just have
   -- to compute it, which is a lot quicker
@@ -194,7 +197,7 @@ theorem isNat_not_prime {n n' : ℕ} (h : IsNat n n') : ¬n'.Prime → ¬n.Prime
         return .isFalse q(isNat_not_prime $pn $prf)
       let r : Q(Nat.ble 2 $nn = true) := (q(Eq.refl true) : Expr)
       let .isNat _ _lit (p2n : Q(IsNat (minFac $nn) $nn)) ←
-        evalMinFac.core nn _ nn q(.raw_refl _) nn.natLit! | failure
+        evalMinFac.core nn nn q(.raw_refl _) n' | failure
       return .isTrue q(isNat_prime_2 $pn $r $p2n)
   core
 

Mathlib/Tactic/ReduceModChar.lean

@@ -8,10 +8,11 @@ module
 public meta import Mathlib.Util.AtLocation
 public import Mathlib.Data.ZMod.Basic  -- shake: keep (Qq dependency)
 public import Mathlib.RingTheory.Polynomial.Basic  -- shake: keep (Qq dependency)
-import all Mathlib.Tactic.NormNum.DivMod  -- for accessing `evalIntMod.go`
 public import Mathlib.Tactic.NormNum.PowMod
 public import Mathlib.Tactic.ReduceModChar.Ext
 
+import Mathlib.Tactic.NormNum.DivMod
+
 /-!
 # `reduce_mod_char` tactic
 

Mathlib/Tactic/Ring/Compare.lean

@@ -5,7 +5,6 @@ Authors: Heather Macbeth
 -/
 module
 
-import all Mathlib.Tactic.NormNum.Ineq
 public import Mathlib.Tactic.NormNum.Ineq
 public import Mathlib.Tactic.Ring.Basic
 

Mathlib/Tactic/Simproc/Factors.lean

@@ -5,7 +5,6 @@ Authors: Mario Carneiro, Eric Wieser
 -/
 module
 
-import all Mathlib.Tactic.NormNum.Prime  -- for accessing `evalMinFac.core`
 public import Mathlib.Data.Nat.Factors
 public import Mathlib.Tactic.NormNum.Prime
 public import Batteries.Lean.Expr
@@ -113,7 +112,7 @@ private partial def evalPrimeFactorsListAux
       have ehp₂ : Q(Nat.blt $ea $eb = true) :=
         have : a < b := lt_of_le_of_ne' hab h_ba_eq
         (q(Eq.refl (true)) : Expr)
-      let .isNat _ lit ehp₃ ← evalMinFac.core q($eb) q(inferInstance) q($eb) ehb b | failure
+      let .isNat _ lit ehp₃ ← evalMinFac.core q($eb) q($eb) ehb b | failure
       assertInstancesCommute
       have : $lit =Q $eb := ⟨⟩
       let ⟨l, p₄⟩ ← evalPrimeFactorsListAux ehm ehb
@@ -130,7 +129,7 @@ private partial def evalPrimeFactorsListAux
       let eh_a_lt_n : Q(Nat.blt $ea $en = true) :=
         have : a < n := by lia
         (q(Eq.refl true) : Expr)
-      let .isNat _ lit ehn_minFac ← evalMinFac.core q($en) q(inferInstance) q($enl) ehn n | failure
+      let .isNat _ lit ehn_minFac ← evalMinFac.core q($en) q($enl) ehn n | failure
       have : $lit =Q $en := ⟨⟩
       assertInstancesCommute
       pure ⟨q([$en]), q(FactorsHelper.singleton $en $eh_a_lt_n $ehn_minFac)⟩