-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
S : Subgroup G
inst_2 : S.Normal
x : ↥(cocycles₁ A)
hx :
  Eq (α := (↑(groupCohomology (res S.subtype A) 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1π (res S.subtype A)) :
          (a : ↥(cocycles₁ (res S.subtype A))) → (↑(groupCohomology (res S.subtype A) 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (mapCocycles₁ S.subtype (𝟙 (res S.subtype A))) :
              (a : ↥(cocycles₁ A)) → ↥(cocycles₁ (res S.subtype A)))
            x :
          ↥(cocycles₁ (res S.subtype A))) :
      (↑(groupCohomology (res S.subtype A) 1) : Type u))
    (0 : (↑(groupCohomology (res S.subtype A) 1) : Type u))
y : (↑A : Type u)
hy :
  Eq (α := ↥S → (↑(res S.subtype A) : Type u))
    ((ModuleCat.Hom.hom (d₀₁ (res S.subtype A)) :
          (a : (↑(ModuleCat.of k (↑(res S.subtype A) : Type u)) : Type u)) → ↥S → (↑(res S.subtype A) : Type u))
        y :
      ↥S → (↑(res S.subtype A) : Type u))
    ((⇑((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (mapCocycles₁ S.subtype (𝟙 (res S.subtype A))) :
                (a : ↥(cocycles₁ A)) → ↥(cocycles₁ (res S.subtype A)))
              x :
            ↥(cocycles₁ (res S.subtype A))) :
        (a : ↥S) → (↑(res S.subtype A) : Type u)) :
      (a : ↥S) → (↑(res S.subtype A) : Type u))
h1 :
  ∀ (g h : G),
    (x : (a : G) → (↑A : Type u)) (g * h) =
      HAdd.hAdd (α := (↑A : Type u)) (β := (↑A : Type u))
        ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            ((x : (a : G) → (↑A : Type u)) h : (↑A : Type u)) :
          (↑A : Type u))
        ((x : (a : G) → (↑A : Type u)) g : (↑A : Type u))
h2 :
  ∀ s ∈ S,
    (x : (a : G) → (↑A : Type u)) s =
      HSub.hSub (α := (↑A : Type u))
        ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) s : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            y :
          (↑A : Type u))
        y
h :
  ∀ (g : G),
    (ModuleCat.Hom.hom (d₀₁ A) : (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → G → (↑A : Type u)) y g =
      HSub.hSub (α := (a : G) → (↑A : Type u)) (β := (a : G) → (↑A : Type u)) (⇑x : (a : G) → (↑A : Type u))
        (⇑(((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (X := ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) (Y :=
                    ModuleCat.of k ↥(cocycles₁ (of A.ρ)))
                    (mapCocycles₁ (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) :
                      Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S)))
                        (ModuleCat.of k ↥(cocycles₁ (of A.ρ)))) :
                  (↑(ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) : Type u) →ₗ[k]
                    (↑(ModuleCat.of k ↥(cocycles₁ (of A.ρ))) : Type u)) :
                (a : ↥(cocycles₁ (A.quotientToInvariants S))) → ↥(cocycles₁ (of A.ρ)))
              (Subtype.mk (p := fun (x : G ⧸ S → ↥(invariants (MonoidHom.comp A.ρ S.subtype))) ↦
                Membership.mem (γ := Submodule k (G ⧸ S → ↥(invariants (MonoidHom.comp A.ρ S.subtype))))
                  (cocycles₁ (A.quotientToInvariants S)) x)
                (fun (g : G ⧸ S) ↦
                  Quotient.liftOn' g
                    (fun (g : G) ↦
                      Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ invariants (MonoidHom.comp A.ρ S.subtype))
                        (HSub.hSub (β := (↑A : Type u)) ((↑x : G → (↑A : Type u)) g)
                            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g :
                                    (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                                  (a : (↑A : Type u)) → (↑A : Type u))
                                y :
                              (↑A : Type u)) +
                          y)
                        ⋯)
                    ⋯)
                ⋯)) :
          (a : G) → (↑A : Type u))
        g
⊢ (ModuleCat.Hom.hom (d₀₁ A) : (a : (↑(ModuleCat.of k (↑A : Type u)) : Type u)) → G → (↑A : Type u)) y =
    HSub.hSub (α := (a : G) → (↑A : Type u)) (⇑x : (a : G) → (↑A : Type u))
      (⇑(((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (X := ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) (Y :=
                  ModuleCat.of k ↥(cocycles₁ (of A.ρ)))
                  (mapCocycles₁ (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) :
                    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S)))
                      (ModuleCat.of k ↥(cocycles₁ (of A.ρ)))) :
                (↑(ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) : Type u) →ₗ[k]
                  (↑(ModuleCat.of k ↥(cocycles₁ (of A.ρ))) : Type u)) :
              (a : ↥(cocycles₁ (A.quotientToInvariants S))) → ↥(cocycles₁ (of A.ρ)))
            (Subtype.mk (p := fun (x : G ⧸ S → ↥(invariants (MonoidHom.comp A.ρ S.subtype))) ↦
              Membership.mem (γ := Submodule k (G ⧸ S → ↥(invariants (MonoidHom.comp A.ρ S.subtype))))
                (cocycles₁ (A.quotientToInvariants S)) x)
              (fun (g : G ⧸ S) ↦
                Quotient.liftOn' g
                  (fun (g : G) ↦
                    Subtype.mk (p := fun (x : (↑A : Type u)) ↦ x ∈ invariants (MonoidHom.comp A.ρ S.subtype))
                      (HSub.hSub (β := (↑A : Type u)) ((↑x : G → (↑A : Type u)) g)
                          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g :
                                  (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                                (a : (↑A : Type u)) → (↑A : Type u))
                              y :
                            (↑A : Type u)) +
                        y)
                      ⋯)
                  ⋯)
              ⋯)) :
        (a : G) → (↑A : Type u))

Tactic:
ext g

Premises used: CategoryTheory.ShortComplex.g