-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem hasStrongEpiMonoFactorisations_imp_of_isEquivalence (F : C ⥤ D) [IsEquivalence F]
    [h : HasStrongEpiMonoFactorisations C] : HasStrongEpiMonoFactorisations D :=
  ⟨fun {X} {Y} f => by
    let em : StrongEpiMonoFactorisation (F.inv.map f) :=
      (HasStrongEpiMonoFactorisations.has_fac (F.inv.map f)).some
    haveI : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y) := mono_comp _ _
    haveI : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e) := strongEpi_comp _ _
    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

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝ : F.IsEquivalence
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
⊢ Nonempty (StrongEpiMonoFactorisation f)

Tactic:
let em : StrongEpiMonoFactorisation (F.inv.map f) :=
  (HasStrongEpiMonoFactorisations.has_fac (F.inv.map f)).some

Result:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝ : F.IsEquivalence
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
⊢ Nonempty (StrongEpiMonoFactorisation f)

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝ : F.IsEquivalence
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
this✝ : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)
this : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e)
⊢ (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e) ≫ F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y = f

Tactic:
simp only [asEquivalence_functor, Category.assoc, ← F.map_comp_assoc,
  MonoFactorisation.fac, fun_inv_map, id_obj, Iso.inv_hom_id_app, Category.comp_id,
  Iso.inv_hom_id_app_assoc]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝ : F.IsEquivalence
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
this✝ : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)
this : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e)
⊢ Nonempty (StrongEpiMonoFactorisation f)

Tactic:
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
        simp only [asEquivalence_functor, Category.assoc, ← F.map_comp_assoc,
          MonoFactorisation.fac, fun_inv_map, id_obj, Iso.inv_hom_id_app, Category.comp_id,
          Iso.inv_hom_id_app_assoc] }

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝ : F.IsEquivalence
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
this : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)
⊢ Nonempty (StrongEpiMonoFactorisation f)

Tactic:
haveI : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e) := strongEpi_comp _ _

Result:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝ : F.IsEquivalence
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
this✝ : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)
this : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e)
⊢ Nonempty (StrongEpiMonoFactorisation f)

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝ : F.IsEquivalence
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
⊢ Nonempty (StrongEpiMonoFactorisation f)

Tactic:
haveI : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y) := mono_comp _ _

Result:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝ : F.IsEquivalence
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
this : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)
⊢ Nonempty (StrongEpiMonoFactorisation f)