-- 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
inst_3 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ (↑A : Type u)
hxc : x ∈ cycles₁ A
hx :
  Eq (α := (↑(H1 (A.ofQuotient S)) : Type u))
    (((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ↥(cycles₁ (A.ofQuotient S))) (Y :=
              groupHomology (A.ofQuotient S) 1) (H1π (A.ofQuotient S)) :
            (↑(ModuleCat.of k ↥(cycles₁ (A.ofQuotient S))) : Type u) →ₗ[k]
              (↑(groupHomology (A.ofQuotient S) 1) : Type u)) :
          (a : ↥(cycles₁ (A.ofQuotient S))) → (↑(groupHomology (A.ofQuotient S) 1) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ (A.ofQuotient S)))
                (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S))) :
              (a : ↥(cycles₁ A)) → ↥(cycles₁ (A.ofQuotient S)))
            (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ cycles₁ A) x hxc) :
          ↥(cycles₁ (A.ofQuotient S))) :
      (↑(groupHomology (A.ofQuotient S) 1) : Type u))
    (0 : (↑(H1 (A.ofQuotient S)) : Type u))
h :
  ∀ (y : (↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) : Type u))
    (hy :
      Eq (α := G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))
        ((ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S)) :
              (a : (↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))) : Type u)) →
                G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))
            y :
          G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))
        ((↑((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ (A.ofQuotient S)))
                    (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv (A.resOfQuotientIso S))) :
                  (a : ↥(cycles₁ A)) → ↥(cycles₁ (A.ofQuotient S)))
                (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ cycles₁ A) x hxc)) :
            G ⧸ S →₀ (↑(A.ofQuotient S) : Type u)) :
          G ⧸ S →₀ (↑(A.ofQuotient S) : Type u))),
    Membership.mem (α := (↑(H1 A) : Type u)) (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H1π A) :
            (a : ↥(cycles₁ A)) → (↑(H1 A) : Type u))
          (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ cycles₁ A) x hxc) :
        (↑(H1 A) : Type u))
⊢ Membership.mem (α := (↑(H1 A) : Type u)) (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1π A) :
          (a : ↥(cycles₁ A)) → (↑(H1 A) : Type u))
        (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ cycles₁ A) x hxc) :
      (↑(H1 A) : Type u))

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

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