mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A✝ : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
A : Rep.{max w u, u, v} k ↥S
g : G
⊢ ↑(LinearEquiv.ofLinearMap A.indToCoind A.coindToInd ⋯ ⋯) ∘ₗ (Representation.ind S.subtype A.ρ) g =
    (Representation.coind S.subtype A.ρ) g ∘ₗ ↑(LinearEquiv.ofLinearMap A.indToCoind A.coindToInd ⋯ ⋯)

Tactic:
ext

Goal state after:
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A✝ : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
A : Rep.{max w u, u, v} k ↥S
g x✝² : G
x✝¹ : ↑A
x✝ : G
⊢ ↑(((AlgebraTensorModule.curry
                ((↑(LinearEquiv.ofLinearMap A.indToCoind A.coindToInd ⋯ ⋯) ∘ₗ (Representation.ind S.subtype A.ρ) g) ∘ₗ
                  Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ)) ∘ₗ
              MonoidAlgebra.lsingle x✝²)
            1)
          x✝¹)
      x✝ =
    ↑(((AlgebraTensorModule.curry
                (((Representation.coind S.subtype A.ρ) g ∘ₗ ↑(LinearEquiv.ofLinearMap A.indToCoind A.coindToInd ⋯ ⋯)) ∘ₗ
                  Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ)) ∘ₗ
              MonoidAlgebra.lsingle x✝²)
            1)
          x✝¹)
      x✝
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A✝ : Rep k G
g : G
A : Rep k G
⊢ A.norm ≫ (A.applyAsHom g - 𝟙 A) = 0

Tactic:
ext

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A✝ : Rep k G
g : G
A : Rep k G
x✝ : ↑A
⊢ (Hom.hom (A.norm ≫ (A.applyAsHom g - 𝟙 A))).toLinearMap x✝ = (Hom.hom 0).toLinearMap x✝
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A✝ : Rep k G
g : G
A : Rep k G
⊢ (A.applyAsHom g - 𝟙 A) ≫ A.norm = 0

Tactic:
ext

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A✝ : Rep k G
g : G
A : Rep k G
x✝ : ↑A
⊢ (Hom.hom ((A.applyAsHom g - 𝟙 A) ≫ A.norm)).toLinearMap x✝ = (Hom.hom 0).toLinearMap x✝
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap = 0

Tactic:
ext

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
inst✝ : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
⊢ (coindResAdjunction k S).unit.app A =
    (indResAdjunction k S.subtype).unit.app A ≫ (resFunctor S.subtype).map A.indCoindIso.hom

Tactic:
ext

Goal state after:
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
inst✝ : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
x✝ : ↑((𝟭 (Rep.{max (max u v) w, u, v} k ↥S)).obj A)
⊢ (Hom.hom ((coindResAdjunction k S).unit.app A)).toLinearMap x✝ =
    (Hom.hom ((indResAdjunction k S.subtype).unit.app A ≫ (resFunctor S.subtype).map A.indCoindIso.hom)).toLinearMap x✝
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
⊢ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap = 0

Tactic:
ext

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case zero
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ {
        X₁ :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((chainComplexFunctor k g).obj (leftRegular k G))).X₁,
        X₂ :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((chainComplexFunctor k g).obj (leftRegular k G))).X₂,
        X₃ :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((ChainComplex.single₀ (Rep k G)).obj (trivial k G k))).X₂,
        f :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
              ((chainComplexFunctor k g).obj (leftRegular k G))).f,
        g :=
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
              ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
                ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂,
        zero := ⋯ }.Exact ∧
    Epi
      ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
          ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
            ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂

Tactic:
constructor

Goal state after:
case zero.left
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ {
      X₁ :=
        ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
            ((chainComplexFunctor k g).obj (leftRegular k G))).X₁,
      X₂ :=
        ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
            ((chainComplexFunctor k g).obj (leftRegular k G))).X₂,
      X₃ :=
        ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
            ((ChainComplex.single₀ (Rep k G)).obj (trivial k G k))).X₂,
      f :=
        ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
            ((chainComplexFunctor k g).obj (leftRegular k G))).f,
      g :=
        ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
            ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
              ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂,
      zero := ⋯ }.Exact

case zero.right
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ Epi
    ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
        ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
          ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : CommRing k
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommGroup A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommGroup B
inst✝ : Module k B
τ : Representation k G B
h : H
x✝ : G
⊢ LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * h⁻¹) ∘ₗ
      (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) x✝ =
    (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) x✝ ∘ₗ
      LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * h⁻¹)

Tactic:
ext

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : CommRing k
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommGroup A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommGroup B
inst✝ : Module k B
τ : Representation k G B
h : H
x✝² : G
x✝¹ : H
x✝ : A
⊢ ((TensorProduct.AlgebraTensorModule.curry
            (LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * h⁻¹) ∘ₗ
              (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) x✝²) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((tprod (MonoidHom.comp (leftRegular k H) φ) ρ) x✝² ∘ₗ
              LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * h⁻¹)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : CommRing k
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommGroup A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommGroup B
inst✝ : Module k B
τ : Representation k G B
⊢ Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
      { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * 1⁻¹),
        isIntertwining' := ⋯ } =
    1

Tactic:
ext

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : CommRing k
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommGroup A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommGroup B
inst✝ : Module k B
τ : Representation k G B
x✝¹ : H
x✝ : A
⊢ ((TensorProduct.AlgebraTensorModule.curry
            (Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * 1⁻¹),
                  isIntertwining' := ⋯ } ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (1 ∘ₗ Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : CommRing k
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommGroup A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommGroup B
inst✝ : Module k B
τ : Representation k G B
x✝¹ x✝ : H
⊢ Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
      { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * (x✝¹ * x✝)⁻¹),
        isIntertwining' := ⋯ } =
    Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
        { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * x✝¹⁻¹),
          isIntertwining' := ⋯ } *
      Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
        { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * x✝⁻¹),
          isIntertwining' := ⋯ }

Tactic:
ext

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : CommRing k
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommGroup A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommGroup B
inst✝ : Module k B
τ : Representation k G B
x✝³ x✝² x✝¹ : H
x✝ : A
⊢ ((TensorProduct.AlgebraTensorModule.curry
            (Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * (x✝³ * x✝²)⁻¹),
                  isIntertwining' := ⋯ } ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * x✝³⁻¹),
                    isIntertwining' := ⋯ } *
                Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                  { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * x✝²⁻¹),
                    isIntertwining' := ⋯ }) ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
A : Rep k G
n : ℕ
f g : (Fin n → G) → ↑A
⊢ (fun g_1 ↦
      (A.ρ (g_1 0)) ((f + g) fun i ↦ g_1 i.succ) +
        ∑ j, (-1) ^ (↑j + 1) • (f + g) (j.contractNth (fun x1 x2 ↦ x1 * x2) g_1)) =
    (fun g ↦ (A.ρ (g 0)) (f fun i ↦ g i.succ) + ∑ j, (-1) ^ (↑j + 1) • f (j.contractNth (fun x1 x2 ↦ x1 * x2) g)) +
      fun g_1 ↦
      (A.ρ (g_1 0)) (g fun i ↦ g_1 i.succ) + ∑ j, (-1) ^ (↑j + 1) • g (j.contractNth (fun x1 x2 ↦ x1 * x2) g_1)

Tactic:
ext

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
A : Rep k G
n : ℕ
f g : (Fin n → G) → ↑A
x✝ : Fin (n + 1) → G
⊢ (A.ρ (x✝ 0)) ((f + g) fun i ↦ x✝ i.succ) + ∑ j, (-1) ^ (↑j + 1) • (f + g) (j.contractNth (fun x1 x2 ↦ x1 * x2) x✝) =
    ((fun g ↦ (A.ρ (g 0)) (f fun i ↦ g i.succ) + ∑ j, (-1) ^ (↑j + 1) • f (j.contractNth (fun x1 x2 ↦ x1 * x2) g)) +
        fun g_1 ↦
        (A.ρ (g_1 0)) (g fun i ↦ g_1 i.succ) + ∑ j, (-1) ^ (↑j + 1) • g (j.contractNth (fun x1 x2 ↦ x1 * x2) g_1))
      x✝
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
A : Rep k G
n : ℕ
r : k
f : (Fin n → G) → ↑A
⊢ (fun g ↦
      (A.ρ (g 0)) ((r • f) fun i ↦ g i.succ) + ∑ j, (-1) ^ (↑j + 1) • (r • f) (j.contractNth (fun x1 x2 ↦ x1 * x2) g)) =
    (RingHom.id k) r • fun g ↦
      (A.ρ (g 0)) (f fun i ↦ g i.succ) + ∑ j, (-1) ^ (↑j + 1) • f (j.contractNth (fun x1 x2 ↦ x1 * x2) g)

Tactic:
ext

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
A : Rep k G
n : ℕ
r : k
f : (Fin n → G) → ↑A
x✝ : Fin (n + 1) → G
⊢ (A.ρ (x✝ 0)) ((r • f) fun i ↦ x✝ i.succ) + ∑ j, (-1) ^ (↑j + 1) • (r • f) (j.contractNth (fun x1 x2 ↦ x1 * x2) x✝) =
    ((RingHom.id k) r • fun g ↦
        (A.ρ (g 0)) (f fun i ↦ g i.succ) + ∑ j, (-1) ^ (↑j + 1) • f (j.contractNth (fun x1 x2 ↦ x1 * x2) g))
      x✝
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ d A n =
    (freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv ≫
      ((barComplex k G).linearYonedaObj k A).d n (n + 1) ≫ (freeLiftLEquiv k G (Fin (n + 1) → G) A).toModuleIso.hom

Tactic:
ext

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
x✝¹ : ↑(ModuleCat.of k ((Fin n → G) → ↑A))
x✝ : Fin (n + 1) → G
⊢ (ModuleCat.Hom.hom (d A n)) x✝¹ x✝ =
    (ModuleCat.Hom.hom
        ((freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv ≫
          ((barComplex k G).linearYonedaObj k A).d n (n + 1) ≫
            (freeLiftLEquiv k G (Fin (n + 1) → G) A).toModuleIso.hom))
      x✝¹ x✝
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A✝ : Rep k G
A B : Rep k G
f : A ⟶ B
g : H
⊢ Representation.Coinvariants.map (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
        (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) B.ρ)
        { toLinearMap := LinearMap.lTensor k[H] (Hom.hom f).toLinearMap, isIntertwining' := ⋯ } ∘ₗ
      (Representation.ind φ A.ρ) g =
    (Representation.ind φ B.ρ) g ∘ₗ
      Representation.Coinvariants.map (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
        (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) B.ρ)
        { toLinearMap := LinearMap.lTensor k[H] (Hom.hom f).toLinearMap, isIntertwining' := ⋯ }

Tactic:
ext

Goal state after:
k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A✝ : Rep k G
A B : Rep k G
f : A ⟶ B
g x✝¹ : H
x✝ : ↑A
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((Representation.Coinvariants.map
                  (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                  (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) B.ρ)
                  { toLinearMap := LinearMap.lTensor k[H] (Hom.hom f).toLinearMap, isIntertwining' := ⋯ } ∘ₗ
                (Representation.ind φ A.ρ) g) ∘ₗ
              Representation.Coinvariants.mk
                (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            (((Representation.ind φ B.ρ) g ∘ₗ
                Representation.Coinvariants.map
                  (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                  (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) B.ρ)
                  { toLinearMap := LinearMap.lTensor k[H] (Hom.hom f).toLinearMap, isIntertwining' := ⋯ }) ∘ₗ
              Representation.Coinvariants.mk
                (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A x✝ : Rep k G
⊢ indMap φ (𝟙 x✝) = 𝟙 (ind φ x✝)

Tactic:
ext

Goal state after:
k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A x✝² : Rep k G
x✝¹ : H
x✝ : ↑x✝²
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom (indMap φ (𝟙 x✝²))).toLinearMap ∘ₗ
              Representation.Coinvariants.mk
                (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) x✝².ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom (𝟙 (ind φ x✝²))).toLinearMap ∘ₗ
              Representation.Coinvariants.mk
                (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) x✝².ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A X✝ Y✝ Z✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ indMap φ (x✝¹ ≫ x✝) = indMap φ x✝¹ ≫ indMap φ x✝

Tactic:
ext

Goal state after:
k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A X✝ Y✝ Z✝ : Rep k G
x✝³ : X✝ ⟶ Y✝
x✝² : Y✝ ⟶ Z✝
x✝¹ : H
x✝ : ↑X✝
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom (indMap φ (x✝³ ≫ x✝²))).toLinearMap ∘ₗ
              Representation.Coinvariants.mk
                (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X✝.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom (indMap φ x✝³ ≫ indMap φ x✝²)).toLinearMap ∘ₗ
              Representation.Coinvariants.mk
                (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X✝.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A✝ : Rep k G
B✝ : Rep k H
A : Rep k G
B : Rep k H
f : A ⟶ res φ B
g : H
⊢ Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
        (TensorProduct.lift
          (((lift (↑A →ₗ[k] ↑B) k H) fun h ↦ B.ρ h⁻¹ ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ
            ↑(MonoidAlgebra.coeffLinearEquiv k)))
        ⋯ ∘ₗ
      (Representation.ind φ A.ρ) g =
    B.ρ g ∘ₗ
      Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
        (TensorProduct.lift
          (((lift (↑A →ₗ[k] ↑B) k H) fun h ↦ B.ρ h⁻¹ ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ
            ↑(MonoidAlgebra.coeffLinearEquiv k)))
        ⋯

Tactic:
ext

Goal state after:
k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A✝ : Rep k G
B✝ : Rep k H
A : Rep k G
B : Rep k H
f : A ⟶ res φ B
g x✝¹ : H
x✝ : ↑A
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                  (TensorProduct.lift
                    (((lift (↑A →ₗ[k] ↑B) k H) fun h ↦ B.ρ h⁻¹ ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ
                      ↑(MonoidAlgebra.coeffLinearEquiv k)))
                  ⋯ ∘ₗ
                (Representation.ind φ A.ρ) g) ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((B.ρ g ∘ₗ
                Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                  (TensorProduct.lift
                    (((lift (↑A →ₗ[k] ↑B) k H) fun h ↦ B.ρ h⁻¹ ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ
                      ↑(MonoidAlgebra.coeffLinearEquiv k)))
                  ⋯) ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A✝ : Rep k G
B✝ : Rep k H
A : Rep k G
B : Rep k H
x✝ : A ⟶ res φ B
⊢ (fun f ↦ ofHom { toLinearMap := (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1, isIntertwining' := ⋯ })
      ((fun f ↦
          ofHom
            {
              toLinearMap :=
                Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                  (TensorProduct.lift
                    (((lift (↑A →ₗ[k] ↑B) k H) fun h ↦ B.ρ h⁻¹ ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ
                      ↑(MonoidAlgebra.coeffLinearEquiv k)))
                  ⋯,
              isIntertwining' := ⋯ })
        x✝) =
    x✝

Tactic:
ext

Goal state after:
k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A✝ : Rep k G
B✝ : Rep k H
A : Rep k G
B : Rep k H
x✝¹ : A ⟶ res φ B
x✝ : ↑(of A.ρ)
⊢ (Hom.hom
          ((fun f ↦ ofHom { toLinearMap := (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1, isIntertwining' := ⋯ })
            ((fun f ↦
                ofHom
                  {
                    toLinearMap :=
                      Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                        (TensorProduct.lift
                          (((lift (↑A →ₗ[k] ↑B) k H) fun h ↦ B.ρ h⁻¹ ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ
                            ↑(MonoidAlgebra.coeffLinearEquiv k)))
                        ⋯,
                    isIntertwining' := ⋯ })
              x✝¹))).toLinearMap
      x✝ =
    (Hom.hom x✝¹).toLinearMap x✝