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

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep k G
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
⊢ LinearMap.codRestrict (Representation.coindV φ A.ρ) ((LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ∘ₗ B.ρ g)
      ⋯ =
    (Representation.coind φ A.ρ) g ∘ₗ
      LinearMap.codRestrict (Representation.coindV φ A.ρ) (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ⋯

Tactic:
;

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep k G
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
⊢ LinearMap.codRestrict (Representation.coindV φ A.ρ) ((LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ∘ₗ B.ρ g)
      ⋯ =
    (Representation.coind φ A.ρ) g ∘ₗ
      LinearMap.codRestrict (Representation.coindV φ A.ρ) (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ⋯
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
X : Type u_5
inst✝¹³ : CommRing k✝
inst✝¹² : Monoid G✝
inst✝¹¹ : AddCommGroup V✝
inst✝¹⁰ : Module k✝ V✝
inst✝⁹ : AddCommGroup W✝
inst✝⁸ : Module k✝ W✝
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ✝ : Representation k✝ G✝ W✝
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
x✝¹ : V
x✝ : G
⊢ ((TensorProduct.AlgebraTensorModule.curry
            (((Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ
                  (TensorProduct.mk k V k[G]).flip (MonoidAlgebra.single 1 1)) ∘ₗ
                ρ.ofCoinvariantsTprodLeftRegular) ∘ₗ
              Coinvariants.mk (ρ.tprod (leftRegular k G))))
          x✝¹ ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((TensorProduct.AlgebraTensorModule.curry (LinearMap.id ∘ₗ Coinvariants.mk (ρ.tprod (leftRegular k G)))) x✝¹ ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1

Tactic:
;

Goal state after:
k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
X : Type u_5
inst✝¹³ : CommRing k✝
inst✝¹² : Monoid G✝
inst✝¹¹ : AddCommGroup V✝
inst✝¹⁰ : Module k✝ V✝
inst✝⁹ : AddCommGroup W✝
inst✝⁸ : Module k✝ W✝
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ✝ : Representation k✝ G✝ W✝
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
x✝¹ : V
x✝ : G
⊢ ((TensorProduct.AlgebraTensorModule.curry
            (((Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ
                  (TensorProduct.mk k V k[G]).flip (MonoidAlgebra.single 1 1)) ∘ₗ
                ρ.ofCoinvariantsTprodLeftRegular) ∘ₗ
              Coinvariants.mk (ρ.tprod (leftRegular k G))))
          x✝¹ ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((TensorProduct.AlgebraTensorModule.curry (LinearMap.id ∘ₗ Coinvariants.mk (ρ.tprod (leftRegular k G)))) x✝¹ ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep k G
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
x✝¹ : ↑B
x✝ : H
⊢ ↑((LinearMap.codRestrict (Representation.coindV φ A.ρ)
            ((LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ∘ₗ B.ρ g) ⋯)
          x✝¹)
      x✝ =
    ↑(((Representation.coind φ A.ρ) g ∘ₗ
            LinearMap.codRestrict (Representation.coindV φ A.ρ) (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h)
              ⋯)
          x✝¹)
      x✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep k G
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
x✝¹ : ↑B
x✝ : H
⊢ ↑((LinearMap.codRestrict (Representation.coindV φ A.ρ)
            ((LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ∘ₗ B.ρ g) ⋯)
          x✝¹)
      x✝ =
    ↑(((Representation.coind φ A.ρ) g ∘ₗ
            LinearMap.codRestrict (Representation.coindV φ A.ρ) (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h)
              ⋯)
          x✝¹)
      x✝
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
g : G
x✝ : ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))
⊢ ((Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype ∘ₗ (A.ρ.toCoinvariantsKer S) g) x✝ =
    (A.ρ g ∘ₗ (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype) x✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
g : G
x✝ : ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))
⊢ ((Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype ∘ₗ (A.ρ.toCoinvariantsKer S) g) x✝ =
    (A.ρ g ∘ₗ (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype) x✝
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↑(A.toCoinvariantsKer S)
⊢ (Hom.hom
          (ofHom { toLinearMap := (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype, isIntertwining' := ⋯ } ≫
            A.toCoinvariantsMkQ S)).toLinearMap
      x =
    (Hom.hom 0).toLinearMap x

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↑(A.toCoinvariantsKer S)
⊢ (Hom.hom
          (ofHom { toLinearMap := (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype, isIntertwining' := ⋯ } ≫
            A.toCoinvariantsMkQ S)).toLinearMap
      x =
    (Hom.hom 0).toLinearMap x
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep.{?u.16, u, v} k G
B : Rep.{max w t, u, w} k H
A : Rep.{max w t, u, v} k G
x : res φ B ⟶ A
x✝ : ↑(of (MonoidHom.comp B.ρ φ))
⊢ (Hom.hom
          ((fun f ↦
              ofHom
                { toLinearMap := LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap,
                  isIntertwining' := ⋯ })
            ((fun f ↦ resCoindToHom φ B A f) x))).toLinearMap
      x✝ =
    (Hom.hom x).toLinearMap x✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep.{?u.16, u, v} k G
B : Rep.{max w t, u, w} k H
A : Rep.{max w t, u, v} k G
x : res φ B ⟶ A
x✝ : ↑(of (MonoidHom.comp B.ρ φ))
⊢ (Hom.hom
          ((fun f ↦
              ofHom
                { toLinearMap := LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap,
                  isIntertwining' := ⋯ })
            ((fun f ↦ resCoindToHom φ B A f) x))).toLinearMap
      x✝ =
    (Hom.hom x).toLinearMap x✝
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
A B X✝ Y✝ Z✝ : Rep k G
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ↑X✝
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom (Coinvariants.map X✝.ρ Z✝.ρ (Hom.hom (x✝² ≫ x✝¹)))) ∘ₗ Coinvariants.mk X✝.ρ) x✝ =
    (ModuleCat.Hom.hom
          (ModuleCat.ofHom (Coinvariants.map X✝.ρ Y✝.ρ (Hom.hom x✝²)) ≫
            ModuleCat.ofHom (Coinvariants.map Y✝.ρ Z✝.ρ (Hom.hom x✝¹))) ∘ₗ
        Coinvariants.mk X✝.ρ)
      x✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
A B X✝ Y✝ Z✝ : Rep k G
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ↑X✝
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom (Coinvariants.map X✝.ρ Z✝.ρ (Hom.hom (x✝² ≫ x✝¹)))) ∘ₗ Coinvariants.mk X✝.ρ) x✝ =
    (ModuleCat.Hom.hom
          (ModuleCat.ofHom (Coinvariants.map X✝.ρ Y✝.ρ (Hom.hom x✝²)) ≫
            ModuleCat.ofHom (Coinvariants.map Y✝.ρ Z✝.ρ (Hom.hom x✝¹))) ∘ₗ
        Coinvariants.mk X✝.ρ)
      x✝
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep.{?u.16, u, v} k G
B : Rep.{max w t, u, w} k H
A : Rep.{max w t, u, v} k G
z : B ⟶ coind.{u, v, w, max t w} φ A
x✝¹ : ↑B
x✝ : H
⊢ ↑((Hom.hom
              ((fun f ↦ resCoindToHom φ B A f)
                ((fun f ↦
                    ofHom
                      {
                        toLinearMap :=
                          LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap,
                        isIntertwining' := ⋯ })
                  z))).toLinearMap
          x✝¹)
      x✝ =
    ↑((Hom.hom z).toLinearMap x✝¹) x✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep.{?u.16, u, v} k G
B : Rep.{max w t, u, w} k H
A : Rep.{max w t, u, v} k G
z : B ⟶ coind.{u, v, w, max t w} φ A
x✝¹ : ↑B
x✝ : H
⊢ ↑((Hom.hom
              ((fun f ↦ resCoindToHom φ B A f)
                ((fun f ↦
                    ofHom
                      {
                        toLinearMap :=
                          LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap,
                        isIntertwining' := ⋯ })
                  z))).toLinearMap
          x✝¹)
      x✝ =
    ↑((Hom.hom z).toLinearMap x✝¹) x✝
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
A B X : Rep k G
g : G
x✝ : ↑X
⊢ (ModuleCat.Hom.hom ((coinvariantsMk k G).app X) ∘ₗ X.ρ g) x✝ =
    ((Representation.trivial k G ↑((coinvariantsFunctor k G).obj X)) g ∘ₗ
        ModuleCat.Hom.hom ((coinvariantsMk k G).app X))
      x✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
A B X : Rep k G
g : G
x✝ : ↑X
⊢ (ModuleCat.Hom.hom ((coinvariantsMk k G).app X) ∘ₗ X.ρ g) x✝ =
    ((Representation.trivial k G ↑((coinvariantsFunctor k G).obj X)) g ∘ₗ
        ModuleCat.Hom.hom ((coinvariantsMk k G).app X))
      x✝
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Monoid G✝
A B : Rep k✝ G✝
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : S.Normal
X Y : Rep k G
f : X ⟶ Y
g✝ : G ⧸ S
g : G
x✝ : ↑X
⊢ ((ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)) ∘ₗ
          ((X.toCoinvariants S).ρ.ofQuotient S) ↑g) ∘ₗ
        Coinvariants.mk (MonoidHom.comp X.ρ S.subtype))
      x✝ =
    ((((Y.toCoinvariants S).ρ.ofQuotient S) ↑g ∘ₗ
          ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f))) ∘ₗ
        Coinvariants.mk (MonoidHom.comp X.ρ S.subtype))
      x✝

Tactic:
;

Goal state after:
k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Monoid G✝
A B : Rep k✝ G✝
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : S.Normal
X Y : Rep k G
f : X ⟶ Y
g✝ : G ⧸ S
g : G
x✝ : ↑X
⊢ ((ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)) ∘ₗ
          ((X.toCoinvariants S).ρ.ofQuotient S) ↑g) ∘ₗ
        Coinvariants.mk (MonoidHom.comp X.ρ S.subtype))
      x✝ =
    ((((Y.toCoinvariants S).ρ.ofQuotient S) ↑g ∘ₗ
          ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f))) ∘ₗ
        Coinvariants.mk (MonoidHom.comp X.ρ S.subtype))
      x✝
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep.{?u.16, u, v} k G
X'✝ X✝ : Rep.{max w t, u, w} k H
Y✝ : Rep.{max w t, u, v} k G
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (coindFunctor k φ).obj Y✝
⊢ (resCoindHomEquiv.{?u.42, u, v, w} φ X'✝ Y✝).toEquiv.symm (f✝ ≫ g✝) =
    (resFunctor φ).map f✝ ≫ (resCoindHomEquiv.{?u.42, u, v, w} φ X✝ Y✝).toEquiv.symm g✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep.{?u.16, u, v} k G
X'✝ X✝ : Rep.{max w t, u, w} k H
Y✝ : Rep.{max w t, u, v} k G
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (coindFunctor k φ).obj Y✝
⊢ (resCoindHomEquiv.{?u.42, u, v, w} φ X'✝ Y✝).toEquiv.symm (f✝ ≫ g✝) =
    (resFunctor φ).map f✝ ≫ (resCoindHomEquiv.{?u.42, u, v, w} φ X✝ Y✝).toEquiv.symm g✝
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Monoid G✝
A B : Rep k✝ G✝
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : S.Normal
X : Rep k G
x✝ : ↑X
⊢ ((Hom.hom
            (ofHom
              { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map (𝟙 X))),
                isIntertwining' := ⋯ })).toLinearMap ∘ₗ
        Coinvariants.mk (MonoidHom.comp X.ρ S.subtype))
      x✝ =
    ((Hom.hom (𝟙 (X.quotientToCoinvariants S))).toLinearMap ∘ₗ Coinvariants.mk (MonoidHom.comp X.ρ S.subtype)) x✝

Tactic:
;

Goal state after:
k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Monoid G✝
A B : Rep k✝ G✝
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : S.Normal
X : Rep k G
x✝ : ↑X
⊢ ((Hom.hom
            (ofHom
              { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map (𝟙 X))),
                isIntertwining' := ⋯ })).toLinearMap ∘ₗ
        Coinvariants.mk (MonoidHom.comp X.ρ S.subtype))
      x✝ =
    ((Hom.hom (𝟙 (X.quotientToCoinvariants S))).toLinearMap ∘ₗ Coinvariants.mk (MonoidHom.comp X.ρ S.subtype)) x✝
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Monoid G✝
A B : Rep k✝ G✝
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : S.Normal
X✝ Y✝ Z✝ : Rep k G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : ↑X✝
⊢ ((Hom.hom
            (ofHom
              { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map (f ≫ g))),
                isIntertwining' := ⋯ })).toLinearMap ∘ₗ
        Coinvariants.mk (MonoidHom.comp X✝.ρ S.subtype))
      x✝ =
    ((Hom.hom
            (ofHom
                { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)),
                  isIntertwining' := ⋯ } ≫
              ofHom
                { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map g)),
                  isIntertwining' := ⋯ })).toLinearMap ∘ₗ
        Coinvariants.mk (MonoidHom.comp X✝.ρ S.subtype))
      x✝

Tactic:
;

Goal state after:
k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Monoid G✝
A B : Rep k✝ G✝
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : S.Normal
X✝ Y✝ Z✝ : Rep k G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : ↑X✝
⊢ ((Hom.hom
            (ofHom
              { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map (f ≫ g))),
                isIntertwining' := ⋯ })).toLinearMap ∘ₗ
        Coinvariants.mk (MonoidHom.comp X✝.ρ S.subtype))
      x✝ =
    ((Hom.hom
            (ofHom
                { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)),
                  isIntertwining' := ⋯ } ≫
              ofHom
                { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map g)),
                  isIntertwining' := ⋯ })).toLinearMap ∘ₗ
        Coinvariants.mk (MonoidHom.comp X✝.ρ S.subtype))
      x✝
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep.{?u.16, u, v} k G
X✝ : Rep.{max w t, u, w} k H
Y✝ Y'✝ : Rep.{max w t, u, v} k G
f✝ : (resFunctor φ).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
⊢ (resCoindHomEquiv.{t, u, v, w} φ X✝ Y'✝).toEquiv (f✝ ≫ g✝) =
    (resCoindHomEquiv.{t, u, v, w} φ X✝ Y✝).toEquiv f✝ ≫ (coindFunctor k φ).map g✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep.{?u.16, u, v} k G
X✝ : Rep.{max w t, u, w} k H
Y✝ Y'✝ : Rep.{max w t, u, v} k G
f✝ : (resFunctor φ).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
⊢ (resCoindHomEquiv.{t, u, v, w} φ X✝ Y'✝).toEquiv (f✝ ≫ g✝) =
    (resCoindHomEquiv.{t, u, v, w} φ X✝ Y✝).toEquiv f✝ ≫ (coindFunctor k φ).map g✝
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep.{?u.16, u, v} k G
X✝ : Rep.{max w t, u, w} k H
Y✝ Y'✝ : Rep.{max w t, u, v} k G
f✝ : (resFunctor φ).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
x✝ : ↑X✝
⊢ (Hom.hom ((resCoindHomEquiv.{t, u, v, w} φ X✝ Y'✝).toEquiv (f✝ ≫ g✝))).toLinearMap x✝ =
    (Hom.hom ((resCoindHomEquiv.{t, u, v, w} φ X✝ Y✝).toEquiv f✝ ≫ (coindFunctor k φ).map g✝)).toLinearMap x✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep.{?u.16, u, v} k G
X✝ : Rep.{max w t, u, w} k H
Y✝ Y'✝ : Rep.{max w t, u, v} k G
f✝ : (resFunctor φ).obj X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y'✝
x✝ : ↑X✝
⊢ (Hom.hom ((resCoindHomEquiv.{t, u, v, w} φ X✝ Y'✝).toEquiv (f✝ ≫ g✝))).toLinearMap x✝ =
    (Hom.hom ((resCoindHomEquiv.{t, u, v, w} φ X✝ Y✝).toEquiv f✝ ≫ (coindFunctor k φ).map g✝)).toLinearMap x✝
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : Ring k
inst✝ : Monoid G
A B C : TopRep k G
f : A ⟶ B
g h : B ⟶ C
⊢ Hom.hom (f ≫ (g + h)) = Hom.hom (f ≫ g + f ≫ h)

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : Ring k
inst✝ : Monoid G
A B C : TopRep k G
f : A ⟶ B
g h : B ⟶ C
⊢ Hom.hom (f ≫ (g + h)) = Hom.hom (f ≫ g + f ≫ h)
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : Ring k
inst✝ : Monoid G
A B C : TopRep k G
f g : A ⟶ B
h : B ⟶ C
⊢ Hom.hom ((f + g) ≫ h) = Hom.hom (f ≫ h + g ≫ h)

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : Ring k
inst✝ : Monoid G
A B C : TopRep k G
f g : A ⟶ B
h : B ⟶ C
⊢ Hom.hom ((f + g) ≫ h) = Hom.hom (f ≫ h + g ≫ h)
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : CommRing k
inst✝ : Monoid G
A B C : TopRep k G
r : k
f : A ⟶ B
g : B ⟶ C
x✝ : ↑A
⊢ (Hom.hom ((r • f) ≫ g)).toContinuousLinearMap x✝ = (Hom.hom (r • f ≫ g)).toContinuousLinearMap x✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : CommRing k
inst✝ : Monoid G
A B C : TopRep k G
r : k
f : A ⟶ B
g : B ⟶ C
x✝ : ↑A
⊢ (Hom.hom ((r • f) ≫ g)).toContinuousLinearMap x✝ = (Hom.hom (r • f ≫ g)).toContinuousLinearMap x✝
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : CommRing k
inst✝ : Monoid G
A B C : TopRep k G
f : A ⟶ B
r : k
g : B ⟶ C
x✝ : ↑A
⊢ (Hom.hom (f ≫ (r • g))).toContinuousLinearMap x✝ = (Hom.hom (r • f ≫ g)).toContinuousLinearMap x✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : CommRing k
inst✝ : Monoid G
A B C : TopRep k G
f : A ⟶ B
r : k
g : B ⟶ C
x✝ : ↑A
⊢ (Hom.hom (f ≫ (r • g))).toContinuousLinearMap x✝ = (Hom.hom (r • f ≫ g)).toContinuousLinearMap x✝
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
X Y : Type w
inst✝¹² : TopologicalSpace k
inst✝¹¹ : Ring k
inst✝¹⁰ : Monoid G
inst✝⁹ : AddCommGroup X
inst✝⁸ : Module k X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : IsTopologicalAddGroup X
inst✝⁵ : ContinuousSMul k X
inst✝⁴ : AddCommGroup Y
inst✝³ : Module k Y
inst✝² : TopologicalSpace Y
inst✝¹ : IsTopologicalAddGroup Y
inst✝ : ContinuousSMul k Y
ρ : ContRepresentation k G X
σ : ContRepresentation k G Y
A B C : TopRep k G
X✝ Y✝ : TopRep k G
f : X✝ ⟶ Y✝
g : G
⊢ ConcreteCategory.hom
      ({ V := TopModuleCat.of k ↑X✝, ρ := (TopModuleCat.of k ↑X✝).endRingEquiv.symm.toMonoidHom.comp ↑X✝.ρ }.ρ g ≫
        Hom.toTopModuleCatHom f) =
    ConcreteCategory.hom
      (Hom.toTopModuleCatHom f ≫
        { V := TopModuleCat.of k ↑Y✝, ρ := (TopModuleCat.of k ↑Y✝).endRingEquiv.symm.toMonoidHom.comp ↑Y✝.ρ }.ρ g)

Tactic:
;

Goal state after:
k : Type u
G : Type v
X Y : Type w
inst✝¹² : TopologicalSpace k
inst✝¹¹ : Ring k
inst✝¹⁰ : Monoid G
inst✝⁹ : AddCommGroup X
inst✝⁸ : Module k X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : IsTopologicalAddGroup X
inst✝⁵ : ContinuousSMul k X
inst✝⁴ : AddCommGroup Y
inst✝³ : Module k Y
inst✝² : TopologicalSpace Y
inst✝¹ : IsTopologicalAddGroup Y
inst✝ : ContinuousSMul k Y
ρ : ContRepresentation k G X
σ : ContRepresentation k G Y
A B C : TopRep k G
X✝ Y✝ : TopRep k G
f : X✝ ⟶ Y✝
g : G
⊢ ConcreteCategory.hom
      ({ V := TopModuleCat.of k ↑X✝, ρ := (TopModuleCat.of k ↑X✝).endRingEquiv.symm.toMonoidHom.comp ↑X✝.ρ }.ρ g ≫
        Hom.toTopModuleCatHom f) =
    ConcreteCategory.hom
      (Hom.toTopModuleCatHom f ≫
        { V := TopModuleCat.of k ↑Y✝, ρ := (TopModuleCat.of k ↑Y✝).endRingEquiv.symm.toMonoidHom.comp ↑Y✝.ρ }.ρ g)
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁹ : CommRing k
G : Type u_2
inst✝⁸ : Group G
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module k[G] V
inst✝⁴ : IsScalarTower k k[G] V
W : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module k[G] W
inst✝ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
h : ∀ (v : V), π (i v) = v
g : G
v : V
⊢ MonoidAlgebra.single g⁻¹ 1 • MonoidAlgebra.single g 1 • v = v

Tactic:
← mul_smul,

Goal state after:
k : Type u_1
inst✝⁹ : CommRing k
G : Type u_2
inst✝⁸ : Group G
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module k[G] V
inst✝⁴ : IsScalarTower k k[G] V
W : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module k[G] W
inst✝ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
h : ∀ (v : V), π (i v) = v
g : G
v : V
⊢ (MonoidAlgebra.single g⁻¹ 1 * MonoidAlgebra.single g 1) • v = v
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: case ofMonoidHom
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
π₂ : ContRepresentation R G V
toMonoidHom✝ : G →* V →L[R] V
x✝ : (fun π ↦ ⇑π.toMonoidHom) { toMonoidHom := toMonoidHom✝ } = (fun π ↦ ⇑π.toMonoidHom) π₂
⊢ { toMonoidHom := toMonoidHom✝ } = π₂

Tactic:
;

Goal state after:
case ofMonoidHom
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
π₂ : ContRepresentation R G V
toMonoidHom✝ : G →* V →L[R] V
x✝ : (fun π ↦ ⇑π.toMonoidHom) { toMonoidHom := toMonoidHom✝ } = (fun π ↦ ⇑π.toMonoidHom) π₂
⊢ { toMonoidHom := toMonoidHom✝ } = π₂