-- 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
g_1 : G ⧸ S
g : G
s : ↥S
_ :
  (((MonoidHom.comp A.ρ S.subtype : (a : ↥S) → (↑A : Type u) →ₗ[k] (↑A : Type u)) s :
          (↑A : Type u) →ₗ[k] (↑A : Type u)) :
        (a : (↑A : Type u)) → (↑A : Type u))
      (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) =
    HSub.hSub (β := (↑A : Type u))
        (HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
          ((x : (a : G) → (↑A : Type u)) ((↑s : G) * g) : (↑A : Type u))
          ((x : (a : G) → (↑A : Type u)) (↑s : G) : (↑A : Type u)))
        ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) (↑s : G) : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑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))
                y :
              (↑A : Type u)) :
          (↑A : Type u)) +
      HAdd.hAdd (α := (↑A : Type u)) ((x : (a : G) → (↑A : Type u)) (↑s : G) : (↑A : Type u)) y
_₁ :
  HSub.hSub (β := (↑A : Type u))
        (HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
          ((x : (a : G) → (↑A : Type u)) ((↑s : G) * g) : (↑A : Type u))
          ((x : (a : G) → (↑A : Type u)) (↑s : G) : (↑A : Type u)))
        ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) (↑s : G) : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑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))
                y :
              (↑A : Type u)) :
          (↑A : Type u)) +
      HAdd.hAdd (α := (↑A : Type u)) ((x : (a : G) → (↑A : Type u)) (↑s : G) : (↑A : Type u)) y =
    HSub.hSub (β := (↑A : Type u))
        (HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
          ((x : (a : G) → (↑A : Type u)) (g * (g⁻¹ * (↑s : G) * g)) : (↑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))
              (HSub.hSub (α := (↑A : Type u))
                ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) (g⁻¹ * (↑s : G) * g) :
                        (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                      (a : (↑A : Type u)) → (↑A : Type u))
                    y :
                  (↑A : Type u))
                y) :
            (↑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))
            y :
          (↑A : Type u)) +
      y
_₂ :
  HSub.hSub (β := (↑A : Type u))
        (HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u))
          ((x : (a : G) → (↑A : Type u)) (g * (g⁻¹ * (↑s : G) * g)) : (↑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))
              (HSub.hSub (α := (↑A : Type u))
                ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) (g⁻¹ * (↑s : G) * g) :
                        (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                      (a : (↑A : Type u)) → (↑A : Type u))
                    y :
                  (↑A : Type u))
                y) :
            (↑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))
            y :
          (↑A : Type u)) +
      y =
    HSub.hSub (α := (↑A : Type u)) (β := (↑A : Type u)) ((x : (a : G) → (↑A : Type u)) g : (↑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))
            y :
          (↑A : Type u)) +
      y
⊢ (((MonoidHom.comp A.ρ S.subtype : (a : ↥S) → (↑A : Type u) →ₗ[k] (↑A : Type u)) s :
          (↑A : Type u) →ₗ[k] (↑A : Type u)) :
        (a : (↑A : Type u)) → (↑A : Type u))
      (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) =
    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

Tactic:
calc
      _ = x (s * g) - x s - A.ρ s (A.ρ g y) + (x s + y) := by
        simp [add_eq_of_eq_sub (h2 s s.2), sub_eq_of_eq_add (h1 s g)]
      _ = x (g * (g⁻¹ * s * g)) - A.ρ g (A.ρ (g⁻¹ * s * g) y - y) - A.ρ g y + y := by
        simp only [mul_assoc, mul_inv_cancel_left, map_mul, Module.End.mul_apply, map_sub,
          Representation.self_inv_apply]
        abel
      _ = x g - A.ρ g y + y := by
        simp [eq_sub_of_add_eq' (h1 g (g⁻¹ * s * g)).symm,
          h2 (g⁻¹ * s * g) (Subgroup.Normal.conj_mem' ‹_› _ s.2 _)]

Premises used: HMul.hMul, HSub.hSub, Inv.inv, HAdd.hAdd, Rep.ρ, Subtype.val, DFunLike.coe