-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
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 γ₁ γ₂ α
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)) (β := (↑(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))
        ((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 * α j) :
        (↑(G.obj (Opposite.op T)) : Type w))
rw₁ :
  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 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))
        ((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))
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))
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))) =
    γ₃.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))
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)) =
    γ₃.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))
rw₅ :
  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)) =
    γ₃.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))
rw₆ rw₇ :
  γ₃.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)) =
    γ₃.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 * α 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 * α j) :
        (↑(G.obj (Opposite.op T)) : Type w))

Tactic:
rw [map_mul, map_mul, mul_assoc, h₁₂ i j a b, ← mul_assoc,
    h₂₃ i j a b, mul_assoc]

Premises used: mul_assoc, map_mul