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
X✝ Y✝ : Rep.{max u w, u, v} k ↥S
f : X✝ ⟶ Y✝
⊢ (indFunctor k S.subtype).map f ≫ Y✝.indCoindIso.hom = X✝.indCoindIso.hom ≫ (coindFunctor k S.subtype).map f

Tactic:
;

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
X✝ Y✝ : Rep.{max u w, u, v} k ↥S
f : X✝ ⟶ Y✝
⊢ (indFunctor k S.subtype).map f ≫ Y✝.indCoindIso.hom = X✝.indCoindIso.hom ≫ (coindFunctor k S.subtype).map f
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
x✝ : ↑A
⊢ (Hom.hom (A.norm ≫ (A.applyAsHom g - 𝟙 A))).toLinearMap x✝ = (Hom.hom 0).toLinearMap x✝

Tactic:
;

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
x✝ : ↑A
⊢ (Hom.hom (A.norm ≫ (A.applyAsHom g - 𝟙 A))).toLinearMap x✝ = (Hom.hom 0).toLinearMap x✝

Tactic:
simp [sub_hom, applyAsHom, norm]

Goal state after:
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
x✝ : ↑A
⊢ (Hom.hom ((A.applyAsHom g - 𝟙 A) ≫ A.norm)).toLinearMap x✝ = (Hom.hom 0).toLinearMap x✝

Tactic:
;

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
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✝

Tactic:
;

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.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
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✝

Tactic:
simp [sub_hom, applyAsHom, norm]

Goal state after:
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
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✝

Tactic:
;

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: 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✝

Tactic:
simp [sub_hom, applyAsHom, norm]

Goal state after:
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
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✝

Tactic:
;

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
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✝

Tactic:
;

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
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✝

Tactic:
;

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
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✝

Tactic:
;

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✝
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✝

Tactic:
;

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 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✝

Tactic:
;

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
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✝

Tactic:
;

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✝
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
X'✝ X✝ : Rep k G
Y✝ : Rep k H
x✝³ : X'✝ ⟶ X✝
x✝² : X✝ ⟶ (resFunctor φ).obj Y✝
x✝¹ : H
x✝ : ↑X'✝
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom ((indResHomEquiv φ X'✝ Y✝).symm (x✝³ ≫ x✝²))).toLinearMap ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X'✝.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom ((indFunctor k φ).map x✝³ ≫ (indResHomEquiv φ X✝ Y✝).toEquiv.symm x✝²)).toLinearMap ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X'✝.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝

Tactic:
;

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
X'✝ X✝ : Rep k G
Y✝ : Rep k H
x✝³ : X'✝ ⟶ X✝
x✝² : X✝ ⟶ (resFunctor φ).obj Y✝
x✝¹ : H
x✝ : ↑X'✝
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom ((indResHomEquiv φ X'✝ Y✝).symm (x✝³ ≫ x✝²))).toLinearMap ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) X'✝.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom ((indFunctor k φ).map x✝³ ≫ (indResHomEquiv φ X✝ Y✝).toEquiv.symm x✝²)).toLinearMap ∘ₗ
              Coinvariants.mk (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
X✝ : Rep k G
Y✝ Y'✝ : Rep k H
f✝ : (indFunctor k φ).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
⊢ (indResHomEquiv φ X✝ Y'✝).toEquiv (f✝ ≫ g✝) = (indResHomEquiv φ X✝ Y✝).toEquiv f✝ ≫ (resFunctor φ).map g✝

Tactic:
;

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
X✝ : Rep k G
Y✝ Y'✝ : Rep k H
f✝ : (indFunctor k φ).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
⊢ (indResHomEquiv φ X✝ Y'✝).toEquiv (f✝ ≫ g✝) = (indResHomEquiv φ X✝ Y✝).toEquiv f✝ ≫ (resFunctor φ).map g✝
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✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
g : G
x✝² : H
x✝¹ : ↑A
x✝ : ↑B
⊢ (((TensorProduct.AlgebraTensorModule.curry
              (TensorProduct.lift
                  (((lift
                        (↑A →ₗ[k]
                          ↑B →ₗ[k] (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
                        k H)
                      fun g ↦ (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
                    ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
                (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) g) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry
              (TensorProduct.lift
                (((lift
                      (↑A →ₗ[k]
                        ↑B →ₗ[k] (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
                      k H)
                    fun g ↦ (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
                  ↑(MonoidAlgebra.coeffLinearEquiv k))) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝

Tactic:
;

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✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
g : G
x✝² : H
x✝¹ : ↑A
x✝ : ↑B
⊢ (((TensorProduct.AlgebraTensorModule.curry
              (TensorProduct.lift
                  (((lift
                        (↑A →ₗ[k]
                          ↑B →ₗ[k] (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
                        k H)
                      fun g ↦ (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
                    ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
                (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) g) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry
              (TensorProduct.lift
                (((lift
                      (↑A →ₗ[k]
                        ↑B →ₗ[k] (((MonoidalCategory.curriedTensor (Rep k G)).obj A).obj (res φ B)).ρ.Coinvariants)
                      k H)
                    fun g ↦ (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
                  ↑(MonoidAlgebra.coeffLinearEquiv k))) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝