feat(*): Clean up some misstated lemmas about algebra (#9417)

Similar to #9395 clean up a few lemmas whose statement doesn't match the name / docstring about algebraic things, all of these are duplicates of other lemmas, so look like copy paste errors.

src/algebra/group/hom.lean

@@ -495,10 +495,10 @@ lemma one_hom.cancel_left [has_one M] [has_one N] [has_one P]
 ⟨λ h, one_hom.ext $ λ x, hg $ by rw [← one_hom.comp_apply, h, one_hom.comp_apply],
  λ h, h ▸ rfl⟩
 @[to_additive]
-lemma mul_hom.cancel_left [has_one M] [has_one N] [has_one P]
-  {g : one_hom N P} {f₁ f₂ : one_hom M N} (hg : function.injective g) :
+lemma mul_hom.cancel_left [has_mul M] [has_mul N] [has_mul P]
+  {g : mul_hom N P} {f₁ f₂ : mul_hom M N} (hg : function.injective g) :
   g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
-⟨λ h, one_hom.ext $ λ x, hg $ by rw [← one_hom.comp_apply, h, one_hom.comp_apply],
+⟨λ h, mul_hom.ext $ λ x, hg $ by rw [← mul_hom.comp_apply, h, mul_hom.comp_apply],
  λ h, h ▸ rfl⟩
 @[to_additive]
 lemma monoid_hom.cancel_left [mul_one_class M] [mul_one_class N] [mul_one_class P]

src/category_theory/limits/constructions/limits_of_products_and_equalizers.lean

@@ -269,9 +269,9 @@ Any category with coproducts and coequalizers has all colimits.
 See https://stacks.math.columbia.edu/tag/002P.
 -/
 lemma colimits_from_coequalizers_and_coproducts
-  [has_products C] [has_equalizers C] : has_limits C :=
-{ has_limits_of_shape := λ J 𝒥,
-  { has_limit := λ F, by exactI has_limit_of_equalizer_and_product F } }
+  [has_coproducts C] [has_coequalizers C] : has_colimits C :=
+{ has_colimits_of_shape := λ J 𝒥,
+  { has_colimit := λ F, by exactI has_colimit_of_coequalizer_and_coproduct F } }
 
 /--
 Any category with finite coproducts and coequalizers has all finite colimits.

src/data/int/parity.lean

@@ -45,7 +45,7 @@ by rw [not_odd_iff, even_iff]
 @[simp] lemma odd_iff_not_even : odd n ↔ ¬ even n :=
 by rw [not_even_iff, odd_iff]
 
-lemma is_compl_even_odd : is_compl {n : ℕ | even n} {n | odd n} :=
+lemma is_compl_even_odd : is_compl {n : ℤ | even n} {n | odd n} :=
 by simp [← set.compl_set_of, is_compl_compl]
 
 lemma even_or_odd (n : ℤ) : even n ∨ odd n :=

src/linear_algebra/matrix/symmetric.lean

@@ -47,7 +47,7 @@ lemma is_symm_mul_transpose_self [fintype n] [comm_semiring α] (A : matrix n n
 transpose_mul _ _
 
 lemma is_symm_transpose_mul_self [fintype n] [comm_semiring α] (A : matrix n n α) :
-  (A ⬝ Aᵀ).is_symm :=
+  (Aᵀ ⬝ A).is_symm :=
 transpose_mul _ _
 
 lemma is_symm_add_transpose_self [add_comm_semigroup α] (A : matrix n n α) :