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
ht : IsLimit t
inst✝ : Mono f
W : C
h k : W ⟶ t.pt
i : h ≫ snd t = k ≫ snd t
⊢ h ≫ fst t = k ≫ fst t
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
ht : IsLimit t
inst✝ : Mono f
⊢ Mono (snd t)
refine ⟨fun {W} h k i => IsLimit.hom_ext ht ?_ i⟩
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
ht : IsLimit t
inst✝ : Mono f
W : C
h k : W ⟶ t.pt
i : h ≫ snd t = k ≫ snd t
⊢ h ≫ snd t ≫ g = k ≫ snd t ≫ g
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
ht : IsLimit t
inst✝ : Mono f
W : C
h k : W ⟶ t.pt
i : h ≫ snd t = k ≫ snd t
⊢ h ≫ fst t = k ≫ fst t
rw [← cancel_mono f, Category.assoc, Category.assoc, condition]
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
ht : IsLimit t
inst✝ : Mono f
W : C
h k : W ⟶ t.pt
i : h ≫ snd t = k ≫ snd t
this : (h ≫ snd t) ≫ g = (k ≫ snd t) ≫ g
⊢ h ≫ snd t ≫ g = k ≫ snd t ≫ g
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
ht : IsLimit t
inst✝ : Mono f
W : C
h k : W ⟶ t.pt
i : h ≫ snd t = k ≫ snd t
this : (fun x => x ≫ g) (h ≫ snd t) = (fun x => x ≫ g) (k ≫ snd t)
⊢ h ≫ snd t ≫ g = k ≫ snd t ≫ g
dsimp at this
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
ht : IsLimit t
inst✝ : Mono f
W : C
h k : W ⟶ t.pt
i : h ≫ snd t = k ≫ snd t
this : (h ≫ snd t) ≫ g = (k ≫ snd t) ≫ g
⊢ h ≫ snd t ≫ g = k ≫ snd t ≫ g
rwa [Category.assoc, Category.assoc] at this