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