mathlib

76de8ae0 - chore(*): Fix mistakes (#18654)

chore(*): Fix mistakes (#18654) Fix naming errors and non-defeq diamonds recently introduced. Those were discovered during the port.