-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality (goal)
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)
⊢ 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)
have 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, sorry⟩) :
    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, sorry⟩) :
    H)
Tactic: fin_cases x
Cleared hypotheses: x