-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cocycles₁ A)
rw :
  Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := ModuleCat.of k ((Fin 1 → G) → (↑A : Type u))) (inhomogeneousCochains.d A 1) ∘ₗ
            ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (cochainsIso₁ A).inv :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (1 + 1) → G) → (↑A : Type u))) : Type u))
        (⇑x : (a : G) → (↑A : Type u)) :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
rw₁ :
  Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₁ A).inv ≫ inhomogeneousCochains.d A 1) :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (1 + 1) → G) → (↑A : Type u))) : Type u))
        (⇑x : (a : G) → (↑A : Type u)) :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
rw₂ :
  Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    ((ModuleCat.Hom.hom ((cochainsIso₁ A).inv ≫ (inhomogeneousCochains A).d 1 (HAdd.hAdd (α := ℕ) 1 1)) :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (1 + 1) → G) → (↑A : Type u))) : Type u))
        (⇑x : (a : G) → (↑A : Type u)) :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
rw₃ :
  Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    ((ModuleCat.Hom.hom (d₁₂ A ≫ (cochainsIso₂ A).inv) :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (1 + 1) → G) → (↑A : Type u))) : Type u))
        (⇑x : (a : G) → (↑A : Type u)) :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
rw₄ :
  Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    ((ModuleCat.Hom.hom (cochainsIso₂ A).inv ∘ₗ ModuleCat.Hom.hom (d₁₂ A) :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (1 + 1) → G) → (↑A : Type u))) : Type u))
        (⇑x : (a : G) → (↑A : Type u)) :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
rw₅ :
  Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    ((ModuleCat.Hom.hom (cochainsIso₂ A).inv :
          (a : (↑(ModuleCat.of k (G × G → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (1 + 1) → G) → (↑A : Type u))) : Type u))
        ((ModuleCat.Hom.hom (d₁₂ A) :
              (a : (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u)) →
                (↑(ModuleCat.of k (G × G → (↑A : Type u))) : Type u))
            (⇑x : (a : G) → (↑A : Type u)) :
          (↑(ModuleCat.of k (G × G → (↑A : Type u))) : Type u)) :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
rw₆ :
  Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    ((ModuleCat.Hom.hom (cochainsIso₂ A).inv :
          (a : (↑(ModuleCat.of k (G × G → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (1 + 1) → G) → (↑A : Type u))) : Type u))
        0 :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
⊢ Eq (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X := ModuleCat.of k ((Fin 1 → G) → (↑A : Type u))) (inhomogeneousCochains.d A 1) :
          (a : (↑(ModuleCat.of k ((Fin 1 → G) → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (1 + 1) → G) → (↑A : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₁ A).inv :
              (a : (↑(ModuleCat.of k (G → (↑A : Type u))) : Type u)) → (↑((inhomogeneousCochains A).X 1) : Type u))
            (⇑x : (a : G) → (↑A : Type u)) :
          (↑((inhomogeneousCochains A).X 1) : Type u)) :
      (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u))
have rw₇ : Eq.{u + 1} (α := (↑(ModuleCat.of k ((Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑A : Type u))) : Type u)) 0 0
Tactic: rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, ← inhomogeneousCochains.d_def,
        eq_d₁₂_comp_inv, ModuleCat.hom_comp, LinearMap.comp_apply, cocycles₁.d₁₂_apply x,
        map_zero]