no goals
C : Type u
inst✝³ : Category C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ G.map h ≫ G.map f = G.map h ≫ G.map g
simp only [← G.map_comp, w]
case h
C : Type u
inst✝³ : Category C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ (G.map (equalizer.lift h w) ≫ equalizerComparison f g G) ≫ equalizer.ι (G.map f) (G.map g) =
    equalizer.lift (G.map h) (_ : G.map h ≫ G.map f = G.map h ≫ G.map g) ≫ equalizer.ι (G.map f) (G.map g)
C : Type u
inst✝³ : Category C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ G.map (equalizer.lift h w) ≫ equalizerComparison f g G =
    equalizer.lift (G.map h) (_ : G.map h ≫ G.map f = G.map h ≫ G.map g)
apply equalizer.hom_ext
no goals
case h
C : Type u
inst✝³ : Category C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ (G.map (equalizer.lift h w) ≫ equalizerComparison f g G) ≫ equalizer.ι (G.map f) (G.map g) =
    equalizer.lift (G.map h) (_ : G.map h ≫ G.map f = G.map h ≫ G.map g) ≫ equalizer.ι (G.map f) (G.map g)
simp [← G.map_comp]