-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
x_1 : (↑((inhomogeneousCochains A).X 3) : Type u)
g : G × G × G
x : Fin 3
hf :
  Eq (α := H)
    ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
        ((Equiv.symm
              (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
            (a : G × G × G) → (i : Fin (2 + 1)) → G)
          g)
        ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      H)
    ((Equiv.symm
            (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
              ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
          (a : H × H × H) → (i : Fin (2 + 1)) → H)
        (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g)
        ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨0, ⋯⟩) :
      H)
hf₁ :
  Eq (α := H)
    ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
        ((Equiv.symm
              (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
            (a : G × G × G) → (i : Fin (2 + 1)) → G)
          g)
        ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨1, ⋯⟩) :
      H)
    ((Equiv.symm
            (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
              ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
          (a : H × H × H) → (i : Fin (2 + 1)) → H)
        (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g)
        ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨1, ⋯⟩) :
      H)
hf₂ :
  Eq (α := H)
    ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
        ((Equiv.symm
              (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
            (a : G × G × G) → (i : Fin (2 + 1)) → G)
          g)
        ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨2, ⋯⟩) :
      H)
    ((Equiv.symm
            (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
              ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
          (a : H × H × H) → (i : Fin (2 + 1)) → H)
        (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g)
        ((fun (i : Fin ({ len := 2 : SimplexCategory }.len + 1)) ↦ i) ⟨2, ⋯⟩) :
      H)
⊢ Eq (α := H)
    ((fun (x : Fin 3 → G) ↦ ((⇑f : (a : G) → H) ∘ x : Fin 3 → H))
        ((Equiv.symm
              (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ G))
                ((Equiv.refl G).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ G))) :
            (a : G × G × G) → (i : Fin (2 + 1)) → G)
          g)
        x :
      H)
    ((Equiv.symm
            (Equiv.trans (Equiv.symm (Fin.consEquiv.{u} (n := 2) fun (a : Fin 3) ↦ H))
              ((Equiv.refl H).prodCongr (piFinTwoEquiv fun (x : Fin 2) ↦ H))) :
          (a : H × H × H) → (i : Fin (2 + 1)) → H)
        (Prod.map (⇑f : (a : G) → H) (Prod.map (⇑f : (a : G) → H) (⇑f : (a : G) → H)) g) x :
      H)

Tactic:
fin_cases x