C : Type u
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
w :
  ((Functor.const WalkingCospan).obj t.pt).map inl ≫ t.π.app WalkingCospan.one =
    t.π.app WalkingCospan.left ≫ (cospan f g).map inl
⊢ t.π.app WalkingCospan.one = fst t ≫ f
C : Type u
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
⊢ t.π.app WalkingCospan.one = fst t ≫ f
have w := t.π.naturality WalkingCospan.Hom.inl
C : Type u
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
w : 𝟙 t.pt ≫ t.π.app WalkingCospan.one = fst t ≫ f
⊢ t.π.app WalkingCospan.one = fst t ≫ f
C : Type u
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
w :
  ((Functor.const WalkingCospan).obj t.pt).map inl ≫ t.π.app WalkingCospan.one =
    t.π.app WalkingCospan.left ≫ (cospan f g).map inl
⊢ t.π.app WalkingCospan.one = fst t ≫ f
dsimp at w
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
t : PullbackCone f g
w : 𝟙 t.pt ≫ t.π.app WalkingCospan.one = fst t ≫ f
⊢ t.π.app WalkingCospan.one = fst t ≫ f
simpa using w