C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
E : Type u₃
inst✝¹ : Category E
F G : C ⥤ D
inst✝ : PreservesEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi f
this : Epi (F.map f ≫ (α.app Y).hom)
⊢ Epi (G.map f)
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
E : Type u₃
inst✝¹ : Category E
F G : C ⥤ D
inst✝ : PreservesEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi f
⊢ Epi (G.map f)
haveI : Epi (F.map f ≫ (α.app Y).hom) := epi_comp _ _
case h.e'_5
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
E : Type u₃
inst✝¹ : Category E
F G : C ⥤ D
inst✝ : PreservesEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi f
this : Epi (F.map f ≫ (α.app Y).hom)
⊢ G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
E : Type u₃
inst✝¹ : Category E
F G : C ⥤ D
inst✝ : PreservesEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi f
this : Epi (F.map f ≫ (α.app Y).hom)
⊢ Epi (G.map f)
convert (epi_comp _ _ : Epi ((α.app X).inv ≫ F.map f ≫ (α.app Y).hom))
no goals
case h.e'_5
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
E : Type u₃
inst✝¹ : Category E
F G : C ⥤ D
inst✝ : PreservesEpimorphisms F
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi f
this : Epi (F.map f ≫ (α.app Y).hom)
⊢ G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom
rw [Iso.eq_inv_comp, Iso.app_hom, Iso.app_hom, NatTrans.naturality]