Lean 4 Mathlib: `Quotient.lift` resolves to CategoryTheory.Quotient inside namespaces

Inside namespace CategoryTheory... (e.g. CategoryTheory.Triangulated.TStructure), Quotient.lift, Quotient.sound, Quotient.exists_rep may resolve to the category-theory CategoryTheory.Quotient namespace (quotient categories), giving baffling errors like 'Invalid argument name s for function Quotient.lift' or an expected type ⦃Y⦄ → (S ⟶ Y) → (S ⟶ Y) → Prop (a HomRel). Write _root_.Quotient.lift (s := mySetoid) .... Also, when the quotient type is a def (def SimpleIsoClass C := Quotient (simpleIsoSetoid C)), pass the setoid explicitly via (s := ...) so the elaborator can see through the def.