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
g : Fin 2 → G
x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
a : H × H
⊢ Eq (α := (↑B : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (chainsMap f φ).f 2 ≫ (chainsIso₂ B).hom) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) →
                  (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))
              x :
            (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u)) :
          (a : H × H) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (chainsIso₂ A).hom ≫ chainsMap₂ f φ) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) →
                  (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u))
              x :
            (↑(ModuleCat.of k (H × H →₀ (↑B : Type u))) : Type u)) :
          (a : H × H) → (↑B : Type u))
        a :
      (↑B : Type u))

Tactic:
simp [chainsMap_f, chainsIso₂]

Premises used: groupHomology.chainsIso₂, groupHomology.chainsMap_f
-- 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
h :
  ∀ (g : Fin 3 → G) (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) (a : H × H × H),
    Eq (α := (↑B : Type u))
      ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (chainsMap f φ).f 3 ≫ (chainsIso₃ B).hom) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) →
                    (↑(ModuleCat.of k (H × H × H →₀ (↑B : Type u))) : Type u))
                x :
              (↑(ModuleCat.of k (H × H × H →₀ (↑B : Type u))) : Type u)) :
            (a : H × H × H) → (↑B : Type u))
          a :
        (↑B : Type u))
      ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (chainsIso₃ A).hom ≫ chainsMap₃ f φ) :
                  (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) →
                    (↑(ModuleCat.of k (H × H × H →₀ (↑B : Type u))) : Type u))
                x :
              (↑(ModuleCat.of k (H × H × H →₀ (↑B : Type u))) : Type u)) :
            (a : H × H × H) → (↑B : Type u))
          a :
        (↑B : Type u))
⊢ (chainsMap f φ).f 3 ≫ (chainsIso₃ B).hom = (chainsIso₃ A).hom ≫ chainsMap₃ f φ

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 ⟶ res f B
g : Fin 3 → G
x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
a : H × H × H
⊢ Eq (α := (↑B : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (chainsMap f φ).f 3 ≫ (chainsIso₃ B).hom) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) →
                  (↑(ModuleCat.of k (H × H × H →₀ (↑B : Type u))) : Type u))
              x :
            (↑(ModuleCat.of k (H × H × H →₀ (↑B : Type u))) : Type u)) :
          (a : H × H × H) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((((ModuleCat.Hom.hom (ModuleCat.ofHom (lsingle g) ≫ (chainsIso₃ A).hom ≫ chainsMap₃ f φ) :
                (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) →
                  (↑(ModuleCat.of k (H × H × H →₀ (↑B : Type u))) : Type u))
              x :
            (↑(ModuleCat.of k (H × H × H →₀ (↑B : Type u))) : Type u)) :
          (a : H × H × H) → (↑B : Type u))
        a :
      (↑B : Type u))

Tactic:
simp [chainsMap_f, chainsIso₃, ← Fin.comp_tail]

Premises used: Fin.comp_tail, groupHomology.chainsIso₃, groupHomology.chainsMap_f
-- 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
⊢ cyclesMap f φ 0 ≫ (cyclesIso₀ B).hom = (cyclesIso₀ A).hom ≫ Hom.toModuleCatHom φ

Tactic:
simp [cyclesIso₀]

Premises used: groupHomology.cyclesIso₀
-- 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
⊢ (cyclesIso₀ A).inv ≫ cyclesMap f φ 0 = Hom.toModuleCatHom φ ≫ (cyclesIso₀ B).inv

Tactic:
(CommSq.vert_inv ⟨cyclesMap_comp_cyclesIso₀_hom f φ⟩).w.symm

Premises used: CategoryTheory.CommSq.vert_inv, CategoryTheory.CommSq.mk, groupHomology.cyclesMap_comp_cyclesIso₀_hom, CategoryTheory.CommSq.w, Eq.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
⊢ H0π A ≫ map f φ 0 = Hom.toModuleCatHom φ ≫ H0π B

Tactic:
simp [H0π]

Premises used: groupHomology.H0π
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B : Rep k G
f : A ⟶ B
rw :
  H0π A ≫ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom =
    H0π A ≫ (H0Iso A).hom ≫ CategoryTheory.Functor.map (coinvariantsFunctor k G) f
⊢ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom = (H0Iso A).hom ≫ CategoryTheory.Functor.map (coinvariantsFunctor k G) f

Tactic:
rw [← cancel_epi (H0π A)]

Premises used: groupHomology.H0π, CategoryTheory.cancel_epi
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B : Rep k G
f : A ⟶ B
hf :
  ∀ (x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)),
    Eq (α := (↑(Functor.obj (coinvariantsFunctor k G) B) : Type u))
      ((ModuleCat.Hom.hom (H0π A ≫ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom) :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((coinvariantsFunctor k G).obj B) : Type u))
          x :
        (↑(Functor.obj (coinvariantsFunctor k G) B) : Type u))
      ((ModuleCat.Hom.hom (H0π A ≫ (H0Iso A).hom ≫ CategoryTheory.Functor.map (coinvariantsFunctor k G) f) :
            (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((coinvariantsFunctor k G).obj B) : Type u))
          x :
        (↑(Functor.obj (coinvariantsFunctor k G) B) : Type u))
⊢ H0π A ≫ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom =
    H0π A ≫ (H0Iso A).hom ≫ CategoryTheory.Functor.map (coinvariantsFunctor k G) f

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A B : Rep k G
f : A ⟶ B
x : (↑(ModuleCat.of k (↑A : Type u)) : Type u)
⊢ Eq (α := (↑(Functor.obj (coinvariantsFunctor k G) B) : Type u))
    ((ModuleCat.Hom.hom (H0π A ≫ map (MonoidHom.id G) f 0 ≫ (H0Iso B).hom) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((coinvariantsFunctor k G).obj B) : Type u))
        x :
      (↑(Functor.obj (coinvariantsFunctor k G) B) : Type u))
    ((ModuleCat.Hom.hom (H0π A ≫ (H0Iso A).hom ≫ CategoryTheory.Functor.map (coinvariantsFunctor k G) f) :
          (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → (↑((coinvariantsFunctor k G).obj B) : Type u))
        x :
      (↑(Functor.obj (coinvariantsFunctor k G) 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_1 : Rep k G
B_1 : Rep k H
f_1 : G →* H
φ : Quiver.Hom.{?u.311982, max u (?u.311982 + 1)} A_1 (res f_1 B_1)
n : ℕ
A B : Rep k G
f : A ⟶ B
inst_3 : Epi f
Z : ModuleCat k
g h : groupHomology B 0 ⟶ Z
hgh : Eq (α := groupHomology A 0 ⟶ Z) (map (MonoidHom.id G) f 0 ≫ g) (map (MonoidHom.id G) f 0 ≫ h)
⊢ H0π A ≫ map (MonoidHom.id G) f 0 ≫ g = H0π A ≫ map (MonoidHom.id G) f 0 ≫ h

Tactic:
simp only [← cancel_epi (H0π A)] at hgh

Premises used: groupHomology.H0π, CategoryTheory.cancel_epi
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k G
B_1 : Rep k H
f_1 : G →* H
φ : Quiver.Hom.{?u.311982, max u (?u.311982 + 1)} A_1 (res f_1 B_1)
n : ℕ
A B : Rep k G
f : A ⟶ B
inst_3 : Epi f
Z : ModuleCat k
g h : groupHomology B 0 ⟶ Z
hgh : H0π A ≫ map (MonoidHom.id G) f 0 ≫ g = H0π A ≫ map (MonoidHom.id G) f 0 ≫ h
⊢ g = h

Tactic:
simp_all [cancel_epi]

Premises used: CategoryTheory.cancel_epi
-- 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) (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))
⊢ 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
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(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
φ : A ⟶ res f B
n : ℕ
simp : chainsMap₁ f φ ≫ d₁₀ B = d₁₀ A ≫ Hom.toModuleCatHom φ
⊢ chainsMap₁ f φ ≫ (shortComplexH1 B).g = (shortComplexH1 A).g ≫ Hom.toModuleCatHom φ

Tactic:
simp only [shortComplexH1]

Premises used: groupHomology.shortComplexH1
-- 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) (x : (↑A : Type u)),
    Eq (α := (↑(ModuleCat.of k (↑B : Type u)) : Type u))
      ((ModuleCat.Hom.hom (chainsMap₁ f φ ≫ d₁₀ B) ∘ₗ lsingle a :
            (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
          x :
        (↑(ModuleCat.of k (↑B : Type u)) : Type u))
      ((ModuleCat.Hom.hom (d₁₀ A ≫ Hom.toModuleCatHom φ) ∘ₗ lsingle a :
            (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
          x :
        (↑(ModuleCat.of k (↑B : Type u)) : Type u))
⊢ chainsMap₁ f φ ≫ d₁₀ B = d₁₀ A ≫ Hom.toModuleCatHom φ

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
x : (↑A : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (↑B : Type u)) : Type u))
    ((ModuleCat.Hom.hom (chainsMap₁ f φ ≫ d₁₀ B) ∘ₗ lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑B : Type u)) : Type u))
    ((ModuleCat.Hom.hom (d₁₀ A ≫ Hom.toModuleCatHom φ) ∘ₗ lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑B : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑B : Type u)) : Type u))

Tactic:
simpa [← map_inv, d₁₀] using (hom_comm_apply φ _ _).symm

Premises used: map_inv, groupHomology.d₁₀, Rep.hom_comm_apply, Eq.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
⊢ Eq (α := shortComplexH1 A ⟶ shortComplexH1 B) (mapShortComplexH1 f 0) 0

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

Premises used: CategoryTheory.ShortComplex.hom_ext, rfl
-- 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 (α := (shortComplexH1 A).X₁ ⟶ (shortComplexH1 B).X₁) (Hom.τ₁ (mapShortComplexH1 f 0)) (Hom.τ₁ 0)
refine_2 : Eq (α := (shortComplexH1 A).X₂ ⟶ (shortComplexH1 B).X₂) (Hom.τ₂ (mapShortComplexH1 f 0)) (Hom.τ₂ 0)
⊢ Eq (α := shortComplexH1 A ⟶ shortComplexH1 B) (mapShortComplexH1 f 0) 0

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

Premises used: CategoryTheory.ShortComplex.hom_ext, rfl
-- 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) (x : (↑A : Type u)) (a_1 : H × H),
    Eq (α := (↑B : Type u))
      ((((ModuleCat.Hom.hom (Hom.τ₁ (mapShortComplexH1 f 0)) ∘ₗ lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                            X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ }.X₁ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                      X₃ := ModuleCat.of k (↑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 →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G →₀ (↑A : Type u)),
                                X₃ := ModuleCat.of k (↑A : Type u), f := d₂₁ A, g := d₁₀ A, zero := ⋯ :
                                ShortComplex (ModuleCat k) }.X₁ :
                          Type u) →ₗ[k]
                        (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                                X₃ := ModuleCat.of k (↑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 →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                            X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ }.X₁ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                      X₃ := ModuleCat.of k (↑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.τ₁ (mapShortComplexH1 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.τ₁ (mapShortComplexH1 f 0)) ∘ₗ lsingle a :
                (a : (↑A : Type u)) →
                  (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                          X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ }.X₁ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                    X₃ := ModuleCat.of k (↑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 →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G →₀ (↑A : Type u)),
                              X₃ := ModuleCat.of k (↑A : Type u), f := d₂₁ A, g := d₁₀ A, zero := ⋯ :
                              ShortComplex (ModuleCat k) }.X₁ :
                        Type u) →ₗ[k]
                      (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                              X₃ := ModuleCat.of k (↑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 →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                          X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ }.X₁ :
                    Type u))
              x :
            (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                    X₃ := ModuleCat.of k (↑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
-- 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 →₀ (↑A : Type u))) (ModuleCat.of k (H × H →₀ (↑B : Type u))))
    (Hom.τ₁ (mapShortComplexH1 f 0)) (Hom.τ₁ 0)
refine_1₁ :
  ∀ (a : G × G) (x : (↑A : Type u)) (a_1 : H × H),
    Eq (α := (↑B : Type u))
      ((((ModuleCat.Hom.hom (Hom.τ₁ (mapShortComplexH1 f 0)) ∘ₗ lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                            X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ }.X₁ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                      X₃ := ModuleCat.of k (↑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 →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G →₀ (↑A : Type u)),
                                X₃ := ModuleCat.of k (↑A : Type u), f := d₂₁ A, g := d₁₀ A, zero := ⋯ :
                                ShortComplex (ModuleCat k) }.X₁ :
                          Type u) →ₗ[k]
                        (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                                X₃ := ModuleCat.of k (↑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 →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                            X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ }.X₁ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                      X₃ := ModuleCat.of k (↑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 (α := (shortComplexH1 A).X₁ ⟶ (shortComplexH1 B).X₁) (Hom.τ₁ (mapShortComplexH1 f 0)) (Hom.τ₁ 0)

Tactic:
{ simp only [shortComplexH1]
    ext
    simp }

Premises used: groupHomology.shortComplexH1
-- 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) (x : (↑A : Type u)) (a_1 : H),
    Eq (α := (↑B : Type u))
      ((((ModuleCat.Hom.hom (Hom.τ₂ (mapShortComplexH1 f 0)) ∘ₗ lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                            X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ }.X₂ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                      X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₂ :
                Type u)) :
            (a : H) → (↑B : Type u))
          a_1 :
        (↑B : Type u))
      (((((ModuleCat.Hom.hom (Hom.τ₂ 0) :
                      (↑{ X₁ := ModuleCat.of k (G × G →₀ (↑A : Type u)), X₂ := ModuleCat.of k (G →₀ (↑A : Type u)),
                                X₃ := ModuleCat.of k (↑A : Type u), f := d₂₁ A, g := d₁₀ A, zero := ⋯ :
                                ShortComplex (ModuleCat k) }.X₂ :
                          Type u) →ₗ[k]
                        (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                                X₃ := ModuleCat.of k (↑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 →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                            X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ }.X₂ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (H × H →₀ (↑B : Type u)), X₂ := ModuleCat.of k (H →₀ (↑B : Type u)),
                      X₃ := ModuleCat.of k (↑B : Type u), f := d₂₁ B, g := d₁₀ B, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₂ :
                Type u)) :
            (a : H) → (↑B : Type u))
          a_1 :
        (↑B : Type u))
⊢ Eq (α := Quiver.Hom (V := ModuleCat k) (ModuleCat.of k (G →₀ (↑A : Type u))) (ModuleCat.of k (H →₀ (↑B : Type u))))
    (Hom.τ₂ (mapShortComplexH1 f 0)) (Hom.τ₂ 0)

Tactic:
ext