-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
S : Subgroup G
A_1 : Rep.{?u.447, u, u} k ↥S
P : ProjectiveResolution (C := Rep.{u, u, u} k G) (Rep.trivial k G k)
A : Rep.{u, u, u} k ↥S
x x_1 : ℕ
h : (ComplexShape.up ℕ).Rel x x_1
f :
  (↑(HomologicalComplex.X
        (ChainComplex.linearYonedaObj
          (ProjectiveResolution.complex (Z := Functor.obj (resFunctor S.subtype) (Rep.trivial k G k))
            (Functor.mapProjectiveResolution (resFunctor S.subtype) P))
          k A)
        x) :
    Type u)
⊢ Eq.{u + 1} (α := (Opposite.unop (Opposite.op (P.complex.X x_1))).ρ.IntertwiningMap (coind.{u, u, u, u} S.subtype A).ρ)
    (Hom.hom
      ((ModuleCat.Hom.hom
            (Iso.hom ((fun (x : ℕ) ↦ (resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x) A).toModuleIso) x) ≫
              HomologicalComplex.d (P.complex.linearYonedaObj k (coind.{u, u, u, u} S.subtype A)) x x_1) :
          (a : (↑((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).X x) : Type u)) →
            (↑((P.complex.linearYonedaObj k (coind.{u, u, u, u} S.subtype A)).X x_1) : Type u))
        f))
    (Hom.hom
      ((ModuleCat.Hom.hom
            (HomologicalComplex.d
                (ChainComplex.linearYonedaObj
                  (ProjectiveResolution.complex (Z := Functor.obj (resFunctor S.subtype) (Rep.trivial k G k))
                    (Functor.mapProjectiveResolution (resFunctor S.subtype) P))
                  k A)
                x x_1 ≫
              Iso.hom ((fun (x : ℕ) ↦ (resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x) A).toModuleIso) x_1)) :
          (a : (↑((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).X x) : Type u)) →
            (↑((P.complex.linearYonedaObj k (coind.{u, u, u, u} S.subtype A)).X x_1) : Type u))
        f))
have h : ∀ (x_2 : (↑(Opposite.unop (Opposite.op (P.complex.X x_1))) : Type u)) (x_3 : G),
  Eq.{u + 1} (α := (↑A : Type u))
    ((↑((Representation.IntertwiningMap.toLinearMap
                (Hom.hom
                  ((ModuleCat.Hom.hom
                        (Iso.hom
                            ((fun (x : ℕ) ↦ (resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x) A).toModuleIso)
                              x) ≫
                          HomologicalComplex.d (P.complex.linearYonedaObj k (coind.{u, u, u, u} S.subtype A)) x x_1) :
                      (a :
                          (↑((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).X x) :
                            Type u)) →
                        (↑((P.complex.linearYonedaObj k (coind.{u, u, u, u} S.subtype A)).X x_1) : Type u))
                    f)) :
              (a : (↑(Opposite.unop (Opposite.op (P.complex.X x_1))) : Type u)) →
                (↑(coind.{u, u, u, u} S.subtype A) : Type u))
            x_2) :
        G → (↑A : Type u))
      x_3)
    ((↑((Representation.IntertwiningMap.toLinearMap
                (Hom.hom
                  ((ModuleCat.Hom.hom
                        (HomologicalComplex.d
                            (ChainComplex.linearYonedaObj
                              (ProjectiveResolution.complex (Z :=
                                Functor.obj (resFunctor S.subtype) (Rep.trivial k G k))
                                (Functor.mapProjectiveResolution (resFunctor S.subtype) P))
                              k A)
                            x x_1 ≫
                          Iso.hom
                            ((fun (x : ℕ) ↦ (resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x) A).toModuleIso)
                              x_1)) :
                      (a :
                          (↑((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).X x) :
                            Type u)) →
                        (↑((P.complex.linearYonedaObj k (coind.{u, u, u, u} S.subtype A)).X x_1) : Type u))
                    f)) :
              (a : (↑(Opposite.unop (Opposite.op (P.complex.X x_1))) : Type u)) →
                (↑(coind.{u, u, u, u} S.subtype A) : Type u))
            x_2) :
        G → (↑A : Type u))
      x_3)
Tactic: ext