awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
J : GrothendieckTopology.{u_3, u_1} C
inst_2 : HasPullbacks.{u_4, u_2} D
inst_3 : HasPushouts.{u_4, u_2} D
inst_4 : IsRegularEpiCategory.{u_4, u_2} D
h :
  ∀ {F G : Sheaf.{u_3, u_4, u_1, u_2} J D} (f : F ⟶ G) [Epi f],
    ∃ (I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D) (p : F.obj (P := Presheaf.IsSheaf J) ⟶ I) (i :
      I ⟶ G.obj (P := Presheaf.IsSheaf J)), Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst_5 : HasSheafify.{u_3, u_4, u_1, u_2} J D
inst_6 : Balanced (Sheaf.{u_3, u_4, u_1, u_2} J D)
F G : Sheaf.{u_3, u_4, u_1, u_2} J D
f : F ⟶ G
h_1 : Epi f
I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D
p : F.obj (P := Presheaf.IsSheaf J) ⟶ I
i : I ⟶ G.obj (P := Presheaf.IsSheaf J)
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  Eq (α :=
    Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)) ⟶
      Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F ≫
      f ≫ inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))
h₂ :
  f =
    CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G)
this :
  Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) p ≫ Functor.map (presheafToSheaf J D) i)
⊢ Epi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)

Tactic:
exact epi_of_epi ((presheafToSheaf J D).map p) _

Premises used: CategoryTheory.epi_of_epi, CategoryTheory.presheafToSheaf, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Sites.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
J : GrothendieckTopology.{u_3, u_1} C
inst_2 : HasPullbacks.{u_4, u_2} D
inst_3 : HasPushouts.{u_4, u_2} D
inst_4 : IsRegularEpiCategory.{u_4, u_2} D
h :
  ∀ {F G : Sheaf.{u_3, u_4, u_1, u_2} J D} (f : F ⟶ G) [Epi f],
    ∃ (I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D) (p : F.obj (P := Presheaf.IsSheaf J) ⟶ I) (i :
      I ⟶ G.obj (P := Presheaf.IsSheaf J)), Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst_5 : HasSheafify.{u_3, u_4, u_1, u_2} J D
inst_6 : Balanced (Sheaf.{u_3, u_4, u_1, u_2} J D)
F G : Sheaf.{u_3, u_4, u_1, u_2} J D
f : F ⟶ G
h_1 : Epi f
I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D
p : F.obj (P := Presheaf.IsSheaf J) ⟶ I
i : I ⟶ G.obj (P := Presheaf.IsSheaf J)
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  Eq (α :=
    Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)) ⟶
      Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F ≫
      f ≫ inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))
h₂ :
  f =
    CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G)
this :
  Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
⊢ Epi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)

Tactic:
have : Epi ((presheafToSheaf J D).map i) := by
      rw [← hpi, Functor.map_comp] at this
      exact epi_of_epi ((presheafToSheaf J D).map p) _
-- Module: Mathlib.CategoryTheory.Sites.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
J : GrothendieckTopology.{u_3, u_1} C
inst_2 : HasPullbacks.{u_4, u_2} D
inst_3 : HasPushouts.{u_4, u_2} D
inst_4 : IsRegularEpiCategory.{u_4, u_2} D
h :
  ∀ {F G : Sheaf.{u_3, u_4, u_1, u_2} J D} (f : F ⟶ G) [Epi f],
    ∃ (I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D) (p : F.obj (P := Presheaf.IsSheaf J) ⟶ I) (i :
      I ⟶ G.obj (P := Presheaf.IsSheaf J)), Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst_5 : HasSheafify.{u_3, u_4, u_1, u_2} J D
inst_6 : Balanced (Sheaf.{u_3, u_4, u_1, u_2} J D)
F G : Sheaf.{u_3, u_4, u_1, u_2} J D
f : F ⟶ G
h_1 : Epi f
I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D
p : F.obj (P := Presheaf.IsSheaf J) ⟶ I
i : I ⟶ G.obj (P := Presheaf.IsSheaf J)
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  Eq (α :=
    Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)) ⟶
      Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F ≫
      f ≫ inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))
h₂ :
  f =
    CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G)
this_1 :
  Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
this : Epi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
⊢ IsIso (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)

Tactic:
have : IsIso ((presheafToSheaf J D).map i) :=
      Balanced.isIso_of_mono_of_epi _
-- Module: Mathlib.CategoryTheory.Sites.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
J : GrothendieckTopology.{u_3, u_1} C
inst_2 : HasPullbacks.{u_4, u_2} D
inst_3 : HasPushouts.{u_4, u_2} D
inst_4 : IsRegularEpiCategory.{u_4, u_2} D
h :
  ∀ {F G : Sheaf.{u_3, u_4, u_1, u_2} J D} (f : F ⟶ G) [Epi f],
    ∃ (I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D) (p : F.obj (P := Presheaf.IsSheaf J) ⟶ I) (i :
      I ⟶ G.obj (P := Presheaf.IsSheaf J)), Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst_5 : HasSheafify.{u_3, u_4, u_1, u_2} J D
inst_6 : Balanced (Sheaf.{u_3, u_4, u_1, u_2} J D)
F G : Sheaf.{u_3, u_4, u_1, u_2} J D
f : F ⟶ G
h_1 : Epi f
I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D
p : F.obj (P := Presheaf.IsSheaf J) ⟶ I
i : I ⟶ G.obj (P := Presheaf.IsSheaf J)
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  Eq (α :=
    Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)) ⟶
      Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F ≫
      f ≫ inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))
h₂ :
  f =
    CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G)
this_1 :
  Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
this_2 : Epi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
this : IsIso (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
rw :
  EffectiveEpi
    (CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))
⊢ IsRegularEpi f

Tactic:
rw [h₂, isRegularEpi_iff_effectiveEpi]

Premises used: CategoryTheory.isRegularEpi_iff_effectiveEpi
-- Module: Mathlib.CategoryTheory.Sites.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
J : GrothendieckTopology.{u_3, u_1} C
inst_2 : HasPullbacks.{u_4, u_2} D
inst_3 : HasPushouts.{u_4, u_2} D
inst_4 : IsRegularEpiCategory.{u_4, u_2} D
h :
  ∀ {F G : Sheaf.{u_3, u_4, u_1, u_2} J D} (f : F ⟶ G) [Epi f],
    ∃ (I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D) (p : F.obj (P := Presheaf.IsSheaf J) ⟶ I) (i :
      I ⟶ G.obj (P := Presheaf.IsSheaf J)), Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst_5 : HasSheafify.{u_3, u_4, u_1, u_2} J D
inst_6 : Balanced (Sheaf.{u_3, u_4, u_1, u_2} J D)
F G : Sheaf.{u_3, u_4, u_1, u_2} J D
f : F ⟶ G
h_1 : Epi f
I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D
p : F.obj (P := Presheaf.IsSheaf J) ⟶ I
i : I ⟶ G.obj (P := Presheaf.IsSheaf J)
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  Eq (α :=
    Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)) ⟶
      Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F ≫
      f ≫ inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))
h₂ :
  f =
    CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G)
this_1 :
  Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
this_2 : Epi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
this_3 : IsIso (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
this :
  EffectiveEpi (X := Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
⊢ EffectiveEpi
    (CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
J : GrothendieckTopology.{u_3, u_1} C
inst_2 : HasPullbacks.{u_4, u_2} D
inst_3 : HasPushouts.{u_4, u_2} D
inst_4 : IsRegularEpiCategory.{u_4, u_2} D
h :
  ∀ {F G : Sheaf.{u_3, u_4, u_1, u_2} J D} (f : F ⟶ G) [Epi f],
    ∃ (I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D) (p : F.obj (P := Presheaf.IsSheaf J) ⟶ I) (i :
      I ⟶ G.obj (P := Presheaf.IsSheaf J)), Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst_5 : HasSheafify.{u_3, u_4, u_1, u_2} J D
inst_6 : Balanced (Sheaf.{u_3, u_4, u_1, u_2} J D)
F G : Sheaf.{u_3, u_4, u_1, u_2} J D
f : F ⟶ G
h_1 : Epi f
I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D
p : F.obj (P := Presheaf.IsSheaf J) ⟶ I
i : I ⟶ G.obj (P := Presheaf.IsSheaf J)
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  Eq (α :=
    Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)) ⟶
      Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F ≫
      f ≫ inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))
h₂ :
  f =
    CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G)
this_1 :
  Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
this_2 : Epi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
this : IsIso (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
suffices :
  EffectiveEpi (X := Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
⊢ EffectiveEpi
    (CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))

Tactic:
suffices EffectiveEpi ((presheafToSheaf J D).map f.hom) by infer_instance
-- Module: Mathlib.CategoryTheory.Sites.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
J : GrothendieckTopology.{u_3, u_1} C
inst_2 : HasPullbacks.{u_4, u_2} D
inst_3 : HasPushouts.{u_4, u_2} D
inst_4 : IsRegularEpiCategory.{u_4, u_2} D
h :
  ∀ {F G : Sheaf.{u_3, u_4, u_1, u_2} J D} (f : F ⟶ G) [Epi f],
    ∃ (I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D) (p : F.obj (P := Presheaf.IsSheaf J) ⟶ I) (i :
      I ⟶ G.obj (P := Presheaf.IsSheaf J)), Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst_5 : HasSheafify.{u_3, u_4, u_1, u_2} J D
inst_6 : Balanced (Sheaf.{u_3, u_4, u_1, u_2} J D)
F G : Sheaf.{u_3, u_4, u_1, u_2} J D
f : F ⟶ G
h_1 : Epi f
I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D
p : F.obj (P := Presheaf.IsSheaf J) ⟶ I
i : I ⟶ G.obj (P := Presheaf.IsSheaf J)
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  Eq (α :=
    Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)) ⟶
      Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F ≫
      f ≫ inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))
h₂ :
  f =
    CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G)
this_1 :
  Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
this_2 : Epi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
this : IsIso (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
rw :
  EffectiveEpi (X := Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) p ≫ Functor.map (presheafToSheaf J D) i)
⊢ EffectiveEpi (X := Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)

Tactic:
rw [← hpi, Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sites.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
J : GrothendieckTopology.{u_3, u_1} C
inst_2 : HasPullbacks.{u_4, u_2} D
inst_3 : HasPushouts.{u_4, u_2} D
inst_4 : IsRegularEpiCategory.{u_4, u_2} D
h :
  ∀ {F G : Sheaf.{u_3, u_4, u_1, u_2} J D} (f : F ⟶ G) [Epi f],
    ∃ (I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D) (p : F.obj (P := Presheaf.IsSheaf J) ⟶ I) (i :
      I ⟶ G.obj (P := Presheaf.IsSheaf J)), Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst_5 : HasSheafify.{u_3, u_4, u_1, u_2} J D
inst_6 : Balanced (Sheaf.{u_3, u_4, u_1, u_2} J D)
F G : Sheaf.{u_3, u_4, u_1, u_2} J D
f : F ⟶ G
h_1 : Epi f
I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D
p : F.obj (P := Presheaf.IsSheaf J) ⟶ I
i : I ⟶ G.obj (P := Presheaf.IsSheaf J)
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  Eq (α :=
    Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)) ⟶
      Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F ≫
      f ≫ inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))
h₂ :
  f =
    CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G)
this_1 :
  Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
this_2 : Epi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
this_3 : IsIso (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
this : EffectiveEpi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) p)
⊢ EffectiveEpi (X := Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) p ≫ Functor.map (presheafToSheaf J D) i)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
J : GrothendieckTopology.{u_3, u_1} C
inst_2 : HasPullbacks.{u_4, u_2} D
inst_3 : HasPushouts.{u_4, u_2} D
inst_4 : IsRegularEpiCategory.{u_4, u_2} D
h :
  ∀ {F G : Sheaf.{u_3, u_4, u_1, u_2} J D} (f : F ⟶ G) [Epi f],
    ∃ (I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D) (p : F.obj (P := Presheaf.IsSheaf J) ⟶ I) (i :
      I ⟶ G.obj (P := Presheaf.IsSheaf J)), Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst_5 : HasSheafify.{u_3, u_4, u_1, u_2} J D
inst_6 : Balanced (Sheaf.{u_3, u_4, u_1, u_2} J D)
F G : Sheaf.{u_3, u_4, u_1, u_2} J D
f : F ⟶ G
h_1 : Epi f
I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D
p : F.obj (P := Presheaf.IsSheaf J) ⟶ I
i : I ⟶ G.obj (P := Presheaf.IsSheaf J)
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  Eq (α :=
    Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)) ⟶
      Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F ≫
      f ≫ inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))
h₂ :
  f =
    CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G)
this_1 :
  Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
this_2 : Epi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
this : IsIso (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
suffices : EffectiveEpi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) p)
⊢ EffectiveEpi (X := Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) p ≫ Functor.map (presheafToSheaf J D) i)

Tactic:
suffices EffectiveEpi ((presheafToSheaf J D).map p) by infer_instance
-- Module: Mathlib.CategoryTheory.Sites.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
J : GrothendieckTopology.{u_3, u_1} C
inst_2 : HasPullbacks.{u_4, u_2} D
inst_3 : HasPushouts.{u_4, u_2} D
inst_4 : IsRegularEpiCategory.{u_4, u_2} D
h :
  ∀ {F G : Sheaf.{u_3, u_4, u_1, u_2} J D} (f : F ⟶ G) [Epi f],
    ∃ (I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D) (p : F.obj (P := Presheaf.IsSheaf J) ⟶ I) (i :
      I ⟶ G.obj (P := Presheaf.IsSheaf J)), Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst_5 : HasSheafify.{u_3, u_4, u_1, u_2} J D
inst_6 : Balanced (Sheaf.{u_3, u_4, u_1, u_2} J D)
F G : Sheaf.{u_3, u_4, u_1, u_2} J D
f : F ⟶ G
h_1 : Epi f
I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D
p : F.obj (P := Presheaf.IsSheaf J) ⟶ I
i : I ⟶ G.obj (P := Presheaf.IsSheaf J)
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  Eq (α :=
    Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)) ⟶
      Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F ≫
      f ≫ inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))
h₂ :
  f =
    CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G)
this_1 :
  Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
this_2 : Epi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
this : IsIso (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
rw :
  IsRegularEpi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) p)
⊢ EffectiveEpi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) p)

Tactic:
rw [← isRegularEpi_iff_effectiveEpi]

Premises used: CategoryTheory.isRegularEpi_iff_effectiveEpi
-- Module: Mathlib.CategoryTheory.Sites.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
J : GrothendieckTopology.{u_3, u_1} C
inst_2 : HasPullbacks.{u_4, u_2} D
inst_3 : HasPushouts.{u_4, u_2} D
inst_4 : IsRegularEpiCategory.{u_4, u_2} D
h :
  ∀ {F G : Sheaf.{u_3, u_4, u_1, u_2} J D} (f : F ⟶ G) [Epi f],
    ∃ (I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D) (p : F.obj (P := Presheaf.IsSheaf J) ⟶ I) (i :
      I ⟶ G.obj (P := Presheaf.IsSheaf J)), Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst_5 : HasSheafify.{u_3, u_4, u_1, u_2} J D
inst_6 : Balanced (Sheaf.{u_3, u_4, u_1, u_2} J D)
F G : Sheaf.{u_3, u_4, u_1, u_2} J D
f : F ⟶ G
h_1 : Epi f
I : Functor.{u_3, u_4, u_1, u_2} Cᵒᵖ D
p : F.obj (P := Presheaf.IsSheaf J) ⟶ I
i : I ⟶ G.obj (P := Presheaf.IsSheaf J)
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  Eq (α :=
    Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)) ⟶
      Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F ≫
      f ≫ inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))
h₂ :
  f =
    CategoryStruct.comp (Y := Functor.obj (sheafToPresheaf J D ⋙ presheafToSheaf J D) F)
      (inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F))
      (Functor.map (presheafToSheaf J D) f.hom ≫ NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G)
this_1 :
  Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
this_2 : Epi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
this : IsIso (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) i)
rw :
  Eq (α :=
    Functor.obj (presheafToSheaf J D) ((pullback f f).obj (P := Presheaf.IsSheaf J)) ⟶
      Functor.obj (presheafToSheaf J D) I)
    (Functor.map (presheafToSheaf J D) (InducedCategory.Hom.hom (pullback.fst f f) ≫ p))
    (Functor.map (presheafToSheaf J D) (InducedCategory.Hom.hom (pullback.snd f f) ≫ p))
⊢ Eq (α :=
    Functor.obj (presheafToSheaf J D) ((pullback f f).obj (P := Presheaf.IsSheaf J)) ⟶
      Functor.obj (presheafToSheaf J D) I)
    (Functor.map (presheafToSheaf J D) (InducedCategory.Hom.hom (pullback.fst f f)) ≫
      Functor.map (presheafToSheaf J D) p)
    (Functor.map (presheafToSheaf J D) (InducedCategory.Hom.hom (pullback.snd f f)) ≫
      Functor.map (presheafToSheaf J D) p)

Tactic:
rw [← Functor.map_comp, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp