-- 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 ⧸ S
g : G
h₁ :
  ∀ (h : G),
    Quotient.liftOn' (HMul.hMul (α := G ⧸ S) (↑g : G ⧸ S) (↑h : G ⧸ S))
        (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)
            ⋯)
        ⋯ =
      HAdd.hAdd (α := (↑(A.quotientToInvariants S) : Type u))
        ((((ρ (A.quotientToInvariants S) :
                  (a : G ⧸ S) → (↑(A.quotientToInvariants S) : Type u) →ₗ[k] (↑(A.quotientToInvariants S) : Type u))
                (↑g : G ⧸ S) :
              (↑(A.quotientToInvariants S) : Type u) →ₗ[k] (↑(A.quotientToInvariants S) : Type u)) :
            (a : (↑(A.quotientToInvariants S) : Type u)) → (↑(A.quotientToInvariants S) : Type u))
          (Quotient.liftOn' (s₁ := QuotientGroup.leftRel S) (↑h : G ⧸ S)
            (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)
                ⋯)
            ⋯))
        (Quotient.liftOn' (s₁ := QuotientGroup.leftRel S) (↑g : G ⧸ S)
          (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)
              ⋯)
          ⋯)
⊢ Quotient.liftOn' ((↑g : G ⧸ S) * h)
      (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)
          ⋯)
      ⋯ =
    HAdd.hAdd (α := (↑(A.quotientToInvariants S) : Type u))
      ((((ρ (A.quotientToInvariants S) :
                (a : G ⧸ S) → (↑(A.quotientToInvariants S) : Type u) →ₗ[k] (↑(A.quotientToInvariants S) : Type u))
              (↑g : G ⧸ S) :
            (↑(A.quotientToInvariants S) : Type u) →ₗ[k] (↑(A.quotientToInvariants S) : Type u)) :
          (a : (↑(A.quotientToInvariants S) : Type u)) → (↑(A.quotientToInvariants S) : Type u))
        (Quotient.liftOn' h
          (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)
              ⋯)
          ⋯))
      (Quotient.liftOn' (s₁ := QuotientGroup.leftRel S) (↑g : G ⧸ S)
        (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)
            ⋯)
        ⋯)

Tactic:
induction h using QuotientGroup.induction_on with | @H h =>
    apply Subtype.ext
    simp [← QuotientGroup.mk_mul, h1 g h, sub_add_eq_add_sub, add_assoc]

Premises used: add_assoc, QuotientGroup.mk_mul, sub_add_eq_add_sub, Subtype.ext