-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A_1 : Rep k H
B : Rep k G
f : G →* H
φ : Quiver.Hom.{?u.266374, max (?u.266374 + 1) u} (res f A_1) B
n : ℕ
A : Rep k G
S : Subgroup G
inst_3 : S.Normal
x : ↥(cocycles₁ (A.quotientToInvariants S))
hx :
  Eq (α := (↑(groupCohomology A 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1π (of A.ρ)) :
          (a : ↥(cocycles₁ (of A.ρ))) → (↑(groupCohomology (of A.ρ) 1) : Type u))
        (((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (X := ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) (Y :=
                  ModuleCat.of k ↥(cocycles₁ (of A.ρ)))
                  (mapCocycles₁ (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) :
                    Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S)))
                      (ModuleCat.of k ↥(cocycles₁ (of A.ρ)))) :
                (↑(ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) : Type u) →ₗ[k]
                  (↑(ModuleCat.of k ↥(cocycles₁ (of A.ρ))) : Type u)) :
              (a : ↥(cocycles₁ (A.quotientToInvariants S))) → ↥(cocycles₁ (of A.ρ)))
            x :
          ↥(cocycles₁ (of A.ρ))) :
      (↑(groupCohomology (of A.ρ) 1) : Type u))
    (0 : (↑(H1InfRes A S).X₂ : Type u))
h :
  ∀ (y : (↑(ModuleCat.of k (↑(of A.ρ) : Type u)) : Type u))
    (hy :
      Eq (α := G → (↑(of A.ρ) : Type u))
        ((ModuleCat.Hom.hom (d₀₁ (of A.ρ)) :
              (a : (↑(ModuleCat.of k (↑(of A.ρ) : Type u)) : Type u)) → G → (↑(of A.ρ) : Type u))
            y :
          G → (↑(of A.ρ) : Type u))
        ((⇑(((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                        ModuleCat.carrier) (X := ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) (Y :=
                        ModuleCat.of k ↥(cocycles₁ (of A.ρ)))
                        (mapCocycles₁ (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) :
                          Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S)))
                            (ModuleCat.of k ↥(cocycles₁ (of A.ρ)))) :
                      (↑(ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) : Type u) →ₗ[k]
                        (↑(ModuleCat.of k ↥(cocycles₁ (of A.ρ))) : Type u)) :
                    (a : ↥(cocycles₁ (A.quotientToInvariants S))) → ↥(cocycles₁ (of A.ρ)))
                  x :
                ↥(cocycles₁ (of A.ρ))) :
            (a : G) → (↑(of A.ρ) : Type u)) :
          (a : G) → (↑(of A.ρ) : Type u))),
    Eq (α := (↑(groupCohomology (A.quotientToInvariants S) 1) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) (Y :=
              H1 (A.quotientToInvariants S)) (H1π (A.quotientToInvariants S)) :
            (a : ↥(cocycles₁ (A.quotientToInvariants S))) → (↑(H1 (A.quotientToInvariants S)) : Type u))
          x :
        (↑(H1 (A.quotientToInvariants S)) : Type u))
      (0 : (↑(H1InfRes A S).X₁ : Type u))
⊢ Eq (α := (↑(groupCohomology (A.quotientToInvariants S) 1) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of k ↥(cocycles₁ (A.quotientToInvariants S))) (Y :=
            H1 (A.quotientToInvariants S)) (H1π (A.quotientToInvariants S)) :
          (a : ↥(cocycles₁ (A.quotientToInvariants S))) → (↑(H1 (A.quotientToInvariants S)) : Type u))
        x :
      (↑(H1 (A.quotientToInvariants S)) : Type u))
    (0 : (↑(H1InfRes A S).X₁ : Type u))

Tactic:
rcases (H1π_eq_zero_iff _).1 hx with ⟨y, hy⟩

Premises used: groupCohomology.H1π_eq_zero_iff, Iff.mp