C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq : (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
have eq : (pullbackSymmetry (D.f i i) (D.f i j)).hom = pullback.snd ≫ inv pullback.fst := by simp
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq : (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
this : t' D i j i ≫ t' D j i i ≫ t' D i i j = 𝟙 (pullback (f D i j) (f D i i))
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq : (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
have := D.cocycle i j i
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq : (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
this :
  (pullback.fst ≫ t D i j ≫ inv pullback.snd) ≫
      (pullback.snd ≫ t D j i ≫ inv pullback.snd) ≫ pullback.snd ≫ inv pullback.fst =
    𝟙 (pullback (f D i j) (f D i i))
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq : (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
this : t' D i j i ≫ t' D j i i ≫ t' D i i j = 𝟙 (pullback (f D i j) (f D i i))
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
rw [D.t'_iij, D.t'_jii, D.t'_iji, fst_eq_snd_of_mono_eq, eq] at this
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq : (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
this : pullback.fst ≫ t D i j ≫ t D j i ≫ inv pullback.fst = 𝟙 (pullback (f D i j) (f D i i))
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq : (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
this :
  (pullback.fst ≫ t D i j ≫ inv pullback.snd) ≫
      (pullback.snd ≫ t D j i ≫ inv pullback.snd) ≫ pullback.snd ≫ inv pullback.fst =
    𝟙 (pullback (f D i j) (f D i i))
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
simp only [Category.assoc, IsIso.inv_hom_id_assoc] at this
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq : (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
this : t D i j ≫ t D j i = (inv pullback.fst ≫ 𝟙 (pullback (f D i j) (f D i i))) ≫ pullback.fst
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq : (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
this : pullback.fst ≫ t D i j ≫ t D j i ≫ inv pullback.fst = 𝟙 (pullback (f D i j) (f D i i))
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
rw [← IsIso.eq_inv_comp, ← Category.assoc, IsIso.comp_inv_eq] at this
no goals
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
eq : (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
this : t D i j ≫ t D j i = (inv pullback.fst ≫ 𝟙 (pullback (f D i j) (f D i i))) ≫ pullback.fst
⊢ t D i j ≫ t D j i = 𝟙 (V D (i, j))
simpa using this
no goals
C : Type u₁
inst✝¹ : Category C
C' : Type u₂
inst✝ : Category C'
D : GlueData C
i j : D.J
⊢ (pullbackSymmetry (f D i i) (f D i j)).hom = pullback.snd ≫ inv pullback.fst
simp