chore(RepresentationTheory): remove some set_option backwards (leanprover-community#41057)

Removes several `set_option backward.defeqAttrib.useBackward true` / `set_option backward.isDefEq.respectTransparency false` workarounds in `Mathlib/RepresentationTheory`, replacing them with the `@[implicit_reducible]` attribute on the relevant functor definitions and simplifying a few proofs accordingly.

Author: Whysoserioushah

Mathlib/RepresentationTheory/Coinduced.lean

@@ -128,13 +128,11 @@ noncomputable abbrev coindMap {A B : Rep k G} (f : A ⟶ B) : coind φ A ⟶ coi
 variable (k) in
 /-- Given a monoid homomorphism `φ : G →* H`, this is the functor sending a `G`-representation `A`
 to the coinduced `H`-representation `coind φ A`, with action on maps given by postcomposition. -/
-@[simps obj map]
+@[implicit_reducible, simps obj map]
 noncomputable def coindFunctor : Rep.{t} k G ⥤ Rep k H where
   obj A := coind φ A
   map f := coindMap φ f
 
-set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 instance {G : Type v'} [Group G] (S : Subgroup G) :
     (coindFunctor k S.subtype).PreservesEpimorphisms where
   preserves {X Y} f := (epi_iff_surjective _).2 fun y => by
@@ -199,7 +197,7 @@ noncomputable def coindMap' {A B : Rep k G} (f : A ⟶ B) : coind' φ A ⟶ coin
 variable (k) in
 /-- Given a monoid homomorphism `φ : G →* H`, this is the functor sending a `G`-representation `A`
 to the coinduced `H`-representation `coind' φ A`, with action on maps given by postcomposition. -/
-@[simps obj map]
+@[implicit_reducible, simps obj map]
 noncomputable def coindFunctor' : Rep k G ⥤ Rep k H where
   obj A := coind' φ A
   map f := coindMap' φ f
@@ -228,8 +226,6 @@ noncomputable def coindVEquiv :
 noncomputable def coindIso : coind φ A ≅ coind' φ A :=
   Rep.mkIso <| .mk (coindVEquiv φ A) fun h => by ext; simp [homEquiv]
 
-set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 /-- Given a monoid homomorphism `φ : G →* H`, the coinduction functors `Rep k G ⥤ Rep k H` given by
 `coindFunctor k φ` and `coindFunctor' k φ` are naturally isomorphic, with isomorphism on objects
 given by `coindIso φ`. -/

Mathlib/RepresentationTheory/Coinvariants.lean

@@ -343,7 +343,7 @@ end
 variable (k G) [Monoid G] (A B : Rep.{w} k G)
 
 /-- The functor sending a representation to its coinvariants. -/
-@[simps! obj_carrier map_hom]
+@[implicit_reducible, simps! obj_carrier map_hom]
 noncomputable def coinvariantsFunctor : Rep.{w} k G ⥤ ModuleCat k where
   obj A := ModuleCat.of k A.ρ.Coinvariants
   map f := ModuleCat.ofHom (Representation.Coinvariants.map _ _ f.hom)
@@ -378,7 +378,6 @@ instance : (coinvariantsFunctor k G).Additive where
 instance : (coinvariantsFunctor k G).Linear k where
 
 set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 /-- The adjunction between the functor sending a representation to its coinvariants and the functor
 equipping a module with the trivial representation. -/
 @[simps]
@@ -394,7 +393,6 @@ theorem coinvariantsAdjunction_homEquiv_apply_hom {X : Rep.{w} k G} {Y : ModuleC
   rfl
 
 set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem coinvariantsAdjunction_homEquiv_symm_apply_hom {X : Rep.{w} k G} {Y : ModuleCat k}
     (f : X ⟶ (trivialFunctor k G).obj Y) :
@@ -437,7 +435,6 @@ section
 
 variable (k : Type u) {G : Type v} [CommRing k] [Group G]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Given a normal subgroup `S ≤ G`, this is the functor sending a `G`-representation `A` to the
 `G ⧸ S`-representation it induces on `A_S`. -/
 @[simps! obj_V map_hom_toLinearMap]
@@ -466,7 +463,6 @@ noncomputable def coinvariantsTensorFreeToFinsupp :
 
 variable {α}
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma coinvariantsTensorFreeToFinsupp_mk_tmul_single (x : A) (i : α) (g : G) (r : k) :
     DFunLike.coe (F := (A.ρ.tprod (Representation.free k G α)).Coinvariants →ₗ[k] α →₀ A.V)
@@ -487,7 +483,6 @@ noncomputable def finsuppToCoinvariantsTensorFree :
 variable {A α}
 
 set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma finsuppToCoinvariantsTensorFree_single (i : α) (x : A) :
     DFunLike.coe (F := (α →₀ A.V) →ₗ[k] (A.ρ.tprod (Representation.free k G α)).Coinvariants)

Mathlib/RepresentationTheory/FiniteIndex.lean

@@ -177,10 +177,9 @@ noncomputable def indCoindIso (A : Rep.{max w u} k S) :
 
 variable (k S)
 
-set_option backward.defeqAttrib.useBackward true in
 /-- Given a finite index subgroup `S ≤ G`, this is a natural isomorphism between the `Ind_S^G` and
 `Coind_G^S` functors `Rep k S ⥤ Rep k G`. -/
-@[simps! hom_app inv_app]
+@[implicit_reducible, simps! hom_app inv_app]
 noncomputable def indCoindNatIso :
     indFunctor k S.subtype ≅ coindFunctor.{max w u} k S.subtype :=
   NatIso.ofComponents (fun (A : Rep k S) => indCoindIso A) fun f => by
@@ -194,7 +193,6 @@ noncomputable def resIndAdjunction :
     resFunctor.{max w u v} S.subtype ⊣ indFunctor.{max w u v} k S.subtype :=
   (resCoindAdjunction.{max w u v} k S.subtype).ofNatIsoRight (indCoindNatIso.{max w u v} k S).symm
 
-
 omit [DecidableRel (QuotientGroup.rightRel S)] in
 @[instance] -- Note: we must use `@[instance] theorem` here due to [lean4#5595](https://github.com/leanprover/lean4/issues/5595).
 theorem instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype :
@@ -215,8 +213,6 @@ lemma resIndAdjunction_unit_app (B : Rep.{max w u v} k G) :
       (resCoindAdjunction.{max w u} k S.subtype).unit.app B ≫
       (indCoindIso.{max w (max u v)} (res S.subtype B)).inv := rfl
 
-set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 lemma resIndAdjunction_homEquiv_apply (A : Rep.{max w u v} k S)
     {B : Rep.{max w u v} k G} (f : res S.subtype B ⟶ A) :
     (resIndAdjunction.{w, u, v} k S).homEquiv _ _ f =
@@ -228,7 +224,7 @@ lemma resIndAdjunction_homEquiv_symm_apply (A : Rep.{max w u v} k S)
     {B : Rep.{max w u v} k G}
     (f : B ⟶ (indFunctor k S.subtype).obj A) :
     ((resIndAdjunction k S).homEquiv _ _).symm f =
-      (resCoindHomEquiv.{max w u v} S.subtype B A).symm (f ≫ (indCoindIso.{max w u v} A).hom) := by
+      (resCoindHomEquiv.{max w u v} S.subtype B A).symm (f ≫ (indCoindIso.{max w u v} A).hom) :=
   rfl
 
 variable (k S) in
@@ -248,7 +244,7 @@ theorem instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype :
 lemma coindResAdjunction_counit_app (B : Rep.{max w u v} k G) :
     (coindResAdjunction.{w, u, v} k S).counit.app B =
       (indCoindIso.{max w u v} (res S.subtype B)).inv ≫
-      (indResAdjunction k S.subtype).counit.app B := by
+      (indResAdjunction k S.subtype).counit.app B :=
   rfl
 
 set_option backward.isDefEq.respectTransparency false in
@@ -257,8 +253,7 @@ lemma coindResAdjunction_unit_app (A : Rep.{max w u v} k S) :
     (coindResAdjunction k S).unit.app A = (indResAdjunction k S.subtype).unit.app A ≫
       (resFunctor S.subtype).map (indCoindIso.{max w u v} A).hom := by
   ext
-  simp [coindResAdjunction, Adjunction.ofNatIsoLeft,
-    indResAdjunction, indCoindIso]
+  simp [coindResAdjunction]
 
 lemma coindResAdjunction_homEquiv_apply (A : Rep.{max w u v} k S)
     {B : Rep k G} (f : coind S.subtype A ⟶ B) :
@@ -270,9 +265,7 @@ lemma coindResAdjunction_homEquiv_symm_apply (A : Rep.{max w u v} k S)
     {B : Rep k G} (f : A ⟶ res S.subtype B) :
     ((coindResAdjunction.{max w u v} k S).homEquiv _ _).symm f =
       (indCoindIso.{max w u v} A).inv ≫ (indResHomEquiv S.subtype A B).symm f := by
-  simp only [coindResAdjunction, indResAdjunction,
+  simp [coindResAdjunction, indResHomEquiv, indResAdjunction,
     Adjunction.homEquiv_ofNatIsoLeft_symm_apply _]
-  simp
-  rfl
 
 end Rep

Mathlib/RepresentationTheory/Induced.lean

@@ -110,7 +110,7 @@ noncomputable def indMap {A B : Rep k G} (f : A ⟶ B) : ind φ A ⟶ ind φ B :
 variable (k) in
 /-- Given a group homomorphism `φ : G →* H`, this is the functor sending a `G`-representation `A`
 to the induced `H`-representation `ind φ A`, with action on maps induced by left tensoring. -/
-@[simps obj map]
+@[implicit_reducible, simps obj map]
 noncomputable def indFunctor : Rep.{w} k G ⥤ Rep k H where
   obj A := ind φ A
   map f := indMap φ f
@@ -152,8 +152,6 @@ noncomputable def indResHomEquiv (A : Rep.{max w v' u} k G) (B : Rep.{max w v' u
     simpa using (hom_comm_apply f h⁻¹ (IndV.mk φ A.ρ 1 a)).symm
   right_inv _ := by ext; simp
 
-set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 variable (k) in
 /-- Given a group homomorphism `φ : G →* H`, the induction functor `Rep k G ⥤ Rep k H` is left
 adjoint to the restriction functor along `φ`. -/

Mathlib/RepresentationTheory/Invariants.lean

@@ -246,7 +246,7 @@ abbrev quotientToInvariants : Rep k (G ⧸ S) := Rep.of (A.ρ.quotientToInvarian
 variable (k G)
 
 /-- The functor sending a representation to its submodule of invariants. -/
-@[simps! obj_carrier map_hom]
+@[implicit_reducible, simps! obj_carrier map_hom]
 noncomputable def invariantsFunctor : Rep.{w} k G ⥤ ModuleCat k where
   obj A := ModuleCat.of k A.ρ.invariants
   map {A B} f := ModuleCat.ofHom <| (f.hom ∘ₗ A.ρ.invariants.subtype).codRestrict
@@ -258,7 +258,6 @@ instance : (invariantsFunctor k G).PreservesZeroMorphisms where
 instance : (invariantsFunctor k G).Additive where
 instance : (invariantsFunctor k G).Linear k where
 
-set_option backward.isDefEq.respectTransparency false in
 variable {G} in
 /-- Given a normal subgroup S ≤ G, this is the functor sending a `G`-representation `A` to the
 `G ⧸ S`-representation it induces on `A^S`. -/

Mathlib/RepresentationTheory/Rep/Basic.lean

@@ -436,7 +436,7 @@ end setup
 
 variable (k G) in
 /-- The functor equipping a module with the trivial representation. -/
-@[simps! obj_V map_hom]
+@[implicit_reducible, simps! obj_V map_hom]
 def trivialFunctor : ModuleCat.{w} k ⥤ Rep.{w} k G where
   obj V := trivial k G V
   map f := ofHom ⟨f.hom, fun _ ↦ rfl⟩