C : Type u
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
w :
  (span f g).map fst ≫ t.ι.app WalkingSpan.left =
    t.ι.app WalkingSpan.zero ≫ ((Functor.const WalkingSpan).obj t.pt).map fst
⊢ t.ι.app WalkingSpan.zero = f ≫ inl t
C : Type u
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
⊢ t.ι.app WalkingSpan.zero = f ≫ inl t
have w := t.ι.naturality WalkingSpan.Hom.fst
C : Type u
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
w : f ≫ inl t = t.ι.app WalkingSpan.zero ≫ 𝟙 t.pt
⊢ t.ι.app WalkingSpan.zero = f ≫ inl t
C : Type u
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
w :
  (span f g).map fst ≫ t.ι.app WalkingSpan.left =
    t.ι.app WalkingSpan.zero ≫ ((Functor.const WalkingSpan).obj t.pt).map fst
⊢ t.ι.app WalkingSpan.zero = f ≫ inl t
dsimp at w
no goals
C : Type u
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
w : f ≫ inl t = t.ι.app WalkingSpan.zero ≫ 𝟙 t.pt
⊢ t.ι.app WalkingSpan.zero = f ≫ inl t
simpa using w.symm