-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ : OneCochain G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁ γ₂ α
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
rw :
  HMul.hMul (β := (↑(G.obj (Opposite.op T)) : Type w))
      (HMul.hMul (α := (↑(G.obj (Opposite.op T)) : Type w))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                GrpCat.carrier) (G.map a.op) :
              (a : (↑(G.obj (Opposite.op (U i))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
            (α⁻¹ i) :
          (↑(G.obj (Opposite.op T)) : Type w))
        (γ₂.ev i j a b))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map b.op) :
            (a : (↑(G.obj (Opposite.op (U j))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          (α j) :
        (↑(G.obj (Opposite.op T)) : Type w)) =
    HMul.hMul (β := (↑(G.obj (Opposite.op T)) : Type w))
      (HMul.hMul (β := (↑(G.obj (Opposite.op T)) : Type w)) (γ₁.ev i j a b)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                GrpCat.carrier) (G.map b.op) :
              (a : (↑(G.obj (Opposite.op (U j))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
            (α⁻¹ j) :
          (↑(G.obj (Opposite.op T)) : Type w)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map b.op) :
            (a : (↑(G.obj (Opposite.op (U j))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          (α j) :
        (↑(G.obj (Opposite.op T)) : Type w))
rw₁ :
  HMul.hMul (α := (↑(G.obj (Opposite.op T)) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map a.op) :
            (a : (↑(G.obj (Opposite.op (U i))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          (α⁻¹ i) :
        (↑(G.obj (Opposite.op T)) : Type w))
      (HMul.hMul (β := (↑(G.obj (Opposite.op T)) : Type w)) (γ₂.ev i j a b)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                GrpCat.carrier) (G.map b.op) :
              (a : (↑(G.obj (Opposite.op (U j))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
            (α j) :
          (↑(G.obj (Opposite.op T)) : Type w))) =
    HMul.hMul (β := (↑(G.obj (Opposite.op T)) : Type w))
      (HMul.hMul (β := (↑(G.obj (Opposite.op T)) : Type w)) (γ₁.ev i j a b)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                GrpCat.carrier) (G.map b.op) :
              (a : (↑(G.obj (Opposite.op (U j))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
            (α⁻¹ j) :
          (↑(G.obj (Opposite.op T)) : Type w)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map b.op) :
            (a : (↑(G.obj (Opposite.op (U j))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          (α j) :
        (↑(G.obj (Opposite.op T)) : Type w))
rw₂ :
  HMul.hMul (α := (↑(G.obj (Opposite.op T)) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map a.op) :
            (a : (↑(G.obj (Opposite.op (U i))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          (α⁻¹ i) :
        (↑(G.obj (Opposite.op T)) : Type w))
      (HMul.hMul (α := (↑(G.obj (Opposite.op T)) : Type w))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                GrpCat.carrier) (G.map a.op) :
              (a : (↑(G.obj (Opposite.op (U i))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
            (α i) :
          (↑(G.obj (Opposite.op T)) : Type w))
        (γ₁.ev i j a b)) =
    HMul.hMul (β := (↑(G.obj (Opposite.op T)) : Type w))
      (HMul.hMul (β := (↑(G.obj (Opposite.op T)) : Type w)) (γ₁.ev i j a b)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                GrpCat.carrier) (G.map b.op) :
              (a : (↑(G.obj (Opposite.op (U j))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
            (α⁻¹ j) :
          (↑(G.obj (Opposite.op T)) : Type w)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map b.op) :
            (a : (↑(G.obj (Opposite.op (U j))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          (α j) :
        (↑(G.obj (Opposite.op T)) : Type w))
rw₃ :
  HMul.hMul (α := (↑(G.obj (Opposite.op T)) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map a.op) :
            (a : (↑(G.obj (Opposite.op (U i))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          (α⁻¹ i) :
        (↑(G.obj (Opposite.op T)) : Type w))
      (HMul.hMul (α := (↑(G.obj (Opposite.op T)) : Type w))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                GrpCat.carrier) (G.map a.op) :
              (a : (↑(G.obj (Opposite.op (U i))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
            (α i) :
          (↑(G.obj (Opposite.op T)) : Type w))
        (γ₁.ev i j a b)) =
    γ₁.ev i j a b *
      HMul.hMul (α := (↑(G.obj (Opposite.op T)) : Type w)) (β := (↑(G.obj (Opposite.op T)) : Type w))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                GrpCat.carrier) (G.map b.op) :
              (a : (↑(G.obj (Opposite.op (U j))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
            (α⁻¹ j) :
          (↑(G.obj (Opposite.op T)) : Type w))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                GrpCat.carrier) (G.map b.op) :
              (a : (↑(G.obj (Opposite.op (U j))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
            (α j) :
          (↑(G.obj (Opposite.op T)) : Type w))
⊢ HMul.hMul (α := (↑(G.obj (Opposite.op T)) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map a.op) :
            (a : (↑(G.obj (Opposite.op (U i))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          (α⁻¹ i) :
        (↑(G.obj (Opposite.op T)) : Type w))
      (γ₂.ev i j a b) =
    HMul.hMul (β := (↑(G.obj (Opposite.op T)) : Type w)) (γ₁.ev i j a b)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map b.op) :
            (a : (↑(G.obj (Opposite.op (U j))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          (α⁻¹ j) :
        (↑(G.obj (Opposite.op T)) : Type w))
have rw₄ : HMul.hMul (α := (↑(G.obj (Opposite.op T)) : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
            (G.map a.op) :
          (a : (↑(G.obj (Opposite.op (U i))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
        (α i)⁻¹ :
      (↑(G.obj (Opposite.op T)) : Type w))
    (HMul.hMul (α := (↑(G.obj (Opposite.op T)) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map a.op) :
            (a : (↑(G.obj (Opposite.op (U i))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          (α i) :
        (↑(G.obj (Opposite.op T)) : Type w))
      (γ₁.ev i j a b)) =
  γ₁.ev i j a b *
    HMul.hMul (α := (↑(G.obj (Opposite.op T)) : Type w)) (β := (↑(G.obj (Opposite.op T)) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map b.op) :
            (a : (↑(G.obj (Opposite.op (U j))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          (α⁻¹ j) :
        (↑(G.obj (Opposite.op T)) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map b.op) :
            (a : (↑(G.obj (Opposite.op (U j))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          (α j) :
        (↑(G.obj (Opposite.op T)) : Type w))
Tactic: rw [← mul_left_inj (G.map b.op (α j)), mul_assoc, ← h i j a b,
    mul_assoc, Cochain₀.inv_apply, map_inv, inv_mul_cancel_left,
    Cochain₀.inv_apply, map_inv, inv_mul_cancel, mul_one]