case a
C : Type u₁
inst✝³ : Category C
J : Type u₂
inst✝² : Category J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pushout.inl ≫ (pullbackIsoUnopPushout f g).hom.op).unop = pullback.fst.op.unop
C : Type u₁
inst✝³ : Category C
J : Type u₂
inst✝² : Category J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ pushout.inl ≫ (pullbackIsoUnopPushout f g).hom.op = pullback.fst.op
apply Quiver.Hom.unop_inj
case a
C : Type u₁
inst✝³ : Category C
J : Type u₂
inst✝² : Category J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pullbackIsoUnopPushout f g).hom ≫ pushout.inl.unop = pullback.fst
case a
C : Type u₁
inst✝³ : Category C
J : Type u₂
inst✝² : Category J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pushout.inl ≫ (pullbackIsoUnopPushout f g).hom.op).unop = pullback.fst.op.unop
dsimp
no goals
case a
C : Type u₁
inst✝³ : Category C
J : Type u₂
inst✝² : Category J
X✝ : Type v₂
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pullbackIsoUnopPushout f g).hom ≫ pushout.inl.unop = pullback.fst
rw [← pullbackIsoUnopPushout_inv_fst, Iso.hom_inv_id_assoc]