C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
⊢ t' D i j i = (t' D i j i ≫ pullback.snd) ≫ inv pullback.snd
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
⊢ t' D i j i = pullback.fst ≫ t D i j ≫ inv pullback.snd
rw [← Category.assoc, ← D.t_fac]
no goals
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
⊢ t' D i j i = (t' D i j i ≫ pullback.snd) ≫ inv pullback.snd
simp