C : Type u
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst✝² : HasPullback f g
inst✝¹ : HasPullback f' pullback.fst
inst✝ : HasPullback (f' ≫ f) g
⊢ (pullbackRightPullbackFstIso f g f').inv ≫ pullback.fst ≫ f' = pullback.fst ≫ f'
C : Type u
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst✝² : HasPullback f g
inst✝¹ : HasPullback f' pullback.fst
inst✝ : HasPullback (f' ≫ f) g
⊢ (pullbackRightPullbackFstIso f g f').inv ≫ pullback.snd ≫ pullback.fst = pullback.fst ≫ f'
rw [← pullback.condition]
no goals
C : Type u
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst✝² : HasPullback f g
inst✝¹ : HasPullback f' pullback.fst
inst✝ : HasPullback (f' ≫ f) g
⊢ (pullbackRightPullbackFstIso f g f').inv ≫ pullback.fst ≫ f' = pullback.fst ≫ f'
exact pullbackRightPullbackFstIso_inv_fst_assoc _ _ _ _