awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst_3 : S.Normal
x : ↥(cycles₁ (A.quotientToCoinvariants S))
y : (↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S))) : Type u)
hy :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ ((A.toCoinvariants S).ofQuotient S)))
          (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv ((A.toCoinvariants S).resOfQuotientIso S))) :
        (a : (↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S))) : Type u)) →
          (↑(ModuleCat.of k ↥(cycles₁ ((A.toCoinvariants S).ofQuotient S))) : Type u))
      y =
    x
Y : G →₀ (↑A : Type u)
hY :
  mapRange
      (⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) :
        (a : (↑A : Type u)) → Coinvariants (MonoidHom.comp A.ρ S.subtype))
      ⋯ Y =
    (↑y : G →₀ (↑(A.toCoinvariants S) : Type u))
⊢ Membership.mem (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u)) (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d₁₀ A) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        Y :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))

Tactic:
have : d₁₀ _ Y ∈ Coinvariants.ker (A.ρ.comp S.subtype) := by
    have h' := congr($((mapShortComplexH1 (B := toCoinvariants A S)
      (MonoidHom.id G) (toCoinvariantsMkQ A S)).comm₂₃) Y)
    simp_all [shortComplexH1, ← Coinvariants.mk_eq_zero]
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst_3 : S.Normal
x : ↥(cycles₁ (A.quotientToCoinvariants S))
y : (↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S))) : Type u)
hy :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ ((A.toCoinvariants S).ofQuotient S)))
          (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv ((A.toCoinvariants S).resOfQuotientIso S))) :
        (a : (↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S))) : Type u)) →
          (↑(ModuleCat.of k ↥(cycles₁ ((A.toCoinvariants S).ofQuotient S))) : Type u))
      y =
    x
Y : G →₀ (↑A : Type u)
hY :
  mapRange
      (⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) :
        (a : (↑A : Type u)) → Coinvariants (MonoidHom.comp A.ρ S.subtype))
      ⋯ Y =
    (↑y : G →₀ (↑(A.toCoinvariants S) : Type u))
this :
  Membership.mem (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u)) (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d₁₀ A) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        Y :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
Z : ↥S →₀ (↑A : Type u)
hZ :
  Eq (α := (↑(ModuleCat.of k ↥(Coinvariants.ker (res S.subtype A).ρ)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chains₁ToCoinvariantsKer (res S.subtype A)) :
          (a : (↑(ModuleCat.of k (↥S →₀ (↑(res S.subtype A) : Type u))) : Type u)) →
            (↑(ModuleCat.of k ↥(Coinvariants.ker (res S.subtype A).ρ)) : Type u))
        Z :
      (↑(ModuleCat.of k ↥(Coinvariants.ker (res S.subtype A).ρ)) : Type u))
    (Subtype.mk (p := fun (x : (↑(res S.subtype A) : Type u)) ↦ x ∈ Coinvariants.ker (res S.subtype A).ρ)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (d₁₀ A) :
            (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          Y)
        this :
      ↥(Coinvariants.ker (res S.subtype A).ρ))
⊢ Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d₁₀ A) :
          (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        (Y - mapDomain (⇑S.subtype : (a : ↥S) → G) Z) :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    (0 : (↑(ModuleCat.of k (↑A : Type u)) : Type u))

Tactic:
have H : d₁₀ A (Y - mapDomain S.subtype Z) = 0 := by
    simpa [map_sub, sub_eq_zero, chains₁ToCoinvariantsKer, - LinearMap.sub_apply, d₁₀,
      sum_mapDomain_index_inj] using Subtype.ext_iff.1 hZ.symm
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
hf :
  ∀ (a : G × G × G) (x : (↑A : Type u)),
    Eq (α := (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))
      ((ModuleCat.Hom.hom (chainsMap₃ f φ ≫ d₃₂ B) ∘ₗ lsingle a :
            (a : (↑A : Type u)) → (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))
          x :
        (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))
      ((ModuleCat.Hom.hom (d₃₂ A ≫ chainsMap₂ f φ) ∘ₗ lsingle a :
            (a : (↑A : Type u)) → (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))
          x :
        (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))
⊢ chainsMap₃ f φ ≫ d₃₂ B = d₃₂ A ≫ chainsMap₂ f φ

Tactic:
ext : 3
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
a : G × G × G
x : (↑A : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))
    ((ModuleCat.Hom.hom (chainsMap₃ f φ ≫ d₃₂ B) ∘ₗ lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))
        x :
      (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))
    ((ModuleCat.Hom.hom (d₃₂ A ≫ chainsMap₂ f φ) ∘ₗ lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))
        x :
      (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))

Tactic:
simpa [d₃₂, map_add, map_sub, ← map_inv]
      using congr(Finsupp.single _ $((hom_comm_apply φ _ _).symm))

Premises used: groupHomology.d₃₂, map_inv, map_sub, map_add
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
a : G × G
x : (↑A : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))
    ((ModuleCat.Hom.hom (chainsMap₂ f φ ≫ d₂₁ B) ∘ₗ lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))
        x :
      (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))
    ((ModuleCat.Hom.hom (d₂₁ A ≫ chainsMap₁ f φ) ∘ₗ lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))
        x :
      (↑(ModuleCat.of k (H →₀ (↑B : Type u))) : Type u))

Tactic:
simpa [d₂₁, map_add, map_sub, ← map_inv]
      using congr(Finsupp.single _ $((hom_comm_apply φ _ _).symm))

Premises used: map_inv, map_sub, map_add, groupHomology.d₂₁
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
⊢ Eq (α := shortComplexH2 A ⟶ shortComplexH2 B) (mapShortComplexH2 f 0) 0

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

Premises used: CategoryTheory.ShortComplex.hom_ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
refine_1 : Eq (α := (shortComplexH2 A).X₁ ⟶ (shortComplexH2 B).X₁) (Hom.τ₁ (mapShortComplexH2 f 0)) (Hom.τ₁ 0)
refine_2 : Eq (α := (shortComplexH2 A).X₂ ⟶ (shortComplexH2 B).X₂) (Hom.τ₂ (mapShortComplexH2 f 0)) (Hom.τ₂ 0)
refine_3 : Eq (α := (shortComplexH2 A).X₃ ⟶ (shortComplexH2 B).X₃) (Hom.τ₃ (mapShortComplexH2 f 0)) (Hom.τ₃ 0)
⊢ Eq (α := shortComplexH2 A ⟶ shortComplexH2 B) (mapShortComplexH2 f 0) 0

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

Premises used: CategoryTheory.ShortComplex.hom_ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
refine_1 :
  ∀ (a : G × G × G) (x : (↑A : Type u)) (a_1 : H × H × H),
    Eq (α := (↑B : Type u))
      ((((ModuleCat.Hom.hom (Hom.τ₁ (mapShortComplexH2 f 0)) ∘ₗ lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)),
                            X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₃ := ModuleCat.of k (H →₀ (↑B : Type u)),
                            f := d₃₂ B, g := d₂₁ B, zero := ⋯ }.X₁ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                      X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₁ :
                Type u)) :
            (a : H × H × H) → (↑B : Type u))
          a_1 :
        (↑B : Type u))
      (((((ModuleCat.Hom.hom (Hom.τ₁ 0) :
                      (↑{ 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) →ₗ[k]
                        (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)),
                                X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                                X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ :
                                ShortComplex (ModuleCat k) }.X₁ :
                          Type u)) ∘ₗ
                    lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)),
                            X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₃ := ModuleCat.of k (H →₀ (↑B : Type u)),
                            f := d₃₂ B, g := d₂₁ B, zero := ⋯ }.X₁ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                      X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₁ :
                Type u)) :
            (a : H × H × H) → (↑B : Type u))
          a_1 :
        (↑B : Type u))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k (G × G × G →₀ (↑A : Type u)))
      (ModuleCat.of k (H × H × H →₀ (↑B : Type u))))
    (Hom.τ₁ (mapShortComplexH2 f 0)) (Hom.τ₁ 0)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
a : G × G × G
x : (↑A : Type u)
a_1 : H × H × H
⊢ Eq (α := (↑B : Type u))
    ((((ModuleCat.Hom.hom (Hom.τ₁ (mapShortComplexH2 f 0)) ∘ₗ lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                          X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ }.X₁ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                    X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₁ :
              Type u)) :
          (a : H × H × H) → (↑B : Type u))
        a_1 :
      (↑B : Type u))
    (((((ModuleCat.Hom.hom (Hom.τ₁ 0) :
                    (↑{ 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) →ₗ[k]
                      (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)),
                              X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₃ := ModuleCat.of k (H →₀ (↑B : Type u)),
                              f := d₃₂ B, g := d₂₁ B, zero := ⋯ : ShortComplex (ModuleCat k) }.X₁ :
                        Type u)) ∘ₗ
                  lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                          X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ }.X₁ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                    X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₁ :
              Type u)) :
          (a : H × H × H) → (↑B : Type u))
        a_1 :
      (↑B : Type u))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
refine_1 :
  Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k (G × G × G →₀ (↑A : Type u)))
      (ModuleCat.of k (H × H × H →₀ (↑B : Type u))))
    (Hom.τ₁ (mapShortComplexH2 f 0)) (Hom.τ₁ 0)
refine_1₁ :
  ∀ (a : G × G × G) (x : (↑A : Type u)) (a_1 : H × H × H),
    Eq (α := (↑B : Type u))
      ((((ModuleCat.Hom.hom (Hom.τ₁ (mapShortComplexH2 f 0)) ∘ₗ lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)),
                            X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₃ := ModuleCat.of k (H →₀ (↑B : Type u)),
                            f := d₃₂ B, g := d₂₁ B, zero := ⋯ }.X₁ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                      X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₁ :
                Type u)) :
            (a : H × H × H) → (↑B : Type u))
          a_1 :
        (↑B : Type u))
      (((((ModuleCat.Hom.hom (Hom.τ₁ 0) :
                      (↑{ 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) →ₗ[k]
                        (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)),
                                X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                                X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ :
                                ShortComplex (ModuleCat k) }.X₁ :
                          Type u)) ∘ₗ
                    lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)),
                            X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₃ := ModuleCat.of k (H →₀ (↑B : Type u)),
                            f := d₃₂ B, g := d₂₁ B, zero := ⋯ }.X₁ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                      X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₁ :
                Type u)) :
            (a : H × H × H) → (↑B : Type u))
          a_1 :
        (↑B : Type u))
⊢ Eq (α := (shortComplexH2 A).X₁ ⟶ (shortComplexH2 B).X₁) (Hom.τ₁ (mapShortComplexH2 f 0)) (Hom.τ₁ 0)

Tactic:
{ simp only [shortComplexH2]
    ext
    simp }

Premises used: groupHomology.shortComplexH2
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
refine_2 :
  ∀ (a : G × G) (x : (↑A : Type u)) (a_1 : H × H),
    Eq (α := (↑B : Type u))
      ((((ModuleCat.Hom.hom (Hom.τ₂ (mapShortComplexH2 f 0)) ∘ₗ lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)),
                            X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₃ := ModuleCat.of k (H →₀ (↑B : Type u)),
                            f := d₃₂ B, g := d₂₁ B, zero := ⋯ }.X₂ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                      X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₂ :
                Type u)) :
            (a : H × H) → (↑B : Type u))
          a_1 :
        (↑B : Type u))
      (((((ModuleCat.Hom.hom (Hom.τ₂ 0) :
                      (↑{ 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) →ₗ[k]
                        (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)),
                                X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                                X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ :
                                ShortComplex (ModuleCat k) }.X₂ :
                          Type u)) ∘ₗ
                    lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)),
                            X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₃ := ModuleCat.of k (H →₀ (↑B : Type u)),
                            f := d₃₂ B, g := d₂₁ B, zero := ⋯ }.X₂ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                      X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₂ :
                Type u)) :
            (a : H × H) → (↑B : Type u))
          a_1 :
        (↑B : Type u))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k (G × G →₀ (↑A : Type u))) (ModuleCat.of k (H × H →₀ (↑B : Type u))))
    (Hom.τ₂ (mapShortComplexH2 f 0)) (Hom.τ₂ 0)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
a : G × G
x : (↑A : Type u)
a_1 : H × H
⊢ Eq (α := (↑B : Type u))
    ((((ModuleCat.Hom.hom (Hom.τ₂ (mapShortComplexH2 f 0)) ∘ₗ lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                          X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ }.X₂ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                    X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₂ :
              Type u)) :
          (a : H × H) → (↑B : Type u))
        a_1 :
      (↑B : Type u))
    (((((ModuleCat.Hom.hom (Hom.τ₂ 0) :
                    (↑{ 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) →ₗ[k]
                      (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)),
                              X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₃ := ModuleCat.of k (H →₀ (↑B : Type u)),
                              f := d₃₂ B, g := d₂₁ B, zero := ⋯ : ShortComplex (ModuleCat k) }.X₂ :
                        Type u)) ∘ₗ
                  lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                          X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ }.X₂ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (H × H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H × H →₀ (↑B : Type u)),
                    X₃ := ModuleCat.of k (H →₀ (↑B : Type u)), f := d₃₂ B, g := d₂₁ B, zero := ⋯ :
                    ShortComplex (ModuleCat k) }.X₂ :
              Type u)) :
          (a : H × H) → (↑B : Type u))
        a_1 :
      (↑B : Type u))

Tactic:
simp