awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.RegularEpi (hypothesis)
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)
⊢ IsRegularEpi f
have this : Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J))) (Functor.map (presheafToSheaf J D) f.hom)
Tactic: have : Epi ((presheafToSheaf J D).map f.hom) := by
      rw [h₁]
      infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.RegularEpi (hypothesis)
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)
have 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)
Tactic: rw [← hpi, Functor.map_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.RegularEpi (hypothesis)
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)
⊢ IsRegularEpi f
have this₁ : 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) _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.RegularEpi (hypothesis)
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)
⊢ IsRegularEpi f
have this₁ : 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 _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.RegularEpi (goal)
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)
⊢ IsRegularEpi f
have 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))
Tactic: rw [h₂, isRegularEpi_iff_effectiveEpi]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.RegularEpi (goal)
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)
⊢ 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))
have suffices : EffectiveEpi (X := Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
  (Functor.map (presheafToSheaf J D) f.hom)
Tactic: suffices EffectiveEpi ((presheafToSheaf J D).map f.hom) by infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.RegularEpi (goal)
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)
⊢ EffectiveEpi (X := Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)
have 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)
Tactic: rw [← hpi, Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.RegularEpi (goal)
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)
⊢ 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)
have suffices : EffectiveEpi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) p)
Tactic: suffices EffectiveEpi ((presheafToSheaf J D).map p) by infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.RegularEpi (goal)
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)
⊢ EffectiveEpi (X := Functor.obj (presheafToSheaf J D) I) (Functor.map (presheafToSheaf J D) p)
have rw : IsRegularEpi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
  (Functor.map (presheafToSheaf J D) p)
Tactic: rw [← isRegularEpi_iff_effectiveEpi]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.RegularEpi (goal)
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)
⊢ 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)
have 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))
Tactic: rw [← Functor.map_comp, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.RegularEpi (goal)
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)
⊢ 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))
have e_a : Eq (α := (pullback f f).obj (P := Presheaf.IsSheaf J) ⟶ I) (InducedCategory.Hom.hom (pullback.fst f f) ≫ p)
  (InducedCategory.Hom.hom (pullback.snd f f) ≫ p)
Tactic: congr 1