C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq₁ : t' D i i j ≫ pullback.snd = pullback.fst ≫ t D i i
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
have eq₁ := D.t_fac i i j
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq₁ : t' D i i j ≫ pullback.snd = pullback.fst ≫ t D i i
eq₂ : pullback.fst = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq₁ : t' D i i j ≫ pullback.snd = pullback.fst ≫ t D i i
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
have eq₂ := (IsIso.eq_comp_inv (D.f i i)).mpr (@pullback.condition _ _ _ _ _ _ (D.f i j) _)
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq₁ : t' D i i j ≫ pullback.snd = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
eq₂ : pullback.fst = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq₁ : t' D i i j ≫ pullback.snd = pullback.fst ≫ t D i i
eq₂ : pullback.fst = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
rw [D.t_id, Category.comp_id, eq₂] at eq₁
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq₁ : t' D i i j ≫ pullback.snd = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
eq₂ : pullback.fst = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
eq₃ : (t' D i i j ≫ pullback.snd) ≫ f D i i = pullback.snd ≫ f D i j
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq₁ : t' D i i j ≫ pullback.snd = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
eq₂ : pullback.fst = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
have eq₃ := (IsIso.eq_comp_inv (D.f i i)).mp eq₁
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq₁ : t' D i i j ≫ pullback.snd = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
eq₂ : pullback.fst = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
eq₃ : (t' D i i j ≫ pullback.fst) ≫ f D i j = pullback.snd ≫ f D i j
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq₁ : t' D i i j ≫ pullback.snd = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
eq₂ : pullback.fst = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
eq₃ : (t' D i i j ≫ pullback.snd) ≫ f D i i = pullback.snd ≫ f D i j
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
rw [Category.assoc, ← pullback.condition, ← Category.assoc] at eq₃
no goals
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq₁ : t' D i i j ≫ pullback.snd = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
eq₂ : pullback.fst = (pullback.snd ≫ f D i j) ≫ inv (f D i i)
eq₃ : (t' D i i j ≫ pullback.fst) ≫ f D i j = pullback.snd ≫ f D i j
⊢ t' D i i j = (pullbackSymmetry (f D i i) (f D i j)).hom
exact
  Mono.right_cancellation _ _
    ((Mono.right_cancellation _ _ eq₃).trans (pullbackSymmetry_hom_comp_fst _ _).symm)