-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g_1 : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g_1) x
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
a : (↑A : Type u)
g : G
subst :
  Eq (α := (↑((moduleCatChainComplex A g_1).X j) : Type u))
    (((LinearMap.compr₂
                  (A.coinvariantsTensorMk
                    (HomologicalComplex.X (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯)) (j + 1)))
                  (ModuleCat.Hom.hom
                    (CategoryStruct.comp (Y := (moduleCatChainComplex A g_1).X (j + 1))
                      (Iso.hom ((fun (x : ℕ) ↦ A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) (j + 1)))
                      ((moduleCatChainComplex A g_1).d (j + 1) j))) :
                (a : (↑A : Type u)) →
                  (↑((resolution k g_1⁻¹ ⋯).complex.X (j + 1)) : Type u) →ₗ[k]
                    (↑((moduleCatChainComplex A g_1).X j) : Type u))
              a ∘ₗ
            lsingle g :
          (a : k) → (↑((moduleCatChainComplex A g_1).X j) : Type u))
        1 :
      (↑((moduleCatChainComplex A g_1).X j) : Type u))
    (((LinearMap.compr₂
                  (A.coinvariantsTensorMk
                    (HomologicalComplex.X (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯)) (j + 1)))
                  (ModuleCat.Hom.hom
                    ((HomologicalComplex.coinvariantsTensorObj A
                            (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯))).d
                        (j + 1) j ≫
                      Iso.hom ((fun (x : ℕ) ↦ A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) j))) :
                (a : (↑A : Type u)) →
                  (↑((resolution k g_1⁻¹ ⋯).complex.X (j + 1)) : Type u) →ₗ[k]
                    (↑((moduleCatChainComplex A g_1).X j) : Type u))
              a ∘ₗ
            lsingle g :
          (a : k) → (↑((moduleCatChainComplex A g_1).X j) : Type u))
        1 :
      (↑((moduleCatChainComplex A g_1).X j) : Type u))
⊢ Eq (α := (↑((moduleCatChainComplex A g_1).X j) : Type u))
    (((LinearMap.compr₂
                  (A.coinvariantsTensorMk
                    (HomologicalComplex.X (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯)) i))
                  (ModuleCat.Hom.hom
                    (Iso.hom ((fun (x : ℕ) ↦ A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) i) ≫
                      (moduleCatChainComplex A g_1).d i j)) :
                (a : (↑A : Type u)) →
                  (↑((resolution k g_1⁻¹ ⋯).complex.X i) : Type u) →ₗ[k]
                    (↑((moduleCatChainComplex A g_1).X j) : Type u))
              a ∘ₗ
            lsingle g :
          (a : k) → (↑((moduleCatChainComplex A g_1).X j) : Type u))
        1 :
      (↑((moduleCatChainComplex A g_1).X j) : Type u))
    (((LinearMap.compr₂
                  (A.coinvariantsTensorMk
                    (HomologicalComplex.X (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯)) i))
                  (ModuleCat.Hom.hom
                    ((HomologicalComplex.coinvariantsTensorObj A
                            (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯))).d
                        i j ≫
                      Iso.hom ((fun (x : ℕ) ↦ A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) j))) :
                (a : (↑A : Type u)) →
                  (↑((resolution k g_1⁻¹ ⋯).complex.X i) : Type u) →ₗ[k]
                    (↑((moduleCatChainComplex A g_1).X j) : Type u))
              a ∘ₗ
            lsingle g :
          (a : k) → (↑((moduleCatChainComplex A g_1).X j) : Type u))
        1 :
      (↑((moduleCatChainComplex A g_1).X j) : Type u))

Tactic:
subst h