awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
refine_2 :
  Hom.τ₂ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)) =
    Hom.τ₂
      (𝟙
        { X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
          X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ : ShortComplex (ModuleCat k) })
refine_2₁ :
  ∀ (a : G × G) (x : (↑A : Type u)) (a_1 : G × G),
    Eq (α := (↑A : Type u))
      ((((ModuleCat.Hom.hom (Hom.τ₂ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A))) ∘ₗ lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)),
                            X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₃ := ModuleCat.of k (G →₀ (↑A : Type u)),
                            f := d₃₂ A, g := d₂₁ A, zero := ⋯ }.X₂ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                      X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₂ :
                Type u)) :
            (a : G × G) → (↑A : Type u))
          a_1 :
        (↑A : Type u))
      ((((ModuleCat.Hom.hom
                      (Hom.τ₂
                        (𝟙
                          { X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)),
                            X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₃ := ModuleCat.of k (G →₀ (↑A : Type u)),
                            f := d₃₂ A, g := d₂₁ A, zero := ⋯ : ShortComplex (ModuleCat k) })) ∘ₗ
                    lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)),
                            X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₃ := ModuleCat.of k (G →₀ (↑A : Type u)),
                            f := d₃₂ A, g := d₂₁ A, zero := ⋯ }.X₂ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                      X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₂ :
                Type u)) :
            (a : G × G) → (↑A : Type u))
          a_1 :
        (↑A : Type u))
⊢ Hom.τ₂ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)) = Hom.τ₂ (𝟙 (shortComplexH2 A))

Tactic:
{ simp only [shortComplexH2]
    ext
    simp }

Premises used: groupHomology.shortComplexH2
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
refine_3 :
  ∀ (a : G) (x : (↑A : Type u)) (a_1 : G),
    Eq (α := (↑A : Type u))
      ((((ModuleCat.Hom.hom (Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A))) ∘ₗ lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)),
                            X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₃ := ModuleCat.of k (G →₀ (↑A : Type u)),
                            f := d₃₂ A, g := d₂₁ A, zero := ⋯ }.X₃ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                      X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₃ :
                Type u)) :
            (a : G) → (↑A : Type u))
          a_1 :
        (↑A : Type u))
      ((((ModuleCat.Hom.hom
                      (Hom.τ₃
                        (𝟙
                          { X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)),
                            X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₃ := ModuleCat.of k (G →₀ (↑A : Type u)),
                            f := d₃₂ A, g := d₂₁ A, zero := ⋯ : ShortComplex (ModuleCat k) })) ∘ₗ
                    lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)),
                            X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₃ := ModuleCat.of k (G →₀ (↑A : Type u)),
                            f := d₃₂ A, g := d₂₁ A, zero := ⋯ }.X₃ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                      X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₃ :
                Type u)) :
            (a : G) → (↑A : Type u))
          a_1 :
        (↑A : Type u))
⊢ Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)) =
    Hom.τ₃
      (𝟙
        { X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
          X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ : ShortComplex (ModuleCat k) })

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
a : G
x : (↑A : Type u)
a_1 : G
⊢ Eq (α := (↑A : Type u))
    ((((ModuleCat.Hom.hom (Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A))) ∘ₗ lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                          X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ }.X₃ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                    X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₃ :
              Type u)) :
          (a : G) → (↑A : Type u))
        a_1 :
      (↑A : Type u))
    ((((ModuleCat.Hom.hom
                    (Hom.τ₃
                      (𝟙
                        { X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)),
                          X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₃ := ModuleCat.of k (G →₀ (↑A : Type u)),
                          f := d₃₂ A, g := d₂₁ A, zero := ⋯ : ShortComplex (ModuleCat k) })) ∘ₗ
                  lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                          X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ }.X₃ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                    X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₃ :
              Type u)) :
          (a : G) → (↑A : Type u))
        a_1 :
      (↑A : Type u))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
refine_3 :
  Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)) =
    Hom.τ₃
      (𝟙
        { X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
          X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ : ShortComplex (ModuleCat k) })
refine_3₁ :
  ∀ (a : G) (x : (↑A : Type u)) (a_1 : G),
    Eq (α := (↑A : Type u))
      ((((ModuleCat.Hom.hom (Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A))) ∘ₗ lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)),
                            X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₃ := ModuleCat.of k (G →₀ (↑A : Type u)),
                            f := d₃₂ A, g := d₂₁ A, zero := ⋯ }.X₃ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                      X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₃ :
                Type u)) :
            (a : G) → (↑A : Type u))
          a_1 :
        (↑A : Type u))
      ((((ModuleCat.Hom.hom
                      (Hom.τ₃
                        (𝟙
                          { X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)),
                            X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₃ := ModuleCat.of k (G →₀ (↑A : Type u)),
                            f := d₃₂ A, g := d₂₁ A, zero := ⋯ : ShortComplex (ModuleCat k) })) ∘ₗ
                    lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)),
                            X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₃ := ModuleCat.of k (G →₀ (↑A : Type u)),
                            f := d₃₂ A, g := d₂₁ A, zero := ⋯ }.X₃ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (G × G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G × G →₀ (↑A : Type u)),
                      X₃ := ModuleCat.of k (G →₀ (↑A : Type u)), f := d₃₂ A, g := d₂₁ A, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₃ :
                Type u)) :
            (a : G) → (↑A : Type u))
          a_1 :
        (↑A : Type u))
⊢ Hom.τ₃ (mapShortComplexH2 (MonoidHom.id G) (𝟙 A)) = Hom.τ₃ (𝟙 (shortComplexH2 A))

Tactic:
{ simp only [shortComplexH2]
    ext
    simp }

Premises used: groupHomology.shortComplexH2
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k : Type u
inst : CommRing k
G H K : Type u
inst_1 : Group G
inst_2 : Group H
inst_3 : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) =
    mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ

Tactic:
ShortComplex.hom_ext _ _ ?_ ?_ ?_

Premises used: CategoryTheory.ShortComplex.hom_ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k : Type u
inst : CommRing k
G H K : Type u
inst_1 : Group G
inst_2 : Group H
inst_3 : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
refine_1 :
  (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₁ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁
refine_2 :
  (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₂ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂
refine_3 :
  (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₃ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃
⊢ mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ) =
    mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ

Tactic:
refine ShortComplex.hom_ext _ _ ?_ ?_ ?_

Premises used: CategoryTheory.ShortComplex.hom_ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k : Type u
inst : CommRing k
G H K : Type u
inst_1 : Group G
inst_2 : Group H
inst_3 : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
refine_1 :
  Hom.τ₁
      (mapShortComplexH2 (g.comp f)
        (φ ≫
          ofHom
            {
              toLinearMap :=
                (↑(Hom.hom ψ) :
                  [inst_4 : FunLike (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (↑B : Type u) (↑C : Type u)] →
                    [SemilinearMapClass (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (RingHom.id k) (↑B : Type u)
                          (↑C : Type u)] →
                      (↑B : Type u) →ₗ[k] (↑C : Type u)),
              isIntertwining' := ⋯ })) =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₁ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁

Tactic:
simp only [shortComplexH2]

Premises used: groupHomology.shortComplexH2
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k : Type u
inst : CommRing k
G H K : Type u
inst_1 : Group G
inst_2 : Group H
inst_3 : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
a : G × G × G
x : (↑A : Type u)
a_1 : K × K × K
⊢ Eq (α := (↑C : Type u))
    ((((ModuleCat.Hom.hom
                    (Hom.τ₁
                      (mapShortComplexH2 (g.comp f)
                        (φ ≫
                          ofHom
                            {
                              toLinearMap :=
                                (↑(Hom.hom ψ) :
                                  [inst_4 :
                                      FunLike (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (↑B : Type u)
                                        (↑C : Type u)] →
                                    [SemilinearMapClass (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (RingHom.id k)
                                          (↑B : Type u) (↑C : Type u)] →
                                      (↑B : Type u) →ₗ[k] (↑C : Type u)),
                              isIntertwining' := ⋯ :
                              IntertwiningMap (MonoidHom.comp B.ρ f) ((MonoidHom.comp C.ρ g).comp f) }))) ∘ₗ
                  lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)),
                          X₃ := ModuleCat.of k (K →₀ (↑C : Type u)), f := d₃₂ C, g := d₂₁ C, zero := ⋯ }.X₁ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)),
                    X₃ := ModuleCat.of k (K →₀ (↑C : Type u)), f := d₃₂ C, g := d₂₁ C, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₁ :
              Type u)) :
          (a : K × K × K) → (↑C : Type u))
        a_1 :
      (↑C : Type u))
    ((((ModuleCat.Hom.hom (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁ ∘ₗ lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)),
                          X₃ := ModuleCat.of k (K →₀ (↑C : Type u)), f := d₃₂ C, g := d₂₁ C, zero := ⋯ }.X₁ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)),
                    X₃ := ModuleCat.of k (K →₀ (↑C : Type u)), f := d₃₂ C, g := d₂₁ C, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₁ :
              Type u)) :
          (a : K × K × K) → (↑C : Type u))
        a_1 :
      (↑C : Type u))

Tactic:
simp [Prod.map]

Premises used: Prod.map
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k : Type u
inst : CommRing k
G H K : Type u
inst_1 : Group G
inst_2 : Group H
inst_3 : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
refine_2 :
  Hom.τ₂
      (mapShortComplexH2 (g.comp f)
        (φ ≫
          ofHom
            {
              toLinearMap :=
                (↑(Hom.hom ψ) :
                  [inst_4 : FunLike (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (↑B : Type u) (↑C : Type u)] →
                    [SemilinearMapClass (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (RingHom.id k) (↑B : Type u)
                          (↑C : Type u)] →
                      (↑B : Type u) →ₗ[k] (↑C : Type u)),
              isIntertwining' := ⋯ })) =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₂ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂

Tactic:
simp only [shortComplexH2]

Premises used: groupHomology.shortComplexH2
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k : Type u
inst : CommRing k
G H K : Type u
inst_1 : Group G
inst_2 : Group H
inst_3 : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
a : G × G
x : (↑A : Type u)
a_1 : K × K
⊢ Eq (α := (↑C : Type u))
    ((((ModuleCat.Hom.hom
                    (Hom.τ₂
                      (mapShortComplexH2 (g.comp f)
                        (φ ≫
                          ofHom
                            {
                              toLinearMap :=
                                (↑(Hom.hom ψ) :
                                  [inst_4 :
                                      FunLike (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (↑B : Type u)
                                        (↑C : Type u)] →
                                    [SemilinearMapClass (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (RingHom.id k)
                                          (↑B : Type u) (↑C : Type u)] →
                                      (↑B : Type u) →ₗ[k] (↑C : Type u)),
                              isIntertwining' := ⋯ :
                              IntertwiningMap (MonoidHom.comp B.ρ f) ((MonoidHom.comp C.ρ g).comp f) }))) ∘ₗ
                  lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)),
                          X₃ := ModuleCat.of k (K →₀ (↑C : Type u)), f := d₃₂ C, g := d₂₁ C, zero := ⋯ }.X₂ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)),
                    X₃ := ModuleCat.of k (K →₀ (↑C : Type u)), f := d₃₂ C, g := d₂₁ C, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₂ :
              Type u)) :
          (a : K × K) → (↑C : Type u))
        a_1 :
      (↑C : Type u))
    ((((ModuleCat.Hom.hom (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂ ∘ₗ lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)),
                          X₃ := ModuleCat.of k (K →₀ (↑C : Type u)), f := d₃₂ C, g := d₂₁ C, zero := ⋯ }.X₂ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)),
                    X₃ := ModuleCat.of k (K →₀ (↑C : Type u)), f := d₃₂ C, g := d₂₁ C, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₂ :
              Type u)) :
          (a : K × K) → (↑C : Type u))
        a_1 :
      (↑C : Type u))

Tactic:
simp [Prod.map]

Premises used: Prod.map
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k : Type u
inst : CommRing k
G H K : Type u
inst_1 : Group G
inst_2 : Group H
inst_3 : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
refine_3 :
  Hom.τ₃
      (mapShortComplexH2 (g.comp f)
        (φ ≫
          ofHom
            {
              toLinearMap :=
                (↑(Hom.hom ψ) :
                  [inst_4 : FunLike (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (↑B : Type u) (↑C : Type u)] →
                    [SemilinearMapClass (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (RingHom.id k) (↑B : Type u)
                          (↑C : Type u)] →
                      (↑B : Type u) →ₗ[k] (↑C : Type u)),
              isIntertwining' := ⋯ })) =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₃ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃

Tactic:
simp only [shortComplexH2]

Premises used: groupHomology.shortComplexH2
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k : Type u
inst : CommRing k
G H K : Type u
inst_1 : Group G
inst_2 : Group H
inst_3 : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
a : G
x : (↑A : Type u)
a_1 : K
⊢ Eq (α := (↑C : Type u))
    ((((ModuleCat.Hom.hom
                    (Hom.τ₃
                      (mapShortComplexH2 (g.comp f)
                        (φ ≫
                          ofHom
                            {
                              toLinearMap :=
                                (↑(Hom.hom ψ) :
                                  [inst_4 :
                                      FunLike (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (↑B : Type u)
                                        (↑C : Type u)] →
                                    [SemilinearMapClass (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (RingHom.id k)
                                          (↑B : Type u) (↑C : Type u)] →
                                      (↑B : Type u) →ₗ[k] (↑C : Type u)),
                              isIntertwining' := ⋯ :
                              IntertwiningMap (MonoidHom.comp B.ρ f) ((MonoidHom.comp C.ρ g).comp f) }))) ∘ₗ
                  lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)),
                          X₃ := ModuleCat.of k (K →₀ (↑C : Type u)), f := d₃₂ C, g := d₂₁ C, zero := ⋯ }.X₃ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)),
                    X₃ := ModuleCat.of k (K →₀ (↑C : Type u)), f := d₃₂ C, g := d₂₁ C, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₃ :
              Type u)) :
          (a : K) → (↑C : Type u))
        a_1 :
      (↑C : Type u))
    ((((ModuleCat.Hom.hom (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃ ∘ₗ lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)),
                          X₃ := ModuleCat.of k (K →₀ (↑C : Type u)), f := d₃₂ C, g := d₂₁ C, zero := ⋯ }.X₃ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)),
                    X₃ := ModuleCat.of k (K →₀ (↑C : Type u)), f := d₃₂ C, g := d₂₁ C, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₃ :
              Type u)) :
          (a : K) → (↑C : Type u))
        a_1 :
      (↑C : Type u))

Tactic:
simp [Prod.map]

Premises used: Prod.map
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
⊢ mapShortComplexH2 (MonoidHom.id G) (φ ≫ ψ) =
    CategoryStruct.comp (Y := shortComplexH2 B) (mapShortComplexH2 (MonoidHom.id G) φ)
      (mapShortComplexH2 (MonoidHom.id G) ψ)

Tactic:
mapShortComplexH2_comp (MonoidHom.id G) (MonoidHom.id G) _ _

Premises used: groupHomology.mapShortComplexH2_comp, SemilinearMapClass.semilinearMap, MonoidHom.id