feat(CategoryTheory/Bicategory): add lemmas about mates in bicategories

[yuma-mizuno]

Continued from #20891. This PR completes the bicategorical proofs for the lemmas whose Cat versions are provided in Mathlib/CategoryTheory/Adjunction/Mates.lean.

---

• depends on: [Merged by Bors] - feat(CategoryTheory/Bicategory): define mates in bicategories #20891

[github-actions]

PR summary ebf0d07f67

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Bicategory.Adjunction.Mate	282	283	+1 (+0.35%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Bicategory.Adjunction.Mate	1

---

Declarations diff

+ conjugateEquiv
+ conjugateEquiv_adjunction_id
+ conjugateEquiv_adjunction_id_symm
+ conjugateEquiv_apply
+ conjugateEquiv_apply'
+ conjugateEquiv_comm
+ conjugateEquiv_comp
+ conjugateEquiv_id
+ conjugateEquiv_iso
+ conjugateEquiv_mateEquiv_vcomp
+ conjugateEquiv_of_iso
+ conjugateEquiv_symm_apply
+ conjugateEquiv_symm_apply'
+ conjugateEquiv_symm_comm
+ conjugateEquiv_symm_comp
+ conjugateEquiv_symm_id
+ conjugateEquiv_symm_iso
+ conjugateEquiv_symm_of_iso
+ conjugateIsoEquiv
+ iterated_mateEquiv_conjugateEquiv
+ iterated_mateEquiv_conjugateEquiv_symm
+ leftAdjointConjugateSquare.vcomp
+ leftAdjointSquare.comp
+ leftAdjointSquare.comp_hvcomp
+ leftAdjointSquare.comp_vhcomp
+ leftAdjointSquareConjugate.vcomp
+ mateEquiv_conjugateEquiv_vcomp
+ mateEquiv_square
+ rightAdjointConjugateSquare.vcomp
+ rightAdjointSquare.comp
+ rightAdjointSquare.comp_hvcomp
+ rightAdjointSquare.comp_vhcomp
+ rightAdjointSquareConjugate.vcomp

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory/Bicategory): define mates in bicategories #20891
  By Dependent Issues (🤖). Happy coding!