From 1f74fca91b138a932fa34b5c1d2a5fb66e079c5e Mon Sep 17 00:00:00 2001
From: JX-Mo <jiaximo1998@163.com>
Date: Fri, 18 Sep 2026 23:47:06 +0800
Subject: [PATCH 01/11] Refactor Induced representation definitions

---
 Mathlib/RepresentationTheory/Induced.lean | 171 +++++++++++++---------
 1 file changed, 104 insertions(+), 67 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Induced.lean b/Mathlib/RepresentationTheory/Induced.lean
index 118a2032daaa24..35656d86e632a0 100644
--- a/Mathlib/RepresentationTheory/Induced.lean
+++ b/Mathlib/RepresentationTheory/Induced.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Amelia Livingston. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Amelia Livingston
+Authors: Amelia Livingston, Jiaxi Mo
 -/
 module
 
@@ -50,18 +50,23 @@ universe t w w' u u' v v'
 namespace Representation
 
 variable {k G H : Type*} [CommRing k] [Group G] [Group H] (φ : G →* H) {A B : Type*}
-  [AddCommGroup A] [Module k A] (ρ : Representation k G A)
-  [AddCommGroup B] [Module k B]
+  [AddCommGroup A] [Module k A] [AddCommGroup B] [Module k B] (ρ : Representation k G A)
 
 /-- Given a group homomorphism `φ : G →* H` and a `G`-representation `(A, ρ)`, this is the
 `k`-module `(k[H] ⊗[k] A)_G` with the `G`-representation on `k[H]` defined by `φ`.
 See `Representation.ind` for the induced `H`-representation on `IndV φ ρ`. -/
-abbrev IndV := Coinvariants (V := TensorProduct k k[H] A)
-  (Representation.tprod ((leftRegular k H).comp φ) ρ)
+@[implicit_reducible]
+def IndV := Coinvariants (Representation.tprod ((leftRegular k H).comp φ) ρ)
+
+noncomputable instance : AddCommGroup (IndV φ ρ) := inferInstanceAs <|
+  AddCommGroup (Coinvariants (Representation.tprod ((leftRegular k H).comp φ) ρ))
+
+noncomputable instance : Module k (IndV φ ρ) := inferInstanceAs <|
+  Module k (Coinvariants (Representation.tprod ((leftRegular k H).comp φ) ρ))
 
 /-- Given a group homomorphism `φ : G →* H` and a `G`-representation `(A, ρ)`, this is the
 `H → A →ₗ[k] (k[H] ⊗[k] A)_G` sending `h, a` to `⟦h ⊗ₜ a⟧`. -/
-noncomputable abbrev IndV.mk (h : H) : A →ₗ[k] IndV φ ρ :=
+noncomputable def IndV.mk (h : H) : A →ₗ[k] IndV φ ρ :=
   Coinvariants.mk _ ∘ₗ TensorProduct.mk k _ _ (.single h 1)
 
 @[ext]
@@ -70,26 +75,86 @@ lemma IndV.hom_ext {f g : IndV φ ρ →ₗ[k] B}
   Coinvariants.hom_ext <| TensorProduct.ext <| MonoidAlgebra.lhom_ext' fun h =>
     LinearMap.ext_ring <| hfg h
 
+variable {φ ρ} in
+@[elab_as_elim]
+lemma IndV.inductionOn {p : IndV φ ρ → Prop} (v : IndV φ ρ) (mk : ∀ h a, p (IndV.mk φ ρ h a))
+    (add : ∀ x y : IndV φ ρ, p x → p y → p (x + y)) : p v := by
+  refine Representation.Coinvariants.induction_on v fun w => ?_
+  refine w.inductionOn (fun m a => ?_) (fun _ _ hx hy => by simpa [map_add] using add _ _ hx hy)
+  refine MonoidAlgebra.induction_linear m (by simpa using mk 1 0) ?_ ?_
+  · exact fun _ _ hx hy => by simpa [TensorProduct.add_tmul, map_add] using add _ _ hx hy
+  · intro h r
+    rw [← mul_one r, ← MonoidAlgebra.smul_single', TensorProduct.smul_tmul]
+    exact mk h (r • a)
+
+@[simp]
+lemma IndV.mk_map_mul (g : G) (h : H) (a : A) :
+    IndV.mk φ ρ ((φ g) * h) a = IndV.mk φ ρ h (ρ g⁻¹ a) := by
+  simp [mk, Coinvariants.mk_tmul_inv (g := g)]
+
+@[simp]
+lemma IndV.mk_map_inv_mul (g : G) (h : H) (a : A) :
+    IndV.mk φ ρ ((φ g)⁻¹ * h) a = IndV.mk φ ρ h (ρ g a) := by
+  simp [← map_inv]
+
+@[simp]
+lemma IndV.mk_map_eq (g : G) (a : A) :
+    IndV.mk φ ρ (φ g) a = IndV.mk φ ρ 1 (ρ g⁻¹ a) := by
+  simpa using IndV.mk_map_mul φ ρ g 1 a
+
+@[simp]
+lemma IndV.mk_map_inv_eq (g : G) (a : A) :
+    IndV.mk φ ρ (φ g)⁻¹ a = IndV.mk φ ρ 1 (ρ g a) := by
+  simp [← map_inv]
+
+/-- Construct a linear map `IndV φ ρ →ₗ[k] B` from a compatible family of linear maps
+`f : H → A →ₗ[k] B`, whose composition with `IndV.mk φ ρ h : A →ₗ[k] IndV φ ρ` is `f h`. -/
+noncomputable def IndV.lift (f : H → A →ₗ[k] B)
+    (hf : ∀ (g : G) (h : H) (a : A), f (φ g * h) a = f h (ρ g⁻¹ a)) :
+    IndV φ ρ →ₗ[k] B :=
+  Coinvariants.lift _ (TensorProduct.lift <| (Finsupp.lift _ _ _ fun h => f h) ∘ₗ
+    (MonoidAlgebra.coeffLinearEquiv k).toLinearMap) fun g => by ext; simp [hf]
+
+@[simp]
+lemma IndV.lift_apply_mk (f : H → A →ₗ[k] B) (h : H) (a : A)
+    (hf : ∀ (g : G) (h : H) (a : A), f (φ g * h) a = f h (ρ g⁻¹ a)) :
+    lift φ ρ f hf (mk φ ρ h a) = f h a := by
+  simp [lift, mk, Coinvariants.lift_mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)]
+
 /-- Given a group homomorphism `φ : G →* H` and a `G`-representation `A`, this is
 `(k[H] ⊗[k] A)_G` equipped with the `H`-representation defined by sending `h : H` and `⟦h₁ ⊗ₜ a⟧`
 to `⟦h₁h⁻¹ ⊗ₜ a⟧`. -/
-@[simps]
 noncomputable def ind : Representation k H (IndV φ ρ) where
-  toFun h :=
-    Coinvariants.map _ _ ⟨(MonoidAlgebra.mapDomainLinearMap k k fun x => x * h⁻¹).rTensor _,
-    fun _ => by ext; simp [mul_assoc]⟩
+  toFun h := IndV.lift φ ρ (fun x => IndV.mk φ ρ (x * h⁻¹)) (by simp [mul_assoc])
   map_one' := by ext; simp
-  map_mul' _ _ := by ext; simp [IndV, mul_assoc]
+  map_mul' _ _ := by ext; simp [mul_assoc]
 
-lemma ind_mk (h₁ h₂ : H) (a : A) :
+@[simp]
+lemma ind_apply_mk (h₁ h₂ : H) (a : A) :
     ind φ ρ h₁ (IndV.mk _ _ h₂ a) = IndV.mk _ _ (h₂ * h₁⁻¹) a := by
+  simp [ind]
+
+lemma ind_conj_map_apply (g : G) (h : H) (a : A) :
+    ind φ ρ (h⁻¹ * (φ g) * h) (IndV.mk _ _ h a) = IndV.mk _ _ h (ρ g a) := by
   simp
 
+variable {ρ} in
+/-- Construct an `IntertwiningMap` starting from an induced representation by lifting an
+`IntertwiningMap` with a `res` representation as target. -/
+noncomputable def ind.lift {σ : Representation k H B} (f : IntertwiningMap ρ (σ.comp φ)) :
+    (ind φ ρ).IntertwiningMap σ :=
+  ⟨IndV.lift φ ρ (fun h => σ h⁻¹ ∘ₗ f) (by simp [f.isIntertwining]), fun g => by ext; simp⟩
+
+@[simp]
+lemma ind.lift_apply {σ : Representation k H B} (f : IntertwiningMap ρ (σ.comp φ)) (h : H) (a : A) :
+    ind.lift φ f (IndV.mk φ ρ h a) = σ h⁻¹ (f a) := by
+  simp [ind.lift]
+
 end Representation
 
 namespace Rep
 
-open CategoryTheory Finsupp
+open CategoryTheory Finsupp Representation
 
 variable {k : Type u} {G : Type v} {H : Type v'} [CommRing k] [Group G] [Group H] (φ : G →* H)
   (A : Rep.{w} k G)
@@ -103,10 +168,8 @@ noncomputable abbrev ind : Rep k H := Rep.of (A.ρ.ind φ)
 
 /-- Given a group homomorphism `φ : G →* H`, a morphism of `G`-representations `f : A ⟶ B` induces
 a morphism of `H`-representations `(k[H] ⊗[k] A)_G ⟶ (k[H] ⊗[k] B)_G`. -/
-noncomputable def indMap {A B : Rep k G} (f : A ⟶ B) : ind φ A ⟶ ind φ B := Rep.ofHom
-  ⟨Representation.Coinvariants.map _ _ ⟨f.hom.toLinearMap.lTensor _, by
-    simp [LinearMap.lTensor_comp_map, f.hom.2, LinearMap.map_comp_lTensor]⟩,
-    fun g ↦ by ext; simp⟩
+noncomputable abbrev indMap {A B : Rep k G} (f : A ⟶ B) : ind φ A ⟶ ind φ B := Rep.ofHom <|
+  ind.lift φ ⟨IndV.mk φ B.ρ 1 ∘ₗ f.hom, fun g => by ext; simp [IntertwiningMap.isIntertwining]⟩
 
 variable (k) in
 /-- Given a group homomorphism `φ : G →* H`, this is the functor sending a `G`-representation `A`
@@ -115,8 +178,8 @@ to the induced `H`-representation `ind φ A`, with action on maps induced by lef
 noncomputable def indFunctor : Rep.{w} k G ⥤ Rep k H where
   obj A := ind φ A
   map f := indMap φ f
-  map_id _ := by ext; rfl
-  map_comp _ _ := by ext; rfl
+  map_id _ := by ext; simp
+  map_comp _ _ := by ext; simp
 
 end Ind
 section Adjunction
@@ -127,38 +190,26 @@ variable (B : Rep k H)
 
 /-- Given a group homomorphism `φ : G →* H`, an `H`-representation `B`, and a `G`-representation
 `A`, there is a `k`-linear equivalence between the `H`-representation morphisms `ind φ A ⟶ B` and
-the `G`-representation morphisms `A ⟶ B`. -/
+the `G`-representation morphisms `A ⟶ res B`. -/
 @[simps]
 noncomputable def indResHomEquiv (A : Rep.{max w v' u} k G) (B : Rep.{max w v' u} k H) :
     (ind φ A ⟶ B) ≃ₗ[k] (A ⟶ res φ B) where
-  toFun f := Rep.ofHom ⟨f.hom.toLinearMap ∘ₗ IndV.mk φ A.ρ 1, fun g ↦ by
-    ext x
-    have := (hom_comm_apply f (φ g) (IndV.mk φ A.ρ 1 x)).symm
-    simp_all [← Coinvariants.mk_inv_tmul] ⟩
+  toFun f := Rep.ofHom
+    ⟨f.hom.toLinearMap ∘ₗ IndV.mk φ A.ρ 1, fun g => by ext; simp [← f.hom.isIntertwining]⟩
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
-  invFun f := Rep.ofHom ⟨Representation.Coinvariants.lift _
-    (TensorProduct.lift <| (Finsupp.lift _ _ _ fun h => B.ρ h⁻¹ ∘ₗ f.hom.toLinearMap) ∘ₗ
-      (MonoidAlgebra.coeffLinearEquiv k).toLinearMap)
-    fun g ↦ by
-      ext h x
-      simp only [LinearMap.coe_comp, Function.comp_apply, MonoidAlgebra.lsingle_apply]
-      simp [ofMulAction_single, mul_inv_rev, hom_comm_apply f g], fun g ↦ by ext; simp⟩
-  left_inv f := by
-    ext h a
-    simpa using (hom_comm_apply f h⁻¹ (IndV.mk φ A.ρ 1 a)).symm
+  invFun f := Rep.ofHom (Representation.ind.lift φ f.hom)
+  left_inv f := by ext; simp [← f.hom.isIntertwining]
   right_inv _ := by ext; simp
 
 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 `φ`. -/
 noncomputable def indResAdjunction : indFunctor k φ ⊣ resFunctor.{max w v' u} φ :=
-  Adjunction.mkOfHomEquiv {
-    homEquiv A B := (indResHomEquiv φ A B).toEquiv
-    homEquiv_naturality_left_symm _ _ := by
-      change (indResHomEquiv φ _ _).symm (_ ≫ _) = _
-      ext; simp [indMap, indResHomEquiv]
-    homEquiv_naturality_right := by intros; rfl }
+  Adjunction.mkOfHomEquiv
+    { homEquiv A B := (indResHomEquiv φ A B).toEquiv
+      homEquiv_naturality_left_symm _ _ := by rw [Equiv.symm_apply_eq]; ext; simp [indResHomEquiv]
+      homEquiv_naturality_right _ _ := by ext; simp }
 
 noncomputable instance : (indFunctor.{max u v' w} k φ).IsLeftAdjoint :=
   (indResAdjunction k φ).isLeftAdjoint
@@ -168,38 +219,30 @@ noncomputable instance : (resFunctor.{max u v' w} (k := k) φ).IsRightAdjoint :=
 
 end Adjunction
 
-section
-
 variable {G H : Type u} [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H)
 
 open Representation
 
-set_option backward.defeqAttrib.useBackward true in
 /-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear map
 `(Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G` sending `⟦h ⊗ₜ a⟧ ⊗ₜ b` to `⟦a ⊗ ρ(h)(b)⟧` for all
 `h : H`, `a : A`, and `b : B`. -/
 noncomputable def coinvariantsTensorIndHom :
     ((coinvariantsTensor k H).obj (ind φ A)).obj B ⟶
       ((coinvariantsTensor k G).obj A).obj (res φ B) :=
-  ModuleCat.ofHom <| Coinvariants.lift _ (TensorProduct.lift <| Coinvariants.lift _
-    (TensorProduct.lift <| (Finsupp.lift _ _ _ <| fun g ↦
-      (coinvariantsTensorMk A (res φ B)).compl₂ (B.ρ g)) ∘ₗ
-      (MonoidAlgebra.coeffLinearEquiv k).toLinearMap)
-      fun g ↦ by ext; simpa [coinvariantsTensorMk, Coinvariants.mk_eq_iff]
-        using! Coinvariants.sub_mem_ker _ _) fun _ ↦ by
-    simp only [MonoidalCategory.curriedTensor_obj_obj, tensor_V, tensor_ρ, res_obj_ρ,
-      Functor.postcompose₂_obj_obj_obj_obj, coinvariantsFunctor_obj_carrier,
-      tprod_apply, ind_apply]
-    ext; simp
-
-set_option backward.defeqAttrib.useBackward true in
+  ModuleCat.ofHom <| Coinvariants.lift _
+    (TensorProduct.lift <| IndV.lift φ A.ρ
+      (fun h => (coinvariantsTensorMk A (res φ B)).compl₂ (B.ρ h))
+      (fun g h a => by ext; simp [coinvariantsTensorMk]))
+    (fun h => by
+        simp only [MonoidalCategory.curriedTensor_obj_obj, tensor_V]
+        ext; simp)
+
 variable {A B} in
 lemma coinvariantsTensorIndHom_mk_tmul_indVMk (h : H) (x : A) (y : B) :
     coinvariantsTensorIndHom φ A B (coinvariantsTensorMk _ _ (IndV.mk φ _ h x) y) =
       coinvariantsTensorMk _ _ x (B.ρ h y) := by
   simp [coinvariantsTensorIndHom, coinvariantsTensorMk]
 
-set_option backward.defeqAttrib.useBackward true in
 /-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear map
 `(A ⊗ Res(φ)(B))_G ⟶ (Ind(φ)(A) ⊗ B))_H` sending `⟦a ⊗ₜ b⟧` to `⟦1 ⊗ₜ a⟧ ⊗ₜ b` for all
 `a : A`, and `b : B`. -/
@@ -208,14 +251,11 @@ noncomputable def coinvariantsTensorIndInv :
       ((coinvariantsTensor k H).obj (ind φ A)).obj B :=
   ModuleCat.ofHom <| Coinvariants.lift _ (TensorProduct.lift <|
     (coinvariantsTensorMk (ind (k := k) φ A) B) ∘ₗ IndV.mk _ _ 1) fun s ↦ by
-    simp only [MonoidalCategory.curriedTensor_obj_obj, tensor_V, tensor_ρ, tprod_apply,
-      MonoidHom.coe_comp, Function.comp_apply]
-    ext x y
-    simpa [Coinvariants.mk_eq_iff, coinvariantsTensorMk] using
-      Coinvariants.mem_ker_of_eq (φ s) (IndV.mk φ A.ρ (1 : H) x ⊗ₜ[k] y) _ <| by
-      simp [← Coinvariants.mk_inv_tmul]
-
-set_option backward.defeqAttrib.useBackward true in
+      simp only [MonoidalCategory.curriedTensor_obj_obj, tensor_V]
+      ext x y
+      simpa [coinvariantsTensorMk, Coinvariants.mk_eq_iff] using Coinvariants.mem_ker_of_eq (φ s)
+        ((IndV.mk φ A.ρ (1 : H) x) ⊗ₜ[k] y) _ (by simp)
+
 variable {A B} in
 lemma coinvariantsTensorIndInv_mk_tmul_indMk (x : A) (y : B) :
     coinvariantsTensorIndInv φ A B (Coinvariants.mk
@@ -223,7 +263,6 @@ lemma coinvariantsTensorIndInv_mk_tmul_indMk (x : A) (y : B) :
       coinvariantsTensorMk _ _ (IndV.mk φ _ 1 x) y := by
   simp [coinvariantsTensorIndInv, coinvariantsTensorMk]
 
-set_option backward.defeqAttrib.useBackward true in
 /-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear
 isomorphism `(Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G` sending `⟦h ⊗ₜ a⟧ ⊗ₜ b` to `⟦a ⊗ ρ(h)(b)⟧`
 for all `h : H`, `a : A`, and `b : B`. -/
@@ -242,7 +281,6 @@ noncomputable def coinvariantsTensorIndIso :
     ext
     simp [coinvariantsTensorIndInv, coinvariantsTensorMk, coinvariantsTensorIndHom]
 
-set_option backward.defeqAttrib.useBackward true in
 /-- Given a group hom `φ : G →* H` and `A : Rep k G`, the functor `Rep k H ⥤ ModuleCat k` sending
 `B ↦ (Ind(φ)(A) ⊗ B))_H` is naturally isomorphic to the one sending `B ↦ (A ⊗ Res(φ)(B))_G`. -/
 @[simps! hom_app inv_app]
@@ -252,5 +290,4 @@ noncomputable def coinvariantsTensorIndNatIso :
     ext
     simp [coinvariantsTensorIndHom, coinvariantsTensorMk, hom_comm_apply]
 
-end
 end Rep

From 27dd14e8726d18d8bb34ca3cb5047a148f2e8da7 Mon Sep 17 00:00:00 2001
From: JX-Mo <jiaximo1998@163.com>
Date: Fri, 18 Sep 2026 23:47:37 +0800
Subject: [PATCH 02/11] fix proof in FiniteIndex

---
 Mathlib/RepresentationTheory/FiniteIndex.lean | 43 +++++++++----------
 1 file changed, 21 insertions(+), 22 deletions(-)

diff --git a/Mathlib/RepresentationTheory/FiniteIndex.lean b/Mathlib/RepresentationTheory/FiniteIndex.lean
index 30fe13f399eccc..ec432f7f851809 100644
--- a/Mathlib/RepresentationTheory/FiniteIndex.lean
+++ b/Mathlib/RepresentationTheory/FiniteIndex.lean
@@ -70,13 +70,13 @@ lemma indToCoindAux_mul_snd (g g₁ : G) (a : A) (s : S) :
 
 @[simp]
 lemma indToCoindAux_mul_fst (g₁ g₂ : G) (a : A) (s : S) :
-     indToCoindAux A (s * g₁) (A.ρ s a) g₂ = indToCoindAux A g₁ a g₂ := by
+     indToCoindAux A (s * g₁) a g₂ = indToCoindAux A g₁ (A.ρ s⁻¹ a) g₂ := by
   rcases em ((QuotientGroup.rightRel S).r g₂ g₁) with ⟨s₁, rfl⟩ | h
-  · simp only [indToCoindAux, LinearMap.pi_apply]
+  · simp only [indToCoindAux, mul_inv_rev, LinearMap.pi_apply]
     rw [dite_eq_left ⟨s₁ * s⁻¹, by simp [S.1.smul_def, smul_eq_mul, mul_assoc]⟩,
       dite_eq_left ⟨s₁, rfl⟩, ← Module.End.mul_apply, ← map_mul]
-    congr
-    simp [Subtype.ext_iff, S.1.smul_def, mul_assoc]
+    congr 2
+    simp [Subtype.ext_iff, S.1.smul_def]
   · rw [indToCoindAux_of_not_rel (h := h), indToCoindAux_of_not_rel]
     exact mt (fun ⟨s₁, hs₁⟩ => ⟨s₁ * s, by simp_all [S.1.smul_def, mul_assoc]⟩) h
 
@@ -99,15 +99,18 @@ lemma indToCoindAux_comm {A B : Rep k S} (f : A ⟶ B) (g₁ g₂ : G) (a : A) :
   · simp [S.1.smul_def, hom_comm_apply]
   · simp [indToCoindAux_of_not_rel (h := h)]
 
-set_option backward.isDefEq.respectTransparency.types false in
 variable (A) in
 /-- Let `S ≤ G` be a subgroup and `A` a `k`-linear `S`-representation. This is the `k`-linear map
 `Ind_S^G(A) →ₗ[k] Coind_S^G(A)` sending `(⟦g ⊗ₜ[k] a⟧, sg) ↦ ρ(s)(a)`. -/
-noncomputable abbrev indToCoind :
+noncomputable def indToCoind :
     ind S.subtype A →ₗ[k] coind S.subtype A :=
-  Representation.Coinvariants.lift _ (TensorProduct.lift <| (linearCombination _ fun g =>
-    LinearMap.codRestrict _ (indToCoindAux A g) fun _ _ _ => by simp) ∘ₗ
-    (MonoidAlgebra.coeffLinearEquiv k).toLinearMap) fun _ => by ext; simp
+  Representation.IndV.lift S.subtype A.ρ
+    (fun g => LinearMap.codRestrict _ (indToCoindAux A g) (by simp)) (by intros; ext; simp)
+
+lemma indToCoind_mk (g : G) (a : A) :
+    indToCoind A (IndV.mk S.subtype A.ρ g a) = indToCoindAux A g a := by
+  ext
+  simp [indToCoind]
 
 variable [S.FiniteIndex]
 
@@ -145,31 +148,27 @@ lemma coindToInd_of_support_subset_orbit (g : G) (f : coind S.subtype A)
 
 variable (A)
 
-set_option backward.isDefEq.respectTransparency.types false in
 lemma coindToInd_indToCoind : A.indToCoind ∘ₗ A.coindToInd = LinearMap.id := by
   ext g a
   simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq]
   conv_lhs => rw [coindToInd_apply]
   simp only [map_sum, AddSubmonoidClass.coe_finsetSum, Finset.sum_apply]
   rw [Finset.sum_eq_single ⟦a⟧]
-  · simp
+  · simp [indToCoind_mk _]
   · intro b _ hb
     induction b using Quotient.inductionOn with | h b =>
-    simpa using indToCoindAux_of_not_rel b a (g.1 b) (mt Quotient.sound hb.symm)
+    simpa [indToCoind_mk _] using indToCoindAux_of_not_rel b a (g.1 b) (mt Quotient.sound hb.symm)
   · simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 lemma indToCoind_coindToInd : A.coindToInd ∘ₗ A.indToCoind = LinearMap.id := by
   ext g a
-  simp only [LinearMap.comp_apply, AlgebraTensorModule.curry_apply,
-    TensorProduct.curry_apply, LinearMap.coe_restrictScalars, LinearMap.id_apply]
+  simp only [LinearMap.comp_apply, LinearMap.id_apply]
   rw [coindToInd_of_support_subset_orbit g]
-  · simp
+  · simp [indToCoind_mk _]
   · intro x hx
     contrapose hx
-    simpa using indToCoindAux_of_not_rel g x a hx
+    simpa [indToCoind_mk _] using indToCoindAux_of_not_rel g x a hx
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Let `S ≤ G` be a finite index subgroup, `g₁, ..., gₙ` a set of right coset representatives of
 `S`, and `A` a `k`-linear `S`-representation. This is an isomorphism `Ind_S^G(A) ≅ Coind_S^G(A)`.
 The forward map sends `(⟦g ⊗ₜ[k] a⟧, sg) ↦ ρ(s)(a)`, and the inverse sends `f : G → A` to
@@ -177,12 +176,12 @@ The forward map sends `(⟦g ⊗ₜ[k] a⟧, sg) ↦ ρ(s)(a)`, and the inverse
 @[simps! hom_hom_toLinearMap inv_hom_toLinearMap]
 noncomputable def indCoindIso (A : Rep.{max w u} k S) :
     ind S.subtype A ≅ coind S.subtype A :=
-  mkIso (.mk (.ofLinearMap (indToCoind A) (coindToInd A)
-    (coindToInd_indToCoind A) (indToCoind_coindToInd A)) <| fun g ↦ by ext; simp)
+  mkIso (.mk (.ofLinearMap _ _ (coindToInd_indToCoind A) (indToCoind_coindToInd A)) fun g ↦ by
+    ext h
+    simp [indToCoind_mk _])
 
 variable (k S)
 
-set_option backward.isDefEq.respectTransparency.types false 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`. -/
 @[implicit_reducible, simps! hom_app inv_app]
@@ -191,7 +190,7 @@ noncomputable def indCoindNatIso :
   NatIso.ofComponents (fun (A : Rep k S) => indCoindIso A) fun f => by
     simp only [indFunctor_obj, coindFunctor_obj];
     ext g1 x g2
-    simp [indToCoind, indMap, indToCoindAux_comm]
+    simp [indToCoind, indToCoindAux_comm]
 
 /-- Given a finite index subgroup `S ≤ G`, `Ind_S^G` is right adjoint to the restriction functor
 `Res k G ⥤ Res k S`, since it is naturally isomorphic to `Coind_S^G`. -/

From d1596c3d029bde20ce700845c8f44418cb9b3196 Mon Sep 17 00:00:00 2001
From: JX-Mo <jiaximo1998@163.com>
Date: Fri, 18 Sep 2026 23:48:20 +0800
Subject: [PATCH 03/11] update

---
 Mathlib/RepresentationTheory/Coinduced.lean | 23 ++++++++++-----------
 1 file changed, 11 insertions(+), 12 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Coinduced.lean b/Mathlib/RepresentationTheory/Coinduced.lean
index 6ecfd42b7283c0..58c423043f079e 100644
--- a/Mathlib/RepresentationTheory/Coinduced.lean
+++ b/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,14 +244,13 @@ 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⟩
+  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⟩
 
 @[simp]
 lemma resCoindToHom_hom_apply_coe (B : Rep k H) (A : Rep k G) (f : res φ B ⟶ A) (c : ↑B.V)
@@ -270,7 +270,6 @@ info: _.1 (@DFunLike.coe _ _.1 _ _ (@ConcreteCategory.hom (Rep _ _ _ _) _ _ _ _
 
 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`.

From 8505af54824133744a9147dd3b53fa92e901ab18 Mon Sep 17 00:00:00 2001
From: JX-Mo <jiaximo1998@163.com>
Date: Sat, 19 Sep 2026 13:26:54 +0800
Subject: [PATCH 04/11] deprecation

---
 Mathlib/RepresentationTheory/Induced.lean | 44 ++++++++++++-----------
 1 file changed, 23 insertions(+), 21 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Induced.lean b/Mathlib/RepresentationTheory/Induced.lean
index 35656d86e632a0..41bedfad7d7021 100644
--- a/Mathlib/RepresentationTheory/Induced.lean
+++ b/Mathlib/RepresentationTheory/Induced.lean
@@ -43,7 +43,7 @@ is used to prove Shapiro's lemma in
 
 @[expose] public section
 
-open scoped MonoidAlgebra
+open scoped MonoidAlgebra Representation
 
 universe t w w' u u' v v'
 
@@ -124,6 +124,7 @@ lemma IndV.lift_apply_mk (f : H → A →ₗ[k] B) (h : H) (a : A)
 /-- Given a group homomorphism `φ : G →* H` and a `G`-representation `A`, this is
 `(k[H] ⊗[k] A)_G` equipped with the `H`-representation defined by sending `h : H` and `⟦h₁ ⊗ₜ a⟧`
 to `⟦h₁h⁻¹ ⊗ₜ a⟧`. -/
+@[simps -isSimp]
 noncomputable def ind : Representation k H (IndV φ ρ) where
   toFun h := IndV.lift φ ρ (fun x => IndV.mk φ ρ (x * h⁻¹)) (by simp [mul_assoc])
   map_one' := by ext; simp
@@ -134,19 +135,22 @@ lemma ind_apply_mk (h₁ h₂ : H) (a : A) :
     ind φ ρ h₁ (IndV.mk _ _ h₂ a) = IndV.mk _ _ (h₂ * h₁⁻¹) a := by
   simp [ind]
 
+@[deprecated (since := "2026-09-19")] alias ind_mk := ind_apply_mk
+
 lemma ind_conj_map_apply (g : G) (h : H) (a : A) :
     ind φ ρ (h⁻¹ * (φ g) * h) (IndV.mk _ _ h a) = IndV.mk _ _ h (ρ g a) := by
   simp
 
-variable {ρ} in
+variable {ρ : Representation k G A} {σ : Representation k H B}
+
 /-- Construct an `IntertwiningMap` starting from an induced representation by lifting an
 `IntertwiningMap` with a `res` representation as target. -/
-noncomputable def ind.lift {σ : Representation k H B} (f : IntertwiningMap ρ (σ.comp φ)) :
+noncomputable def ind.lift (f : IntertwiningMap ρ (σ.comp φ)) :
     (ind φ ρ).IntertwiningMap σ :=
   ⟨IndV.lift φ ρ (fun h => σ h⁻¹ ∘ₗ f) (by simp [f.isIntertwining]), fun g => by ext; simp⟩
 
 @[simp]
-lemma ind.lift_apply {σ : Representation k H B} (f : IntertwiningMap ρ (σ.comp φ)) (h : H) (a : A) :
+lemma ind.lift_apply_mk (f : ρ.IntertwiningMap (σ.comp φ)) (h : H) (a : A) :
     ind.lift φ f (IndV.mk φ ρ h a) = σ h⁻¹ (f a) := by
   simp [ind.lift]
 
@@ -154,7 +158,7 @@ end Representation
 
 namespace Rep
 
-open CategoryTheory Finsupp Representation
+open CategoryTheory Finsupp
 
 variable {k : Type u} {G : Type v} {H : Type v'} [CommRing k] [Group G] [Group H] (φ : G →* H)
   (A : Rep.{w} k G)
@@ -182,9 +186,8 @@ noncomputable def indFunctor : Rep.{w} k G ⥤ Rep k H where
   map_comp _ _ := by ext; simp
 
 end Ind
-section Adjunction
 
-open Representation
+section Adjunction
 
 variable (B : Rep k H)
 
@@ -221,8 +224,6 @@ end Adjunction
 
 variable {G H : Type u} [Group G] [Group H] (φ : G →* H) (A : Rep k G) (B : Rep k H)
 
-open Representation
-
 /-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear map
 `(Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G` sending `⟦h ⊗ₜ a⟧ ⊗ₜ b` to `⟦a ⊗ ρ(h)(b)⟧` for all
 `h : H`, `a : A`, and `b : B`. -/
@@ -239,9 +240,12 @@ noncomputable def coinvariantsTensorIndHom :
 
 variable {A B} in
 lemma coinvariantsTensorIndHom_mk_tmul_indVMk (h : H) (x : A) (y : B) :
-    coinvariantsTensorIndHom φ A B (coinvariantsTensorMk _ _ (IndV.mk φ _ h x) y) =
-      coinvariantsTensorMk _ _ x (B.ρ h y) := by
-  simp [coinvariantsTensorIndHom, coinvariantsTensorMk]
+    coinvariantsTensorIndHom φ A B (Coinvariants.mk ((Representation.ind φ A.ρ).tprod B.ρ)
+      ((IndV.mk φ _ h x) ⊗ₜ[k] y)) = Coinvariants.mk (A.ρ.tprod (res φ B).ρ) (x ⊗ₜ[k] (B.ρ h y))
+  := by simp [coinvariantsTensorIndHom]
+
+@[deprecated (since := "2026-09-19")]
+alias coinvariantsTensorIndHom_mk_tmul_indMk := coinvariantsTensorIndHom_mk_tmul_indVMk
 
 /-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear map
 `(A ⊗ Res(φ)(B))_G ⟶ (Ind(φ)(A) ⊗ B))_H` sending `⟦a ⊗ₜ b⟧` to `⟦1 ⊗ₜ a⟧ ⊗ₜ b` for all
@@ -257,10 +261,9 @@ noncomputable def coinvariantsTensorIndInv :
         ((IndV.mk φ A.ρ (1 : H) x) ⊗ₜ[k] y) _ (by simp)
 
 variable {A B} in
-lemma coinvariantsTensorIndInv_mk_tmul_indMk (x : A) (y : B) :
-    coinvariantsTensorIndInv φ A B (Coinvariants.mk
-      (A.ρ.tprod (Rep.ρ (res φ B))) <| x ⊗ₜ y) =
-      coinvariantsTensorMk _ _ (IndV.mk φ _ 1 x) y := by
+lemma coinvariantsTensorIndInv_mk_tmul_indVMk (x : A) (y : B) :
+    coinvariantsTensorIndInv φ A B (Coinvariants.mk (A.ρ.tprod (res φ B).ρ) (x ⊗ₜ y)) =
+      Coinvariants.mk ((Representation.ind φ A.ρ).tprod B.ρ) ((IndV.mk φ _ 1 x) ⊗ₜ[k] y) := by
   simp [coinvariantsTensorIndInv, coinvariantsTensorMk]
 
 /-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear
@@ -274,12 +277,11 @@ noncomputable def coinvariantsTensorIndIso :
   inv := coinvariantsTensorIndInv φ A B
   hom_inv_id := by
     ext h a b
-    simpa [coinvariantsTensorIndInv, coinvariantsTensorMk,
-      coinvariantsTensorIndHom, Coinvariants.mk_eq_iff] using
-        Coinvariants.mem_ker_of_eq h (IndV.mk φ _ h a ⊗ₜ[k] b) _ <| by simp
+    simp [coinvariantsTensorIndInv_mk_tmul_indVMk φ, coinvariantsTensorIndHom_mk_tmul_indVMk φ,
+      ← Coinvariants.mk_inv_tmul]
   inv_hom_id := by
     ext
-    simp [coinvariantsTensorIndInv, coinvariantsTensorMk, coinvariantsTensorIndHom]
+    simp [coinvariantsTensorIndInv_mk_tmul_indVMk φ, coinvariantsTensorIndHom_mk_tmul_indVMk φ]
 
 /-- Given a group hom `φ : G →* H` and `A : Rep k G`, the functor `Rep k H ⥤ ModuleCat k` sending
 `B ↦ (Ind(φ)(A) ⊗ B))_H` is naturally isomorphic to the one sending `B ↦ (A ⊗ Res(φ)(B))_G`. -/
@@ -288,6 +290,6 @@ noncomputable def coinvariantsTensorIndNatIso :
     (coinvariantsTensor k H).obj (ind φ A) ≅ resFunctor φ ⋙ (coinvariantsTensor k G).obj A :=
   NatIso.ofComponents (fun B => coinvariantsTensorIndIso φ A B) fun {X Y} f => by
     ext
-    simp [coinvariantsTensorIndHom, coinvariantsTensorMk, hom_comm_apply]
+    simp [coinvariantsTensorIndHom_mk_tmul_indVMk φ, hom_comm_apply]
 
 end Rep

From 0eff8c58f9d6d377b4b4e6570d200412a83a2000 Mon Sep 17 00:00:00 2001
From: JX-Mo <jiaximo1998@163.com>
Date: Sat, 19 Sep 2026 13:29:21 +0800
Subject: [PATCH 05/11] fix

---
 Mathlib/RepresentationTheory/Induced.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/RepresentationTheory/Induced.lean b/Mathlib/RepresentationTheory/Induced.lean
index 41bedfad7d7021..96ea89a7367d8b 100644
--- a/Mathlib/RepresentationTheory/Induced.lean
+++ b/Mathlib/RepresentationTheory/Induced.lean
@@ -43,7 +43,8 @@ is used to prove Shapiro's lemma in
 
 @[expose] public section
 
-open scoped MonoidAlgebra Representation
+open Representation 
+open scoped MonoidAlgebra
 
 universe t w w' u u' v v'
 

From b031a6e22670deae52deab5116cb6227de0cbffc Mon Sep 17 00:00:00 2001
From: "pre-commit-ci-lite[bot]"
 <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Date: Sat, 19 Sep 2026 05:30:06 +0000
Subject: [PATCH 06/11] [pre-commit.ci lite] apply automatic fixes

---
 Mathlib/RepresentationTheory/Induced.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RepresentationTheory/Induced.lean b/Mathlib/RepresentationTheory/Induced.lean
index 96ea89a7367d8b..3ca58b857c5524 100644
--- a/Mathlib/RepresentationTheory/Induced.lean
+++ b/Mathlib/RepresentationTheory/Induced.lean
@@ -43,7 +43,7 @@ is used to prove Shapiro's lemma in
 
 @[expose] public section
 
-open Representation 
+open Representation
 open scoped MonoidAlgebra
 
 universe t w w' u u' v v'

From c0d764ef8c794ad17b6065263e9832d05f0fc93f Mon Sep 17 00:00:00 2001
From: JX-Mo <jiaximo1998@163.com>
Date: Sat, 19 Sep 2026 13:31:40 +0800
Subject: [PATCH 07/11] fix

---
 Mathlib/RepresentationTheory/Induced.lean | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Induced.lean b/Mathlib/RepresentationTheory/Induced.lean
index 3ca58b857c5524..97897f293197ab 100644
--- a/Mathlib/RepresentationTheory/Induced.lean
+++ b/Mathlib/RepresentationTheory/Induced.lean
@@ -43,8 +43,7 @@ is used to prove Shapiro's lemma in
 
 @[expose] public section
 
-open Representation
-open scoped MonoidAlgebra
+open Representation 
 
 universe t w w' u u' v v'
 
@@ -57,13 +56,13 @@ variable {k G H : Type*} [CommRing k] [Group G] [Group H] (φ : G →* H) {A B :
 `k`-module `(k[H] ⊗[k] A)_G` with the `G`-representation on `k[H]` defined by `φ`.
 See `Representation.ind` for the induced `H`-representation on `IndV φ ρ`. -/
 @[implicit_reducible]
-def IndV := Coinvariants (Representation.tprod ((leftRegular k H).comp φ) ρ)
+def IndV := Coinvariants (tprod ((leftRegular k H).comp φ) ρ)
 
 noncomputable instance : AddCommGroup (IndV φ ρ) := inferInstanceAs <|
-  AddCommGroup (Coinvariants (Representation.tprod ((leftRegular k H).comp φ) ρ))
+  AddCommGroup (Coinvariants (tprod ((leftRegular k H).comp φ) ρ))
 
 noncomputable instance : Module k (IndV φ ρ) := inferInstanceAs <|
-  Module k (Coinvariants (Representation.tprod ((leftRegular k H).comp φ) ρ))
+  Module k (Coinvariants (tprod ((leftRegular k H).comp φ) ρ))
 
 /-- Given a group homomorphism `φ : G →* H` and a `G`-representation `(A, ρ)`, this is the
 `H → A →ₗ[k] (k[H] ⊗[k] A)_G` sending `h, a` to `⟦h ⊗ₜ a⟧`. -/
@@ -80,9 +79,9 @@ variable {φ ρ} in
 @[elab_as_elim]
 lemma IndV.inductionOn {p : IndV φ ρ → Prop} (v : IndV φ ρ) (mk : ∀ h a, p (IndV.mk φ ρ h a))
     (add : ∀ x y : IndV φ ρ, p x → p y → p (x + y)) : p v := by
-  refine Representation.Coinvariants.induction_on v fun w => ?_
+  refine Coinvariants.induction_on v fun w => ?_
   refine w.inductionOn (fun m a => ?_) (fun _ _ hx hy => by simpa [map_add] using add _ _ hx hy)
-  refine MonoidAlgebra.induction_linear m (by simpa using mk 1 0) ?_ ?_
+  refine m.induction_linear (by simpa using mk 1 0) ?_ ?_
   · exact fun _ _ hx hy => by simpa [TensorProduct.add_tmul, map_add] using add _ _ hx hy
   · intro h r
     rw [← mul_one r, ← MonoidAlgebra.smul_single', TensorProduct.smul_tmul]
@@ -187,7 +186,6 @@ noncomputable def indFunctor : Rep.{w} k G ⥤ Rep k H where
   map_comp _ _ := by ext; simp
 
 end Ind
-
 section Adjunction
 
 variable (B : Rep k H)
@@ -202,7 +200,7 @@ noncomputable def indResHomEquiv (A : Rep.{max w v' u} k G) (B : Rep.{max w v' u
     ⟨f.hom.toLinearMap ∘ₗ IndV.mk φ A.ρ 1, fun g => by ext; simp [← f.hom.isIntertwining]⟩
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
-  invFun f := Rep.ofHom (Representation.ind.lift φ f.hom)
+  invFun f := Rep.ofHom (ind.lift φ f.hom)
   left_inv f := by ext; simp [← f.hom.isIntertwining]
   right_inv _ := by ext; simp
 

From b9071c1b921c3cd404e22521a6131cbaf76ee2d5 Mon Sep 17 00:00:00 2001
From: "pre-commit-ci-lite[bot]"
 <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Date: Sat, 19 Sep 2026 05:32:19 +0000
Subject: [PATCH 08/11] [pre-commit.ci lite] apply automatic fixes

---
 Mathlib/RepresentationTheory/Induced.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RepresentationTheory/Induced.lean b/Mathlib/RepresentationTheory/Induced.lean
index 97897f293197ab..b10299a3d75fec 100644
--- a/Mathlib/RepresentationTheory/Induced.lean
+++ b/Mathlib/RepresentationTheory/Induced.lean
@@ -43,7 +43,7 @@ is used to prove Shapiro's lemma in
 
 @[expose] public section
 
-open Representation 
+open Representation
 
 universe t w w' u u' v v'
 

From 547df3fcd880132d5bdcad94c829ef4a1d1939be Mon Sep 17 00:00:00 2001
From: JX-Mo <jiaximo1998@163.com>
Date: Sat, 19 Sep 2026 13:54:14 +0800
Subject: [PATCH 09/11] remove open Finsupp

---
 Mathlib/RepresentationTheory/Induced.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Induced.lean b/Mathlib/RepresentationTheory/Induced.lean
index b10299a3d75fec..0718e601c5c7db 100644
--- a/Mathlib/RepresentationTheory/Induced.lean
+++ b/Mathlib/RepresentationTheory/Induced.lean
@@ -158,7 +158,7 @@ end Representation
 
 namespace Rep
 
-open CategoryTheory Finsupp
+open CategoryTheory
 
 variable {k : Type u} {G : Type v} {H : Type v'} [CommRing k] [Group G] [Group H] (φ : G →* H)
   (A : Rep.{w} k G)
@@ -186,13 +186,14 @@ noncomputable def indFunctor : Rep.{w} k G ⥤ Rep k H where
   map_comp _ _ := by ext; simp
 
 end Ind
+
 section Adjunction
 
 variable (B : Rep k H)
 
 /-- Given a group homomorphism `φ : G →* H`, an `H`-representation `B`, and a `G`-representation
 `A`, there is a `k`-linear equivalence between the `H`-representation morphisms `ind φ A ⟶ B` and
-the `G`-representation morphisms `A ⟶ res B`. -/
+the `G`-representation morphisms `A ⟶ res φ B`. -/
 @[simps]
 noncomputable def indResHomEquiv (A : Rep.{max w v' u} k G) (B : Rep.{max w v' u} k H) :
     (ind φ A ⟶ B) ≃ₗ[k] (A ⟶ res φ B) where
@@ -275,7 +276,7 @@ noncomputable def coinvariantsTensorIndIso :
   hom := coinvariantsTensorIndHom φ A B
   inv := coinvariantsTensorIndInv φ A B
   hom_inv_id := by
-    ext h a b
+    ext
     simp [coinvariantsTensorIndInv_mk_tmul_indVMk φ, coinvariantsTensorIndHom_mk_tmul_indVMk φ,
       ← Coinvariants.mk_inv_tmul]
   inv_hom_id := by

From 25cf8c465041606f577323819bdf31b3f3a23942 Mon Sep 17 00:00:00 2001
From: JX-Mo <jiaximo1998@163.com>
Date: Sat, 19 Sep 2026 13:57:36 +0800
Subject: [PATCH 10/11] remove unused variable

---
 Mathlib/RepresentationTheory/Induced.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Induced.lean b/Mathlib/RepresentationTheory/Induced.lean
index 0718e601c5c7db..2ea2a4a8d44477 100644
--- a/Mathlib/RepresentationTheory/Induced.lean
+++ b/Mathlib/RepresentationTheory/Induced.lean
@@ -189,8 +189,6 @@ end Ind
 
 section Adjunction
 
-variable (B : Rep k H)
-
 /-- Given a group homomorphism `φ : G →* H`, an `H`-representation `B`, and a `G`-representation
 `A`, there is a `k`-linear equivalence between the `H`-representation morphisms `ind φ A ⟶ B` and
 the `G`-representation morphisms `A ⟶ res φ B`. -/

From accf3eb508b986c6072ea9ef777b887297ca9aef Mon Sep 17 00:00:00 2001
From: JX-Mo <jiaximo1998@163.com>
Date: Sat, 19 Sep 2026 16:02:29 +0800
Subject: [PATCH 11/11] fix deprecation

---
 Mathlib/RepresentationTheory/Induced.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Induced.lean b/Mathlib/RepresentationTheory/Induced.lean
index 2ea2a4a8d44477..3fc0206f17ff63 100644
--- a/Mathlib/RepresentationTheory/Induced.lean
+++ b/Mathlib/RepresentationTheory/Induced.lean
@@ -242,9 +242,6 @@ lemma coinvariantsTensorIndHom_mk_tmul_indVMk (h : H) (x : A) (y : B) :
       ((IndV.mk φ _ h x) ⊗ₜ[k] y)) = Coinvariants.mk (A.ρ.tprod (res φ B).ρ) (x ⊗ₜ[k] (B.ρ h y))
   := by simp [coinvariantsTensorIndHom]
 
-@[deprecated (since := "2026-09-19")]
-alias coinvariantsTensorIndHom_mk_tmul_indMk := coinvariantsTensorIndHom_mk_tmul_indVMk
-
 /-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear map
 `(A ⊗ Res(φ)(B))_G ⟶ (Ind(φ)(A) ⊗ B))_H` sending `⟦a ⊗ₜ b⟧` to `⟦1 ⊗ₜ a⟧ ⊗ₜ b` for all
 `a : A`, and `b : B`. -/
@@ -264,6 +261,9 @@ lemma coinvariantsTensorIndInv_mk_tmul_indVMk (x : A) (y : B) :
       Coinvariants.mk ((Representation.ind φ A.ρ).tprod B.ρ) ((IndV.mk φ _ 1 x) ⊗ₜ[k] y) := by
   simp [coinvariantsTensorIndInv, coinvariantsTensorMk]
 
+@[deprecated (since := "2026-09-19")]
+alias coinvariantsTensorIndInv_mk_tmul_indMk := coinvariantsTensorIndInv_mk_tmul_indVMk
+
 /-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear
 isomorphism `(Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G` sending `⟦h ⊗ₜ a⟧ ⊗ₜ b` to `⟦a ⊗ ρ(h)(b)⟧`
 for all `h : H`, `a : A`, and `b : B`. -/