Commit 2024-01-16 02:11 87c10369

chore(Function): rename some lemmas (#9738)

• Merge Function.left_id and Function.comp.left_id into Function.id_comp.
• Merge Function.right_id and Function.comp.right_id into Function.comp_id.
• Merge Function.comp_const_right and Function.comp_const into Function.comp_const, use explicit arguments.
• Move Function.const_comp to Mathlib.Init.Function, use explicit arguments.