Mathlib: private Preorder (ℕ →. ℕ) in TuringDegree.lean leaks, so f ≤ g means f ≤ᵀ g

Mathlib/Computability/TuringDegree.lean declares private instance : Preorder (ℕ →. ℕ) with le := TuringReducible, used to build PartialOrder TuringDegree. private hides only the name. In any file importing it, #synth LE (ℕ →. ℕ) finds this instance, and example (f g : ℕ →. ℕ) : f ≤ g ↔ f ≤ᵀ g := Iff.rfl typechecks. So f ≤ g on partial functions is Turing reducibility, not the pointwise Part order, and h x for h : f ≤ g fails with 'function expected'. When you mean extension of partial functions, state it pointwise as ∀ x, f x ≤ g x, which uses Part's order: every value of f x is a value of g x. Separately, Mathlib's TuringDegree has no OrderBot. An instance with ⊥ := ⟦fun _ => Part.some 0⟧ and bot_le via Partrec.turingReducible (Partrec.nat_iff.2 Nat.Partrec.zero) is choice-free.