The link of https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html#managing-type-class-inference is invalid now, should be replaced with https://leanprover.github.io/theorem_proving_in_lean4/Type-Classes/#managing-type-class-inference