C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j k : D.J
⊢ t' D j k i ≫ t' D k i j = inv (t' D i j k)

C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j k : D.J
⊢ inv (t' D i j k) =
    (pullbackSymmetry (f D j k) (f D j i)).hom ≫ t' D j i k ≫ (pullbackSymmetry (f D i k) (f D i j)).hom
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j k : D.J
⊢ t' D j k i ≫ t' D k i j =
    (pullbackSymmetry (f D j k) (f D j i)).hom ≫ t' D j i k ≫ (pullbackSymmetry (f D i k) (f D i j)).hom
trans inv (D.t' i j k)
no goals
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j k : D.J
⊢ t' D j k i ≫ t' D k i j = inv (t' D i j k)
exact IsIso.eq_inv_of_hom_inv_id (D.cocycle _ _ _)
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j k : D.J
⊢ inv (t' D i j k) ≫ pullback.fst =
    ((pullbackSymmetry (f D j k) (f D j i)).hom ≫ t' D j i k ≫ (pullbackSymmetry (f D i k) (f D i j)).hom) ≫
      pullback.fst
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j k : D.J
⊢ inv (t' D i j k) =
    (pullbackSymmetry (f D j k) (f D j i)).hom ≫ t' D j i k ≫ (pullbackSymmetry (f D i k) (f D i j)).hom
rw [← cancel_mono (pullback.fst : pullback (D.f i j) (D.f i k) ⟶ _)]
no goals
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j k : D.J
⊢ inv (t' D i j k) ≫ pullback.fst =
    ((pullbackSymmetry (f D j k) (f D j i)).hom ≫ t' D j i k ≫ (pullbackSymmetry (f D i k) (f D i j)).hom) ≫
      pullback.fst
simp [t_fac, t_fac_assoc]