-- 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
x : (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u)
h : Membership.mem (γ := Submodule k (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u)) ⊤ x
X : G →₀ ↥S →₀ (↑A : Type u)
hX :
  mapRange
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (chains₁ToCoinvariantsKer (res S.subtype A))) :
        (a : (↑(ModuleCat.of k (↥S →₀ (↑(res S.subtype A) : Type u))) : Type u)) →
          (↑(ModuleCat.of k ↥(Coinvariants.ker (res S.subtype A).ρ)) : Type u))
      ⋯ X =
    x
Y : ↥S →₀ (↑A : Type u) :=
  X.sum fun (g : G) (f : ↥S →₀ (↑A : Type u)) ↦
    HSub.hSub (α := ↥S →₀ (↑A : Type u))
      ((mapRange.linearMap ((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹) :
            (a : ↥S →₀ (↑A : Type u)) → ↥S →₀ (↑A : Type u))
          ((lmapDomain (↑A : Type u) k fun (s : ↥S) ↦
                (((MulAut.conjNormal : (a : G) → MulAut ↥S) g⁻¹ : MulAut ↥S) : (a : ↥S) → ↥S) s :
              (a : ↥S →₀ (↑A : Type u)) → ↥S →₀ (↑A : Type u))
            f) :
        ↥S →₀ (↑A : Type u))
      f
Z : G × G →₀ (↑A : Type u) :=
  X.sum fun (g : G) (f : ↥S →₀ (↑A : Type u)) ↦
    HSub.hSub (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
      ((lmapDomain (↑A : Type u) k fun (s : ↥S) ↦ (g, g⁻¹ * (↑s : G) * g) :
            (a : ↥S →₀ (↑A : Type u)) → G × G →₀ (↑A : Type u))
          f :
        G × G →₀ (↑A : Type u))
      ((lmapDomain (↑A : Type u) k fun (s : ↥S) ↦ ((↑s : G), g) : (a : ↥S →₀ (↑A : Type u)) → G × G →₀ (↑A : Type u))
          f :
        G × G →₀ (↑A : Type u))
change :
  (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))
      Z =
    HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
      (mapRange id ⋯
        ((lmapDomain (↑A : Type u) k (Subtype.val (p := fun (x : G) ↦ x ∈ S)) :
            (a : ↥S →₀ (↑A : Type u)) → G →₀ (↑A : Type u))
          Y))
      ((mapRange.linearMap (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype :
            (a : G →₀ ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))) → G →₀ (↑A : Type u))
          (mapDomain id x) :
        G →₀ (↑A : Type u))
⊢ (ModuleCat.Hom.hom (shortComplexH1 A).f : (a : (↑(shortComplexH1 A).X₁ : Type u)) → (↑(shortComplexH1 A).X₂ : Type u))
      Z =
    HSub.hSub (α := (↑(shortComplexH1 A).X₂ : Type u)) (β := (↑(shortComplexH1 A).X₂ : Type u))
      (((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂.hom' :
            (a : (↑(shortComplexH1 (res S.subtype A)).X₂ : Type u)) → (↑(shortComplexH1 A).X₂ : Type u))
          Y :
        (↑(shortComplexH1 A).X₂ : Type u))
      ((ModuleCat.Hom.hom' (Hom.τ₂ (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f)) :
            (a : (↑(shortComplexH1 (A.coinvariantsShortComplex S).X₁).X₂ : Type u)) → (↑(shortComplexH1 A).X₂ : Type u))
          x :
        (↑(shortComplexH1 A).X₂ : Type u))

Tactic:
change d₂₁ A Z = mapRange id rfl (lmapDomain _ k Subtype.val Y) -
    mapRange.linearMap (Submodule.subtype _) (mapDomain id x)

Premises used: CategoryTheory.ConcreteCategory.hom, Finsupp.mapDomain, Finsupp.lmapDomain, id, groupHomology.d₂₁, Submodule.subtype, Finsupp.mapRange.linearMap, Finsupp.mapRange, Subtype.val, DFunLike.coe, rfl