-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
S : Subgroup G
inst_2 : S.Normal
inst_3 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ (↑A : Type u)
hxc : x ∈ cycles₁ A
hx :
  Eq (α := (↑(H1 (A.ofQuotient S)) : Type u))
    (((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(cycles₁ (A.ofQuotient S))) (Y :=
              groupHomology (A.ofQuotient S) 1) (H1π (A.ofQuotient S)) :
            (↑(ModuleCat.of k ↥(cycles₁ (A.ofQuotient S))) : Type u) →ₗ[k]
              (↑(groupHomology (A.ofQuotient S) 1) : Type u)) :
          (a : ↥(cycles₁ (A.ofQuotient S))) → (↑(groupHomology (A.ofQuotient S) 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ (A.ofQuotient S)))
                (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S))) :
              (a : ↥(cycles₁ A)) → ↥(cycles₁ (A.ofQuotient S)))
            (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ cycles₁ A) x hxc) :
          ↥(cycles₁ (A.ofQuotient S))) :
      (↑(groupHomology (A.ofQuotient S) 1) : Type u))
    (0 : (↑(H1 (A.ofQuotient S)) : Type u))
y : (↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) : Type u)
hy :
  Eq (α := G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))
    ((ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S)) :
          (a : (↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) : Type u)) →
            G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))
        y :
      G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))
    ((↑((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ (A.ofQuotient S)))
                (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S))) :
              (a : ↥(cycles₁ A)) → ↥(cycles₁ (A.ofQuotient S)))
            (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ cycles₁ A) x hxc)) :
        G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)) :
      G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))
s : (b : G ⧸ S) → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S : (a : G) → G ⧸ S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ (↑A : Type u) :=
  (lmapDomain (↑A : Type u) k (Prod.map s s) : (a : (G ⧸ S) × G ⧸ S →₀ (↑A : Type u)) → G × G →₀ (↑A : Type u)) y
hz :
  Eq (α := G ⧸ S →₀ (↑A : Type u))
    ((lmapDomain (↑A : Type u) k (⇑(QuotientGroup.mk' S) : (a : G) → G ⧸ S) :
          (a : G →₀ (↑A : Type u)) → G ⧸ S →₀ (↑A : Type u))
        ((ModuleCat.Hom.hom (d₂₁ A) :
            (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
              (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
          z) :
      G ⧸ S →₀ (↑A : Type u))
    ((ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S)) :
          (a : (↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) : Type u))
        y :
      (↑(ModuleCat.of k (G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) : Type u))
v : G →₀ (↑A : Type u) :=
  HSub.hSub (β := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) x
    ((ModuleCat.Hom.hom (d₂₁ A) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
        z :
      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun (g : G) ↦ (s (↑g : G ⧸ S), (s (↑g : G ⧸ S))⁻¹ * g)
he : Function.Injective e
ve : G × G →₀ (↑A : Type u) := mapDomain e v
hS :
  (↑(HAdd.hAdd (β := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) v
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (d₂₁ A) :
                  (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
                    (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
                ve :
              (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))).support :
      Set G) ⊆
    (↑S : Set G)
this :
  Eq (α := (↑A : Type u))
    ((HAdd.hAdd (β := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) v
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (d₂₁ A) :
                (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
                  (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
              ve :
            (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))).sum
      fun (g : G) (a : (↑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))
        a)
    ((HAdd.hAdd (β := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) v
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (d₂₁ A) :
                (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
                  (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
              ve :
            (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))).sum
      fun (x : G) (a : (↑A : Type u)) ↦ a)
w :
  ∀
    (this :
      Eq (α := (↑A : Type u))
        (sum (α := ↥S)
          (comapDomain (Subtype.val (p := fun (x : G) ↦ x ∈ S))
            (HAdd.hAdd (β := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) v
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                      ModuleCat.carrier) (d₂₁ A) :
                    (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
                      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
                  ve :
                (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)))
            ⋯)
          ((fun (g : G) (a : (↑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))
                a) ∘
            Subtype.val (p := fun (x : G) ↦ x ∈ S)))
        ((HAdd.hAdd (β := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) v
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                      ModuleCat.carrier) (d₂₁ A) :
                    (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
                      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
                  ve :
                (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))).sum
          fun (x : G) (a : (↑A : Type u)) ↦ a)),
    Set.BijOn (α := ↥S) (Subtype.val (p := fun (x : G) ↦ x ∈ S))
      (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹'
        (↑(HAdd.hAdd (β := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) v
                ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                        ModuleCat.carrier) (d₂₁ A) :
                      (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
                        (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
                    ve :
                  (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))).support :
          Set G))
      (↑(HAdd.hAdd (β := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) v
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                      ModuleCat.carrier) (d₂₁ A) :
                    (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
                      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
                  ve :
                (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))).support :
        Set G)
w₁ :
  Set.BijOn (α := ↥S) (Subtype.val (p := fun (x : G) ↦ x ∈ S))
    (Subtype.val (p := fun (x : G) ↦ x ∈ S) ⁻¹'
      (↑(HAdd.hAdd (β := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) v
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                      ModuleCat.carrier) (d₂₁ A) :
                    (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
                      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
                  ve :
                (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))).support :
        Set G))
    (↑(HAdd.hAdd (β := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) v
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (d₂₁ A) :
                  (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
                    (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
                ve :
              (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))).support :
      Set G)
⊢ Eq (α := (↑(res S.subtype A) : Type u))
    (sum
      (comapDomain (Subtype.val (p := fun (x : G) ↦ x ∈ S))
        (HAdd.hAdd (β := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) v
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (d₂₁ A) :
                (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
                  (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
              ve :
            (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)))
        ⋯)
      fun (g : ↥S) (a : (↑(res S.subtype A) : Type u)) ↦
      ((((res S.subtype A).ρ : (a : ↥S) → (↑(res S.subtype A) : Type u) →ₗ[k] (↑(res S.subtype A) : Type u)) g⁻¹ :
            (↑(res S.subtype A) : Type u) →ₗ[k] (↑(res S.subtype A) : Type u)) :
          (a : (↑(res S.subtype A) : Type u)) → (↑(res S.subtype A) : Type u))
        a)
    (sum
      (comapDomain (Subtype.val (p := fun (x : G) ↦ x ∈ S))
        (HAdd.hAdd (β := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) v
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (d₂₁ A) :
                (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
                  (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
              ve :
            (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)))
        ⋯)
      fun (x : ↥S) (a : (↑(res S.subtype A) : Type u)) ↦ a)

Tactic:
rwa [← sum_comapDomain, ← sum_comapDomain (g := fun _ a => a)] at this

Premises used: Finsupp.sum_comapDomain