Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
z : ↥(cycles₁ (res S.subtype (A.toCoinvariants S)))
hz :
  (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
w : ↑(ModuleCat.of k (G × G →₀ ↑(A.toCoinvariants S)))
hzw :
  (ModuleCat.Hom.hom (d₂₁ (A.toCoinvariants S))) w =
    ↑((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) -
      ↑((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
Z : ↥S →₀ ↑A
hZ : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Z = ↑z
W : G × G →₀ ↑A
hW : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ W = w
b : G →₀ ↑A := ↑x + (ConcreteCategory.hom (d₂₁ A)) W - (lmapDomain (↑A) k ⇑S.subtype) Z
g : G
⊢ (Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ((↑x + (ConcreteCategory.hom (d₂₁ A)) W) g) =
    (Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) (((lmapDomain (↑A) k ⇑S.subtype) Z) g)

Tactic:
have := Finsupp.ext_iff.1 (congr($((mapShortComplexH1 (B := toCoinvariants A S)
        (MonoidHom.id G) (toCoinvariantsMkQ A S)).comm₁₂.symm) W)) g

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
z : ↥(cycles₁ (res S.subtype (A.toCoinvariants S)))
hz :
  (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
w : ↑(ModuleCat.of k (G × G →₀ ↑(A.toCoinvariants S)))
hzw :
  (ModuleCat.Hom.hom (d₂₁ (A.toCoinvariants S))) w =
    ↑((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) -
      ↑((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
Z : ↥S →₀ ↑A
hZ : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Z = ↑z
W : G × G →₀ ↑A
hW : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ W = w
b : G →₀ ↑A := ↑x + (ConcreteCategory.hom (d₂₁ A)) W - (lmapDomain (↑A) k ⇑S.subtype) Z
g : G
this :
  ((ConcreteCategory.hom ((shortComplexH1 A).f ≫ (mapShortComplexH1 (MonoidHom.id G) (A.toCoinvariantsMkQ S)).τ₂)) W)
      g =
    ((ConcreteCategory.hom
          ((mapShortComplexH1 (MonoidHom.id G) (A.toCoinvariantsMkQ S)).τ₁ ≫ (shortComplexH1 (A.toCoinvariants S)).f))
        W)
      g
⊢ (Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ((↑x + (ConcreteCategory.hom (d₂₁ A)) W) g) =
    (Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) (((lmapDomain (↑A) k ⇑S.subtype) Z) g)