-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic (goal)
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
⊢ 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))
have subst : Eq (α := (↑((moduleCatChainComplex A g_1).X j) : Type u))
  (((LinearMap.compr₂
                (A.coinvariantsTensorMk
                  (HomologicalComplex.X (ProjectiveResolution.complex (resolution k g_1⁻¹ sorry)) (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⁻¹ sorry).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⁻¹ sorry)) (j + 1)))
                (ModuleCat.Hom.hom
                  ((HomologicalComplex.coinvariantsTensorObj A (ProjectiveResolution.complex (resolution k g_1⁻¹ sorry))).d
                      (j + 1) j ≫
                    Iso.hom ((fun (x : ℕ) ↦ A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) j))) :
              (a : (↑A : Type u)) →
                (↑((resolution k g_1⁻¹ sorry).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))
Tactic: subst h
Cleared hypotheses: i, h