-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro
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_1 : (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)
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)
⊢ 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))

Tactic:
ext