C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j k : D.J
⊢ (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) ≫
      pullback.fst =
    𝟙 (pullback (f D i j) (f D i k)) ≫ pullback.fst
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j k : D.J
⊢ 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 =
    𝟙 (pullback (f D i j) (f D i k))
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
⊢ (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) ≫
      pullback.fst =
    𝟙 (pullback (f D i j) (f D i k)) ≫ pullback.fst
simp [t_fac, t_fac_assoc]