feat: port RepresentationTheory.Action (#4700)

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Mathlib.lean

@@ -2231,6 +2231,7 @@ import Mathlib.Probability.ProbabilityMassFunction.Basic
 import Mathlib.Probability.ProbabilityMassFunction.Constructions
 import Mathlib.Probability.ProbabilityMassFunction.Monad
 import Mathlib.Probability.ProbabilityMassFunction.Uniform
+import Mathlib.RepresentationTheory.Action
 import Mathlib.RepresentationTheory.Basic
 import Mathlib.RepresentationTheory.Maschke
 import Mathlib.RingTheory.Adjoin.Basic

Mathlib/Algebra/Category/MonCat/Basic.lean

@@ -149,6 +149,21 @@ lemma ofHom_apply {X Y : Type u} [Monoid X] [Monoid Y] (f : X →* Y) (x : X) :
 set_option linter.uppercaseLean3 false in
 #align Mon.of_hom_apply MonCat.ofHom_apply
 
+---- porting note: added to ease the port of `RepresentationTheory.Action`
+@[to_additive]
+instance (X Y : MonCat.{u}) : One (X ⟶ Y) := ⟨ofHom 1⟩
+
+@[to_additive (attr := simp)]
+lemma oneHom_apply (X Y : MonCat.{u}) (x : X) : (1 : X ⟶ Y) x = 1 := rfl
+
+---- porting note: added to ease the port of `RepresentationTheory.Action`
+@[to_additive (attr := simp)]
+lemma one_of {A : Type _} [Monoid A] : (1 : MonCat.of A) = (1 : A) := rfl
+
+@[to_additive (attr := simp)]
+lemma mul_of {A : Type _} [Monoid A] (a b : A) :
+    @HMul.hMul (MonCat.of A) (MonCat.of A) (MonCat.of A) _ a b = a * b := rfl
+
 @[to_additive]
 instance {G : Type _} [Group G] : Group (MonCat.of G) := by assumption
 

Mathlib/CategoryTheory/Conj.lean

@@ -128,11 +128,7 @@ def conjAut : Aut X ≃* Aut Y :=
 set_option linter.uppercaseLean3 false in
 #align category_theory.iso.conj_Aut CategoryTheory.Iso.conjAut
 
-theorem conjAut_apply (f : Aut X) : α.conjAut f = α.symm ≪≫ f ≪≫ α := by
-  aesop_cat_nonterminal
-  apply CategoryTheory.Iso.ext
-  simp only [conjAut, Aut.unitsEndEquivAut, conj]
-  rfl
+theorem conjAut_apply (f : Aut X) : α.conjAut f = α.symm ≪≫ f ≪≫ α := by aesop_cat
 set_option linter.uppercaseLean3 false in
 #align category_theory.iso.conj_Aut_apply CategoryTheory.Iso.conjAut_apply
 

Mathlib/CategoryTheory/Endomorphism.lean

@@ -132,6 +132,11 @@ set_option linter.uppercaseLean3 false in
 
 namespace Aut
 
+-- porting note: added because `Iso.ext` is not triggered automatically
+@[ext]
+lemma ext {X : C} {φ₁ φ₂ : Aut X} (h : φ₁.hom = φ₂.hom) : φ₁ = φ₂ :=
+  Iso.ext h
+
 protected instance inhabited : Inhabited (Aut X) := ⟨Iso.refl X⟩
 set_option linter.uppercaseLean3 false in
 #align category_theory.Aut.inhabited CategoryTheory.Aut.inhabited