awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
this :
  (ofArrows Z g).bind Ti =
    ofArrows
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))
i : ι
⊢ Membership.mem (γ := Set (Presieve.{v, u} (Z i))) (J.coverings (Z i)) (Ti (g i) ⋯)

Tactic:
hTi _ _
-- Module: Mathlib.CategoryTheory.Sites.Pretopology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks (C := ?m.1) sorry
inst_2 : Limits.HasPullbacks.{v, u} C
J : Precoverage.{v, u} C
inst_3 : J.HasIsos
inst_4 : J.IsStableUnderBaseChange
inst_5 : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve.{v, u} Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
this :
  (ofArrows Z g).bind Ti =
    ofArrows
      (fun (ij : (i : ι) × κ (g i) ⋯) ↦
        W (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)))
      fun (ij : (i : ι) × κ (g i) ⋯) ↦
      p (g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))) ⋯ (ij.snd (β := fun (i : ι) ↦ κ (g i) ⋯)) ≫
        g (ij.fst (β := fun (i : ι) ↦ κ (g i) ⋯))
i : ι
⊢ Membership.mem (γ := Set (Presieve.{v, u} (Z i))) (J.coverings (Z i)) (Ti (g i) ⋯)

Tactic:
exact hTi _ _
-- Module: Mathlib.CategoryTheory.Sites.Pullback
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
D : Type u₃
inst_1 : Category.{v₃, u₃} D
G : Functor.{v₂, v₃, u₂, u₃} C D
A : Type u₁
inst_2 : Category.{v₁, u₁} A
J : GrothendieckTopology.{v₂, u₂} C
K : GrothendieckTopology.{v₃, u₃} D
inst_3 : G.IsContinuous J K
inst_4 : ∀ (F : Functor.{v₂, v₁, u₂, u₁} Cᵒᵖ A), G.op.HasLeftKanExtension F
inst_5 : HasWeakSheafify.{v₃, v₁, u₃, u₁} K A
⊢ IsRightAdjoint (C := Sheaf.{v₂, v₁, u₂, u₁} J A) (G.sheafPushforwardContinuous A J K)

Tactic:
(sheafAdjunctionContinuous G A J K).isRightAdjoint

Premises used: CategoryTheory.Functor.sheafPullbackConstruction.sheafAdjunctionContinuous, CategoryTheory.Adjunction.isRightAdjoint
-- Module: Mathlib.CategoryTheory.Sites.Pullback
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
D : Type u₃
inst_1 : Category.{v₃, u₃} D
G : Functor.{v₂, v₃, u₂, u₃} C D
A : Type u₁
inst_2 : Category.{v₁, u₁} A
J : GrothendieckTopology.{v₂, u₂} C
K : GrothendieckTopology.{v₃, u₃} D
inst_3 : G.IsContinuous J K
inst_4 : ∀ (F : Functor.{v₂, v₁, u₂, u₁} Cᵒᵖ A), G.op.HasLeftKanExtension F
inst_5 : RepresentablyFlat G
inst_6 : HasSheafify.{v₃, v₁, u₃, u₁} K A
inst_7 : HasSheafify.{v₂, v₁, u₂, u₁} J A
inst_8 : PreservesFiniteLimits (C := Functor.{v₂, v₁, u₂, u₁} Cᵒᵖ A) G.op.lan
⊢ PreservesFiniteLimits (C := Functor.{v₂, v₁, u₂, u₁} Cᵒᵖ A) (G.op.lan ⋙ presheafToSheaf K A)

Tactic:
have : PreservesFiniteLimits (G.op.lan ⋙ presheafToSheaf K A) :=
    comp_preservesFiniteLimits _ _
-- Module: Mathlib.CategoryTheory.Sites.Pullback
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
D : Type u₃
inst_1 : Category.{v₃, u₃} D
G : Functor.{v₂, v₃, u₂, u₃} C D
A : Type u₁
inst_2 : Category.{v₁, u₁} A
J : GrothendieckTopology.{v₂, u₂} C
K : GrothendieckTopology.{v₃, u₃} D
inst_3 : G.IsContinuous J K
inst_4 : ∀ (F : Functor.{v₂, v₁, u₂, u₁} Cᵒᵖ A), G.op.HasLeftKanExtension F
inst_5 : RepresentablyFlat G
inst_6 : HasSheafify.{v₃, v₁, u₃, u₁} K A
inst_7 : HasSheafify.{v₂, v₁, u₂, u₁} J A
inst_8 : PreservesFiniteLimits (C := Functor.{v₂, v₁, u₂, u₁} Cᵒᵖ A) G.op.lan
this : PreservesFiniteLimits (C := Functor.{v₂, v₁, u₂, u₁} Cᵒᵖ A) (G.op.lan ⋙ presheafToSheaf K A)
⊢ PreservesFiniteLimits (C := Sheaf.{v₂, v₁, u₂, u₁} J A) (sheafPullback G A J K)

Tactic:
apply comp_preservesFiniteLimits

Premises used: CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Sites.Pullback
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
D : Type u₃
inst_1 : Category.{v₃, u₃} D
G : Functor.{v₂, v₃, u₂, u₃} C D
A : Type u₁
inst_2 : Category.{v₁, u₁} A
J : GrothendieckTopology.{v₂, u₂} C
K : GrothendieckTopology.{v₃, u₃} D
inst_3 : G.IsContinuous J K
inst_4 : ∀ (F : Functor.{v₂, v₁, u₂, u₁} Cᵒᵖ A), G.op.HasLeftKanExtension F
inst_5 : RepresentablyFlat G
inst_6 : HasSheafify.{v₃, v₁, u₃, u₁} K A
inst_7 : HasSheafify.{v₂, v₁, u₂, u₁} J A
inst_8 : PreservesFiniteLimits (C := Functor.{v₂, v₁, u₂, u₁} Cᵒᵖ A) G.op.lan
⊢ PreservesFiniteLimits (C := Sheaf.{v₂, v₁, u₂, u₁} J A) (G.sheafPullback A J K)

Tactic:
preservesFiniteLimits_of_natIso (sheafPullbackIso G A J K).symm

Premises used: CategoryTheory.Functor.sheafPullbackConstruction.sheafPullbackIso, CategoryTheory.Iso.symm, CategoryTheory.Limits.preservesFiniteLimits_of_natIso
-- Module: Mathlib.CategoryTheory.Sites.Pullback
Goal:
C : Type v₁
inst : SmallCategory C
D : Type v₁
inst_1 : SmallCategory D
G : C ⥤ D
A : Type u₁
inst_2 : Category.{v₁, u₁} A
J : GrothendieckTopology C
K : GrothendieckTopology D
FA : A → A → Type u_1
CA : A → Type v₁
inst_3 : (X Y : A) → FunLike.{u_1 + 1, v₁ + 1, v₁ + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory A FA (CC := CA)
inst_5 : PreservesLimits (forget A (FC := FA) (CC := CA))
inst_6 : HasColimits.{v₁, u₁} A
inst_7 : HasLimits.{v₁, u₁} A
inst_8 : PreservesFilteredColimits (forget A (FC := FA) (CC := CA))
inst_9 : ReflectsIsomorphisms (forget A (FC := FA) (CC := CA))
inst_10 : G.IsContinuous J K
⊢ IsRightAdjoint (C := Sheaf J A) (G.sheafPushforwardContinuous A J K)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Sites.Pullback
Goal:
C : Type v₁
inst : SmallCategory C
D : Type v₁
inst_1 : SmallCategory D
G : C ⥤ D
A : Type u₁
inst_2 : Category.{v₁, u₁} A
J : GrothendieckTopology C
K : GrothendieckTopology D
FA : A → A → Type u_1
CA : A → Type v₁
inst_3 : (X Y : A) → FunLike.{u_1 + 1, v₁ + 1, v₁ + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory A FA (CC := CA)
inst_5 : PreservesLimits (forget A (FC := FA) (CC := CA))
inst_6 : HasColimits.{v₁, u₁} A
inst_7 : HasLimits.{v₁, u₁} A
inst_8 : PreservesFilteredColimits (forget A (FC := FA) (CC := CA))
inst_9 : ReflectsIsomorphisms (forget A (FC := FA) (CC := CA))
inst_10 : G.IsContinuous J K
inst_11 : RepresentablyFlat G
⊢ PreservesFiniteLimits (C := Sheaf J A) (G.sheafPullback A J K)

Tactic:
apply sheafPullbackConstruction.preservesFiniteLimits

Premises used: CategoryTheory.Functor.sheafPullbackConstruction.preservesFiniteLimits
-- 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
obtain :
  ∀ (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), IsRegularEpi f
⊢ IsRegularEpi f

Tactic:
obtain ⟨I, p, i, hp, hi, hpi⟩ := h f
-- 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
⊢ 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))

Tactic:
simpa [← Category.assoc] using (sheafificationAdjunction J D).counit_naturality f

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.counit_naturality, CategoryTheory.sheafificationAdjunction
-- 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
⊢ 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))

Tactic:
have h₁ : (presheafToSheaf J D).map f.hom =
          (sheafificationAdjunction J D).counit.app F ≫ f ≫
          inv ((sheafificationAdjunction J D).counit.app G) := by
        simpa [← Category.assoc] using (sheafificationAdjunction J D).counit_naturality f
-- 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))
⊢ 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)

Tactic:
simp [h₁]
-- 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))
⊢ 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)

Tactic:
have h₂ : f = inv ((sheafificationAdjunction J D).counit.app F) ≫
        (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G := by
      simp [h₁]
-- 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)
rw :
  Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J))) (Y :=
    Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F ≫
      f ≫ inv (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) G))
⊢ Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) f.hom)

Tactic:
rw [h₁]
-- 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)
⊢ Epi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J))) (Y :=
    Functor.obj (presheafToSheaf J D) (G.obj (P := Presheaf.IsSheaf J)))
    (NatTrans.app (Adjunction.counit (sheafificationAdjunction J D)) F ≫
      f ≫ inv (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)
⊢ 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
-- 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) (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

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 :
  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:
epi_of_epi ((presheafToSheaf J D).map p) _

Premises used: CategoryTheory.epi_of_epi, CategoryTheory.presheafToSheaf, CategoryTheory.Functor.map