C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
inst✝ : IsEquivalence F
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation ((inv F).map f) :=
  Nonempty.some (_ : Nonempty (StrongEpiMonoFactorisation ((inv F).map f)))
⊢ Nonempty (StrongEpiMonoFactorisation f)
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
inst✝ : IsEquivalence F
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
⊢ Nonempty (StrongEpiMonoFactorisation f)
let em : StrongEpiMonoFactorisation (F.inv.map f) :=
  (HasStrongEpiMonoFactorisations.has_fac (F.inv.map f)).some
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
inst✝ : IsEquivalence F
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation ((inv F).map f) :=
  Nonempty.some (_ : Nonempty (StrongEpiMonoFactorisation ((inv F).map f)))
this : Mono (F.map em.m ≫ (asEquivalence F).counitIso.hom.app Y)
⊢ Nonempty (StrongEpiMonoFactorisation f)
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
inst✝ : IsEquivalence F
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation ((inv F).map f) :=
  Nonempty.some (_ : Nonempty (StrongEpiMonoFactorisation ((inv F).map f)))
⊢ Nonempty (StrongEpiMonoFactorisation f)
haveI : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y) := mono_comp _ _
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
inst✝ : IsEquivalence F
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation ((inv F).map f) :=
  Nonempty.some (_ : Nonempty (StrongEpiMonoFactorisation ((inv F).map f)))
this✝ : Mono (F.map em.m ≫ (asEquivalence F).counitIso.hom.app Y)
this : StrongEpi ((asEquivalence F).counitIso.inv.app X ≫ F.map em.e)
⊢ Nonempty (StrongEpiMonoFactorisation f)
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
inst✝ : IsEquivalence F
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation ((inv F).map f) :=
  Nonempty.some (_ : Nonempty (StrongEpiMonoFactorisation ((inv F).map f)))
this : Mono (F.map em.m ≫ (asEquivalence F).counitIso.hom.app Y)
⊢ Nonempty (StrongEpiMonoFactorisation f)
haveI : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e) := strongEpi_comp _ _
no goals
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
inst✝ : IsEquivalence F
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation ((inv F).map f) :=
  Nonempty.some (_ : Nonempty (StrongEpiMonoFactorisation ((inv F).map f)))
this✝ : Mono (F.map em.m ≫ (asEquivalence F).counitIso.hom.app Y)
this : StrongEpi ((asEquivalence F).counitIso.inv.app X ≫ F.map em.e)
⊢ Nonempty (StrongEpiMonoFactorisation f)
exact
  Nonempty.intro
    { I := F.obj em.I
      e := F.asEquivalence.counitIso.inv.app X ≫ F.map em.e
      m := F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y
      fac := by
        simpa only [Category.assoc, ← F.map_comp_assoc, em.fac, IsEquivalence.fun_inv_map,
          Iso.inv_hom_id_app, Iso.inv_hom_id_app_assoc] using Category.comp_id _ }
no goals
C : Type u_3
D : Type u_4
inst✝² : Category C
inst✝¹ : Category D
F : C ⥤ D
inst✝ : IsEquivalence F
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation ((inv F).map f) :=
  Nonempty.some (_ : Nonempty (StrongEpiMonoFactorisation ((inv F).map f)))
this✝ : Mono (F.map em.m ≫ (asEquivalence F).counitIso.hom.app Y)
this : StrongEpi ((asEquivalence F).counitIso.inv.app X ≫ F.map em.e)
⊢ ((asEquivalence F).counitIso.inv.app X ≫ F.map em.e) ≫ F.map em.m ≫ (asEquivalence F).counitIso.hom.app Y = f
simpa only [Category.assoc, ← F.map_comp_assoc, em.fac, IsEquivalence.fun_inv_map,
  Iso.inv_hom_id_app, Iso.inv_hom_id_app_assoc] using Category.comp_id _