-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
Goal:
k G H_1 : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H_1
A : Rep k G
B : Rep k H_1
f : G →* H_1
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst_3 : S.Normal
x : ↥(cycles₁ (A.quotientToCoinvariants S))
y : (↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S))) : Type u)
hy :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (Y := ModuleCat.of k ↥(cycles₁ ((A.toCoinvariants S).ofQuotient S)))
          (mapCycles₁ (QuotientGroup.mk' S) (Iso.inv ((A.toCoinvariants S).resOfQuotientIso S))) :
        (a : (↑(ModuleCat.of k ↥(cycles₁ (A.toCoinvariants S))) : Type u)) →
          (↑(ModuleCat.of k ↥(cycles₁ ((A.toCoinvariants S).ofQuotient S))) : Type u))
      y =
    x
Y : G →₀ (↑A : Type u)
hY :
  mapRange
      (⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) :
        (a : (↑A : Type u)) → Coinvariants (MonoidHom.comp A.ρ S.subtype))
      ⋯ Y =
    (↑y : G →₀ (↑(A.toCoinvariants S) : Type u))
this :
  Membership.mem (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u)) (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))
    ((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 →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        Y :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
Z : ↥S →₀ (↑A : Type u)
hZ :
  Eq (α := (↑(ModuleCat.of k ↥(Coinvariants.ker (res S.subtype A).ρ)) : Type u))
    ((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))
        Z :
      (↑(ModuleCat.of k ↥(Coinvariants.ker (res S.subtype A).ρ)) : Type u))
    (Subtype.mk (p := fun (x : (↑(res S.subtype A) : Type u)) ↦ x ∈ Coinvariants.ker (res S.subtype A).ρ)
        ((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 →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          Y)
        this :
      ↥(Coinvariants.ker (res S.subtype A).ρ))
H :
  Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((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 →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        (Y - mapDomain (⇑S.subtype : (a : ↥S) → G) Z) :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    (0 : (↑(ModuleCat.of k (↑A : Type u)) : Type u))
⊢ Eq (α := (↑(H1CoresCoinf A S).X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (H1CoresCoinf A S).g :
          (a : (↑(H1CoresCoinf A S).X₂ : Type u)) → (↑(H1CoresCoinf A S).X₃ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (H1π A) :
              (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
            (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ cycles₁ A)
              (Y - mapDomain (⇑S.subtype : (a : ↥S) → G) Z) H) :
          (↑(H1 A) : Type u)) :
      (↑(H1CoresCoinf A S).X₃ : 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.quotientToCoinvariants S)))
            (H1π (A.quotientToCoinvariants S)) :
          (a : (↑(ModuleCat.of k ↥(cycles₁ (A.quotientToCoinvariants S))) : Type u)) →
            (↑(H1 (A.quotientToCoinvariants S)) : Type u))
        x :
      (↑(H1 (A.quotientToCoinvariants S)) : Type u))
have h : Eq (α := (↑(H1 (A.quotientToCoinvariants 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.quotientToCoinvariants S))) (Y :=
            groupHomology (A.quotientToCoinvariants S) 1) (H1π (A.quotientToCoinvariants S)) :
          (↑(ModuleCat.of k ↥(cycles₁ (A.quotientToCoinvariants S))) : Type u) →ₗ[k]
            (↑(groupHomology (A.quotientToCoinvariants S) 1) : Type u)) :
        (a : ↥(cycles₁ (A.quotientToCoinvariants S))) → (↑(groupHomology (A.quotientToCoinvariants 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 ↥(cycles₁ A)) (Y :=
                ModuleCat.of k ↥(cycles₁ (A.quotientToCoinvariants S)))
                (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S) :
                  Quiver.Hom (V := ModuleCat k) (ModuleCat.of k ↥(cycles₁ A))
                    (ModuleCat.of k ↥(cycles₁ (A.quotientToCoinvariants S)))) :
              (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u) →ₗ[k]
                (↑(ModuleCat.of k ↥(cycles₁ (A.quotientToCoinvariants S))) : Type u)) :
            (a : ↥(cycles₁ A)) → ↥(cycles₁ (A.quotientToCoinvariants S)))
          (Subtype.mk (p := fun (x : G →₀ (↑A : Type u)) ↦ x ∈ cycles₁ A)
            (Y - mapDomain (Subtype.val (p := fun (x : G) ↦ x ∈ S)) Z) sorry) :
        ↥(cycles₁ (A.quotientToCoinvariants S))) :
    (↑(groupHomology (A.quotientToCoinvariants 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 ↥(cycles₁ (A.quotientToCoinvariants S))) (Y :=
          H1 (A.quotientToCoinvariants S)) (H1π (A.quotientToCoinvariants S)) :
        (a : ↥(cycles₁ (A.quotientToCoinvariants S))) → (↑(H1 (A.quotientToCoinvariants S)) : Type u))
      x :
    (↑(H1 (A.quotientToCoinvariants S)) : Type u))
Tactic: simp only [H1CoresCoinf_X₃, H1CoresCoinf_X₂, H1CoresCoinf_g,
    Subgroup.coe_subtype, H1π_comp_map_apply]