-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₂ X.X₃)
y : G × G →₀ (↑X.X₂ : Type u)
hy :
  (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap : (a : G × G →₀ (↑X.X₂ : Type u)) → G × G →₀ (↑X.X₃ : Type u)) y =
    (↑z : G × G →₀ (↑X.X₃ : Type u))
x : G →₀ (↑X.X₁ : Type u)
hx :
  Eq (α := G →₀ (↑X.X₂ : Type u))
    ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap : (a : G →₀ (↑X.X₁ : Type u)) → G →₀ (↑X.X₂ : Type u)) x :
      G →₀ (↑X.X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d₂₁ X.X₂) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
        y :
      (↑(ModuleCat.of k (G →₀ (↑X.X₂ : Type u))) : Type u))
x_1 : Fin 1 → G
⊢ Eq (α := (↑X.X₂ : Type u))
    ((((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap :
                (a : (Fin 1 → G) →₀ (↑X.X₁ : Type u)) → (Fin 1 → G) →₀ (↑X.X₂ : Type u))
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (chainsIso₁ X.X₁).inv :
                  (a : (↑(ModuleCat.of k (G →₀ (↑X.X₁ : Type u))) : Type u)) →
                    (↑((inhomogeneousChains X.X₁).X 1) : Type u))
                x) :
            (Fin 1 → G) →₀ (↑X.X₂ : Type u)) :
          (a : Fin 1 → G) → (↑X.X₂ : Type u))
        x_1 :
      (↑X.X₂ : Type u))
    ((((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (X := (inhomogeneousChains X.X₂).X 2) (Y := (inhomogeneousChains X.X₂).X 1)
                  ((inhomogeneousChains X.X₂).d 2 1) :
                (a : (↑((inhomogeneousChains X.X₂).X 2) : Type u)) → (↑((inhomogeneousChains X.X₂).X 1) : Type u))
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (chainsIso₂ X.X₂).inv :
                  (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
                    (↑((inhomogeneousChains X.X₂).X 2) : Type u))
                y) :
            (↑((inhomogeneousChains X.X₂).X 1) : Type u)) :
          (a : Fin 1 → G) → (↑X.X₂ : Type u))
        x_1 :
      (↑X.X₂ : Type u))
have conv_rhs : Eq (α := (↑X.X₂ : Type u))
  ((((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap :
              (a : (Fin 1 → G) →₀ (↑X.X₁ : Type u)) → (Fin 1 → G) →₀ (↑X.X₂ : Type u))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (chainsIso₁ X.X₁).inv :
                (a : (↑(ModuleCat.of k (G →₀ (↑X.X₁ : Type u))) : Type u)) →
                  (↑((inhomogeneousChains X.X₁).X 1) : Type u))
              x) :
          (Fin 1 → G) →₀ (↑X.X₂ : Type u)) :
        (a : Fin 1 → G) → (↑X.X₂ : Type u))
      x_1 :
    (↑X.X₂ : Type u))
  ((((ModuleCat.Hom.hom (d₂₁ X.X₂ ≫ (chainsIso₁ X.X₂).inv) :
              (a : (↑(ModuleCat.of k (G × G →₀ (↑X.X₂ : Type u))) : Type u)) →
                (↑((inhomogeneousChains X.X₂).X 1) : Type u))
            y :
          (↑((inhomogeneousChains X.X₂).X 1) : Type u)) :
        (a : Fin 1 → G) → (↑X.X₂ : Type u))
      x_1 :
    (↑X.X₂ : Type u))
Tactic: conv_rhs => rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₂₁_comp_inv]