chore(RepresentationTheory/Coinduced): more tech debt

Mathlib/RepresentationTheory/Coinduced.lean

@@ -69,7 +69,6 @@ def coindV : Submodule k (H → A) where
 lemma mem_coindV (f : H → A) : f ∈ coindV φ σ ↔ ∀ (g : G) (h : H), f (φ g * h) = σ g (f h) :=
   Iff.rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
 /--
 If `ρ : Representation k G A` and `φ : G →* H` then `coind φ ρ` is the representation
 coinduced by `ρ` along `φ`, defined as the following action of `H` on the submodule `coindV φ ρ`
@@ -78,14 +77,17 @@ to the function sending `h₁` to `f (h₁ * h)`.
 
 See also `Rep.coind` and `Representation.coind'` for variants involving the category `Rep k G`.
 -/
-@[simps]
+@[simps -isSimp]
 def coind : Representation k H (coindV φ ρ) where
-  toFun h := (LinearMap.funLeft _ _ (· * h)).restrict fun x hx g h₁ => by
-    simpa [mul_assoc] using hx g (h₁ * h)
+  toFun h := (LinearMap.funLeft _ _ (· * h)).restrict fun x hx => (mem_coindV φ ρ _).mpr <| by
+    simp [(mem_coindV φ ρ _).mp hx, mul_assoc]
   map_one' := by ext; simp
   map_mul' _ _ := by ext; simp [mul_assoc]
 
-set_option backward.isDefEq.respectTransparency.types false in
+@[simp]
+lemma coind_apply_apply (h x : H) (f : coindV φ ρ) :
+    (coind φ ρ h f).val x = f.val (x * h) := rfl
+
 variable {σ ρ} in
 /-- Given a monoid homomorphism `φ : G →* H` and an intertwining map `f : σ ⟶ ρ`, there is a
   natural intertwining map `coind φ σ ⟶ coind φ ρ` given by postcomposition by `f`. -/
@@ -187,7 +189,7 @@ variable {A} in
 @[ext]
 lemma coind'_ext {f g : coind' φ A} (hfg : ∀ h, f.hom.toLinearMap (.single h 1) =
     g.hom.toLinearMap (.single h 1)) : f = g :=
-  Rep.hom_ext <| by ext1; dsimp; ext h; simpa using hfg h
+  Rep.hom_ext <| by ext h; simpa using hfg h
 
 /-- Given a monoid morphism `φ : G →* H` and a morphism of `G`-representations `f : A ⟶ B`, there
 is a natural `H`-representation morphism `coind' φ A ⟶ coind' φ B`, given by postcomposition
@@ -224,7 +226,6 @@ noncomputable def coindVEquiv :
   left_inv x := by simp
   right_inv x := coind'_ext φ fun _ => by simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- `coind φ A` and `coind' φ A` are isomorphic representations, with the underlying
 `k`-linear equivalence given by `coindVEquiv`. -/
 noncomputable def coindIso : coind φ A ≅ coind' φ A :=
@@ -243,68 +244,62 @@ end CoindIso
 
 noncomputable section Adjunction
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- The morphism induced by the adjunction between `res φ` and `coind φ` sending a morphism
   `f : res φ B ⟶ A` to the morphism `B ⟶ coind φ A` given by the underlying linear map sending
   `b : B.V` to the function sending `h : H` to `f ((B.ρ h) b)`. -/
 def resCoindToHom (B : Rep k H) (A : Rep k G) (f : res φ B ⟶ A) : B ⟶ (coind φ A) :=
-  Rep.ofHom ⟨(LinearMap.pi fun h => f.hom.toLinearMap ∘ₗ
-    Rep.ρ B h).codRestrict _ fun _ _ _ => by simpa using hom_comm_apply f _ _, fun g ↦ by
-    dsimp; ext; simp⟩
-
-@[simp]
-lemma resCoindToHom_hom_apply_coe (B : Rep k H) (A : Rep k G) (f : res φ B ⟶ A) (c : ↑B.V)
-    (i : H) : (DFunLike.coe (F := no_index (_)) (resCoindToHom φ B A f).hom c).1 i =
-    (Hom.hom f) ((B.ρ i) c) := rfl
-
--- this `no_index` is to prevent simp discrimination tree from acting weird, i.e before
--- adding it the discrimination tree looks like: _.1 (@DFunLike.coe
--- (@Representation.IntertwiningMap _ _ _.1 (@Rep.mk✝ ..).1 ..)) which is bad because `Rep.mk` is
--- private and should never be used.
+  Rep.ofHom ⟨(LinearMap.pi fun h => f.hom.toLinearMap ∘ₗ Rep.ρ B h).codRestrict _ fun b =>
+    (Representation.mem_coindV φ A.ρ _).mpr <| fun g h => by
+      simpa using hom_comm_apply f g ((B.ρ h) b), fun _ ↦ by ext; simp⟩
 
-/--
-info: _.1 (@DFunLike.coe _ _.1 _ _ (@ConcreteCategory.hom (Rep _ _ _ _) _ _ _ _ _ _ _ (@resCoindToHom _ _ _ _ _ _ _ _ _ _)) _)
--/
-#guard_msgs in
-#discr_tree_simp_key resCoindToHom_hom_apply_coe
+lemma resCoindToHom_hom_apply_coe {B : Rep k H} {A : Rep k G} (f : res φ B ⟶ A) (c : ↑B.V)
+    (i : H) :
+    ((resCoindToHom φ B A f).hom c).1 i = (Hom.hom f) ((B.ρ i) c) := rfl
 
 attribute [pp_with_univ] Rep coind
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Given a monoid homomorphism `φ : G →* H`, an `H`-representation `B`, and a `G`-representation
 `A`, there is a `k`-linear equivalence between the `G`-representation morphisms `res φ B ⟶ A` and
 the `H`-representation morphisms `B ⟶ coind φ A`.
 
 Note `Rep.resCoindHomEquiv.{t, u, v, w}` has the property that
 even with all inputs explicitly given, the first universe cannot be synthesized.
 -/
-@[simps, pp_with_univ]
+@[simps -isSimp, pp_with_univ]
 def resCoindHomEquiv (B : Rep.{max w t} k H) (A : Rep.{max w t} k G) :
     (res φ B ⟶ A) ≃ₗ[k] (B ⟶ coind φ A) where
   toFun f := resCoindToHom φ B A f
-  map_add' _ _ := rfl
-  map_smul' _ _ := rfl
+  map_add' _ _ := by apply Rep.hom_ext; ext; rfl
+  map_smul' _ _ := by apply Rep.hom_ext; ext; rfl
   invFun f := Rep.ofHom ⟨LinearMap.proj 1 ∘ₗ (A.ρ.coindV φ).subtype ∘ₗ f.hom.toLinearMap,
     fun g => by
       ext x
       have := ((f.hom x).2 g 1).symm
       have := hom_comm_apply f (φ g) x
       simp_all⟩
-  left_inv x := by ext; simp
-  right_inv z := by ext; simp [resCoindToHom, hom_comm_apply z]
+  left_inv x := by ext; simp [resCoindToHom_hom_apply_coe φ]
+  right_inv z := by ext; simp [resCoindToHom_hom_apply_coe φ, hom_comm_apply z]
 
-#adaptation_note /-- After https://github.com/leanprover/lean4/pull/12179
-the simpNF linter complains about `@[simps! counit_app_hom_hom unit_app_hom_hom]`,
-but removing it seems to be harmless. -/
 variable (k) in
 /-- Given a monoid homomorphism `φ : G →* H`, the coinduction functor `Rep k G ⥤ Rep k H` is right
 adjoint to the restriction functor along `φ`. -/
-noncomputable abbrev resCoindAdjunction : resFunctor.{max w t} φ ⊣ coindFunctor k φ :=
+@[simps! unit_app_hom_toFun_coe]
+noncomputable def resCoindAdjunction : resFunctor.{max w t} φ ⊣ coindFunctor k φ :=
   Adjunction.mkOfHomEquiv {
     homEquiv X Y := (resCoindHomEquiv φ X Y).toEquiv
     homEquiv_naturality_left_symm := by intros; rfl
     homEquiv_naturality_right := by intros; ext; rfl }
 
+@[simp]
+lemma resCoindAdjunction_counit_app_hom_toFun (Y : Rep.{max w t, u, v} k G) (x : coind φ Y) :
+    (Hom.hom (A := of ((Representation.coind φ Y.ρ).comp φ)) (B := Y)
+      ((resCoindAdjunction k φ).counit.app Y)) x = x.val 1 := by
+  simp [resCoindAdjunction, resCoindHomEquiv_symm_apply _]
+
+@[simp]
+lemma resCoindAdjunction_homEquiv (B : Rep.{max w t} k H) (A : Rep.{max w t} k G) :
+    (resCoindAdjunction k φ).homEquiv B A = (resCoindHomEquiv φ B A).toEquiv := rfl
+
 noncomputable instance : (coindFunctor.{max w t} k φ).IsRightAdjoint :=
   (resCoindAdjunction k φ).isRightAdjoint
 

Mathlib/RepresentationTheory/FiniteIndex.lean

@@ -224,7 +224,7 @@ lemma resIndAdjunction_homEquiv_apply (A : Rep.{max w u v} k S)
     (resIndAdjunction.{w, u, v} k S).homEquiv _ _ f =
       resCoindHomEquiv.{max w u v} S.subtype B A f ≫ (indCoindIso.{max w u v} A).inv := by
   rw [resIndAdjunction, Adjunction.homEquiv_ofNatIsoRight_apply]
-  simp [resCoindHomEquiv]
+  simp
 
 lemma resIndAdjunction_homEquiv_symm_apply (A : Rep.{max w u v} k S)
     {B : Rep.{max w u v} k G}

Mathlib/RepresentationTheory/Homological/GroupCohomology/Shapiro.lean

@@ -52,7 +52,8 @@ noncomputable def linearYonedaObjResProjectiveResolutionIso
   HomologicalComplex.Hom.isoOfComponents
     (fun _ ↦ (resCoindHomEquiv.{u} _ _ _).toModuleIso) fun _ _ _ ↦
       ModuleCat.hom_ext (LinearMap.ext fun f => Rep.hom_ext <| by
-        ext; simp [← ModuleCat.ofHom_comp, resCoindHomEquiv, hom_comm_apply])
+        ext; simp [← ModuleCat.ofHom_comp, resCoindHomEquiv_apply _, resCoindToHom_hom_apply_coe _,
+          hom_comm_apply])
 
 /-- Shapiro's lemma: given a subgroup `S ≤ G` and an `S`-representation `A`, we have
 `Hⁿ(G, Coind_S^G(A)) ≅ Hⁿ(S, A).` -/