-- Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean
theorem Sieve.effectiveEpimorphic_singleton {X Y : C} (f : Y ⟶ X) :
    (Presieve.singleton f).EffectiveEpimorphic ↔ (EffectiveEpi f)

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
⊢ EffectiveEpi f → (Presieve.singleton f).EffectiveEpimorphic

Tactic:
rintro ⟨h⟩

Result:
case mpr.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ (Presieve.singleton f).EffectiveEpimorphic

Proof state:
case mpr.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ Nonempty (IsColimit (generate (Presieve.singleton f)).arrows.cocone)

Tactic:
rw [Sieve.generateSingleton_eq]

Result:
case mpr.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ Nonempty (IsColimit (generateSingleton f).arrows.cocone)

Proof state:
case mpr.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ Nonempty (IsColimit (generateSingleton f).arrows.cocone)

Tactic:
apply Nonempty.map (isColimitOfEffectiveEpiStruct _) h

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
⊢ (Presieve.singleton f).EffectiveEpimorphic → EffectiveEpi f

Tactic:
intro (h : Nonempty _)

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (generate (Presieve.singleton f)).arrows.cocone)
⊢ EffectiveEpi f

Proof state:
case mp.effectiveEpi
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (generateSingleton f).arrows.cocone)
⊢ Nonempty (EffectiveEpiStruct f)

Tactic:
apply Nonempty.map (effectiveEpiStructOfIsColimit _) h

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (generate (Presieve.singleton f)).arrows.cocone)
⊢ EffectiveEpi f

Tactic:
rw [Sieve.generateSingleton_eq] at h

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (generateSingleton f).arrows.cocone)
⊢ EffectiveEpi f

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
⊢ (Presieve.singleton f).EffectiveEpimorphic ↔ EffectiveEpi f

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
⊢ (Presieve.singleton f).EffectiveEpimorphic → EffectiveEpi f

case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
⊢ EffectiveEpi f → (Presieve.singleton f).EffectiveEpimorphic

Proof state:
case mpr.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ (Presieve.singleton f).EffectiveEpimorphic

Tactic:
show Nonempty _

Result:
case mpr.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ Nonempty (IsColimit (generate (Presieve.singleton f)).arrows.cocone)

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (generateSingleton f).arrows.cocone)
⊢ EffectiveEpi f

Tactic:
constructor

Result:
case mp.effectiveEpi
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (generateSingleton f).arrows.cocone)
⊢ Nonempty (EffectiveEpiStruct f)