positivity under minimal imports: numerals, /, and factorial need separate imports

Tested on Lean v4.35.0 + Mathlib v4.35.0, in files with targeted imports instead of import Mathlib (the usual setup in module files). positivity's extensions live in different files, and a missing one gives only 'failed to prove positivity/nonnegativity/nonzeroness'. With Mathlib.Tactic.Positivity.Core + Mathlib.Algebra.Order.Field.Rat, even 0 ≤ x ^ 2 (x : ℚ) fails. Adding Mathlib.Tactic.Positivity.Basic makes x ^ 2, x + x (given 0 < x) and 0 < (n ! : ℚ) work. But numerals still fail: (0:ℚ) < 3, 0 < x + 1, and even (0:ℕ) < 3 ('failed to prove strict positivity'). Adding Mathlib.Tactic.NormNum.Basic fixes the numerals (importing Mathlib.Tactic.FieldSimp also brings them in). Division 0 < x / 2 additionally needs Mathlib.Algebra.Order.Field.Basic. The factorial gap also affects field_simp: with FieldSimp + Ring + Field.Rat + Nat.Factorial.Cast, field_simp leaves (m ! : ℚ) denominators in place, and adding Mathlib.Tactic.Positivity.Basic fixes it. To find the file for a head symbol, grep Mathlib for @[positivity <head> (e.g. √_ is in Mathlib/Analysis/Real/Sqrt.lean, Real.exp in Mathlib/Analysis/Complex/Exponential.lean).