case mk.intro
C : Type u
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X Y Z✝ : C
f✝ : X ⟶ Z✝
g : Y ⟶ Z✝
f : X ⟶ Y
t : IsLimit (mk (𝟙 X) (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ f))
Z : C
val✝ : Z ⟶ (mk (𝟙 X) (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ f)).pt
eq :
  (val✝ ≫ fst (mk (𝟙 X) (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ f))) ≫ f = (val✝ ≫ snd (mk (𝟙 X) (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ f))) ≫ f
⊢ val✝ ≫ fst (mk (𝟙 X) (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ f)) = val✝ ≫ snd (mk (𝟙 X) (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ 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 : X ⟶ Y
t : IsLimit (mk (𝟙 X) (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ f))
Z : C
g h : Z ⟶ X
eq : g ≫ f = h ≫ f
⊢ g = h
rcases PullbackCone.IsLimit.lift' t _ _ eq with ⟨_, rfl, rfl⟩
no goals
case mk.intro
C : Type u
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W X Y Z✝ : C
f✝ : X ⟶ Z✝
g : Y ⟶ Z✝
f : X ⟶ Y
t : IsLimit (mk (𝟙 X) (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ f))
Z : C
val✝ : Z ⟶ (mk (𝟙 X) (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ f)).pt
eq :
  (val✝ ≫ fst (mk (𝟙 X) (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ f))) ≫ f = (val✝ ≫ snd (mk (𝟙 X) (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ f))) ≫ f
⊢ val✝ ≫ fst (mk (𝟙 X) (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ f)) = val✝ ≫ snd (mk (𝟙 X) (𝟙 X) (_ : 𝟙 X ≫ f = 𝟙 X ≫ f))
rfl