-- 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 : (↑(H1InfRes A S).X₂ : Type u)
hx : x ∈ (ModuleCat.Hom.hom (H1InfRes A S).g).ker
h :
  ∀ (x : ↥(cocycles₁ A))
    (hx :
      Membership.mem (α := (↑(H1InfRes A S).X₂ : Type u)) (ModuleCat.Hom.hom (H1InfRes A S).g).ker
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (H1π A) :
              (a : (↑(ModuleCat.of k ↥(cocycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
            x :
          (↑(H1 A) : Type u))),
    Membership.mem (α := (↑(H1InfRes A S).X₂ : Type u)) (ModuleCat.Hom.hom (H1InfRes 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 : (↑(ModuleCat.of k ↥(cocycles₁ A)) : Type u)) → (↑(H1 A) : Type u))
          x :
        (↑(H1 A) : Type u))
⊢ x ∈ (ModuleCat.Hom.hom (H1InfRes A S).f).range

Tactic:
induction x using H1_induction_on with | @h x =>
  simp_all only [H1InfRes_X₂, H1InfRes_X₃, H1InfRes_g, H1InfRes_X₁, LinearMap.mem_ker,
    H1π_comp_map_apply S.subtype, H1InfRes_f]
  rcases (H1π_eq_zero_iff _).1 hx with ⟨(y : A), hy⟩
  have h1 := (mem_cocycles₁_iff x).1 x.2
  have h2 : ∀ s ∈ S, x s = A.ρ s y - y :=
    fun s hs => funext_iff.1 hy.symm ⟨s, hs⟩
  refine ⟨H1π _ ⟨fun g => Quotient.liftOn' g (fun g => ⟨x.1 g - A.ρ g y + y, ?_⟩) ?_, ?_⟩, ?_⟩
  · intro s
    calc
      _ = x (s * g) - x s - A.ρ s (A.ρ g y) + (x s + y) := by
        simp [add_eq_of_eq_sub (h2 s s.2), sub_eq_of_eq_add (h1 s g)]
      _ = x (g * (g⁻¹ * s * g)) - A.ρ g (A.ρ (g⁻¹ * s * g) y - y) - A.ρ g y + y := by
        simp only [mul_assoc, mul_inv_cancel_left, map_mul, Module.End.mul_apply, map_sub,
          Representation.self_inv_apply]
        abel
      _ = x g - A.ρ g y + y := by
        simp [eq_sub_of_add_eq' (h1 g (g⁻¹ * s * g)).symm,
          h2 (g⁻¹ * s * g) (Subgroup.Normal.conj_mem' ‹_› _ s.2 _)]
  · intro g h hgh
    have := congr(A.ρ g $(h2 (g⁻¹ * h) <| QuotientGroup.leftRel_apply.1 hgh))
    simp_all [← sub_eq_add_neg, sub_eq_sub_iff_sub_eq_sub]
  · rw [mem_cocycles₁_iff]
    intro g h
    induction g using QuotientGroup.induction_on with | @H g =>
    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]
  · symm
    simp only [H1π_comp_map_apply, H1π_eq_iff (A := A)]
    use y
    ext g
    simp [coe_mapCocycles₁ (QuotientGroup.mk' S),
      cocycles₁.coe_mk (A := A.quotientToInvariants S), ← sub_sub]

Premises used: groupCohomology.coe_mapCocycles₁, sub_eq_sub_iff_sub_eq_sub, add_assoc, Subgroup.subtype, sub_eq_add_neg, groupCohomology.H1InfRes_X₂, groupCohomology.H1InfRes_X₃, groupCohomology.mem_cocycles₁_iff, LinearMap.mem_ker, sub_sub, groupCohomology.H1InfRes_X₁, QuotientGroup.mk', groupCohomology.H1π_comp_map_apply, groupCohomology.H1InfRes_g, QuotientGroup.mk_mul, sub_add_eq_add_sub, groupCohomology.cocycles₁.coe_mk, groupCohomology.H1InfRes_f, CategoryTheory.ShortComplex.g, groupCohomology.H1π_eq_iff, Subtype.ext