-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst_3 : S.Normal
x : (↑(H1CoresCoinf A S).X₃ : Type u)
h :
  ∀ (x : ↥(cycles₁ (A.quotientToCoinvariants S))),
    ∃ (a : (↑(H1CoresCoinf A S).X₂ : 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))
            a :
          (↑(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))
⊢ ∃ (a : (↑(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))
        a =
      x

Tactic:
induction x using H1_induction_on with | @h x =>
/- Let `x : Z₁(G ⧸ S, A_S)`. We know `Z₁(G, A_S) ⟶ Z₁(G ⧸ S, A_S)` is surjective, so pick
`y : Z₁(G, A_S)` in the preimage of `x`. -/
  rcases (ModuleCat.epi_iff_surjective _).1
    (mapCycles₁_quotientGroupMk'_epi (A.toCoinvariants S) S) x with ⟨y, hy⟩
/- We know `C₁(G, A) ⟶ C₁(G, A_S)` is surjective, so pick `Y` in the preimage of `y`. -/
  rcases mapRange_surjective _ (map_zero _)
    (Coinvariants.mk_surjective (A.ρ.comp S.subtype)) y.1 with ⟨Y, hY⟩
/- Then `d(Y) ∈ I(S)A,` since `d(y) = 0`. -/
  have : d₁₀ _ Y ∈ Coinvariants.ker (A.ρ.comp S.subtype) := by
    have h' := congr($((mapShortComplexH1 (B := toCoinvariants A S)
      (MonoidHom.id G) (toCoinvariantsMkQ A S)).comm₂₃) Y)
    simp_all [shortComplexH1, ← Coinvariants.mk_eq_zero]
  /- Thus we can pick a representation of `d(Y)` as a sum `∑ ρ(sᵢ⁻¹)(aᵢ) - aᵢ`, `sᵢ ∈ S, aᵢ ∈ A`,
and `Y - ∑ aᵢ·sᵢ` is a cycle. -/
  rcases chains₁ToCoinvariantsKer_surjective
    (res S.subtype A) ⟨d₁₀ A Y, this⟩ with ⟨(Z : S →₀ A), hZ⟩
  have H : d₁₀ A (Y - mapDomain S.subtype Z) = 0 := by
    simpa [map_sub, sub_eq_zero, chains₁ToCoinvariantsKer, - LinearMap.sub_apply, d₁₀,
      sum_mapDomain_index_inj] using Subtype.ext_iff.1 hZ.symm
  use H1π A ⟨Y - mapDomain S.subtype Z, H⟩
  simp only [H1CoresCoinf_X₃, H1CoresCoinf_X₂, H1CoresCoinf_g,
    Subgroup.coe_subtype, H1π_comp_map_apply]
/- Moreover, the image of `Y - ∑ aᵢ·sᵢ` in `Z₁(G ⧸ S, A_S)` is `x - ∑ aᵢ·1`, and hence differs from
`x` by a boundary, since `aᵢ·1 = d(aᵢ·(1, 1))`. -/
  refine (H1π_eq_iff _ _).2 ?_
  simpa [← hy, mapCycles₁_hom, map_sub, Rep.hom_id (res _ _), ← mapDomain_comp,
    ← mapDomain_mapRange, hY, Function.comp_def, (QuotientGroup.eq_one_iff <| Subtype.val _).2
    (Subtype.prop _)] using Submodule.finsuppSum_mem _ _ _ _ fun _ _ ↦ single_one_mem_boundaries₁ _

Premises used: Iff.mpr, map_sub, groupHomology.H1CoresCoinf_X₃, Finsupp.mapDomain_mapRange, Rep.hom_id, Subgroup.coe_subtype, groupHomology.H1CoresCoinf_g, groupHomology.H1CoresCoinf_X₂, groupHomology.H1π_comp_map_apply, Rep.res, Function.comp_def, Subtype.prop, Finsupp.mapDomain_comp, groupHomology.mapCycles₁_hom, Submodule.finsuppSum_mem, groupHomology.single_one_mem_boundaries₁, Subtype.val, QuotientGroup.eq_one_iff, DFunLike.coe, groupHomology.H1π_eq_iff