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_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)
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)
⊢ 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:
congr 1
-- 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)
e_a :
  Eq (α := (pullback f f).obj (P := Presheaf.IsSheaf J) ⟶ G.obj (P := Presheaf.IsSheaf J))
    ((InducedCategory.Hom.hom (pullback.fst f f) ≫ p) ≫ i) ((InducedCategory.Hom.hom (pullback.snd f f) ≫ p) ≫ i)
⊢ 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:
rw [← cancel_mono i]

Premises used: CategoryTheory.cancel_mono
-- 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)
⊢ Eq (α := (pullback f f).obj (P := Presheaf.IsSheaf J) ⟶ G.obj (P := Presheaf.IsSheaf J))
    ((InducedCategory.Hom.hom (pullback.fst f f) ≫ p) ≫ i) ((InducedCategory.Hom.hom (pullback.snd f f) ≫ p) ≫ i)

Tactic:
simp [hpi, ← ObjectProperty.FullSubcategory.comp_hom, pullback.condition]

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.comp_hom, CategoryTheory.Limits.pullback.condition
-- 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)
⊢ IsRegularEpi p

Tactic:
have := IsRegularEpiCategory.regularEpiOfEpi 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_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 : IsRegularEpi p
⊢ IsColimit (F :=
    parallelPair (X := Functor.obj (presheafToSheaf J D) ((pullback f f).obj (P := Presheaf.IsSheaf J)))
      (Functor.map (presheafToSheaf J D) (InducedCategory.Hom.hom (pullback.fst f f)))
      (Functor.map (presheafToSheaf J D) (InducedCategory.Hom.hom (pullback.snd f f))))
    (Cofork.ofπ (Functor.map (presheafToSheaf J D) p) ⋯)

Tactic:
exact isColimitCoforkMapOfIsColimit (presheafToSheaf J D) _
          (isColimitCoforkOfEffectiveEpi p _
            (PullbackCone.isLimitOfFactors f.hom f.hom i _ _ hpi hpi _
              ((isLimitPullbackConeMapOfIsLimit (sheafToPresheaf _ _) _
                (pullbackIsPullback f f)))))

Premises used: CategoryTheory.Limits.PullbackCone.isLimitOfFactors, CategoryTheory.Limits.isColimitCoforkMapOfIsColimit, CategoryTheory.isColimitCoforkOfEffectiveEpi, CategoryTheory.presheafToSheaf, CategoryTheory.Limits.pullbackIsPullback, CategoryTheory.Limits.isLimitPullbackConeMapOfIsLimit, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.sheafToPresheaf
-- 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)
⊢ IsRegularEpi (X := Functor.obj (presheafToSheaf J D) (F.obj (P := Presheaf.IsSheaf J)))
    (Functor.map (presheafToSheaf J D) p)

Tactic:
exact ⟨⟨{
      W := (presheafToSheaf J D).obj (pullback f f).obj
      left := (presheafToSheaf J D).map (pullback.fst f f).hom
      right := (presheafToSheaf J D).map (pullback.snd f f).hom
      w := by
        rw [← Functor.map_comp, ← Functor.map_comp]
        congr 1
        rw [← cancel_mono i]
        simp [hpi, ← ObjectProperty.FullSubcategory.comp_hom, pullback.condition]
      isColimit := by
        have := IsRegularEpiCategory.regularEpiOfEpi p
        exact isColimitCoforkMapOfIsColimit (presheafToSheaf J D) _
          (isColimitCoforkOfEffectiveEpi p _
            (PullbackCone.isLimitOfFactors f.hom f.hom i _ _ hpi hpi _
              ((isLimitPullbackConeMapOfIsLimit (sheafToPresheaf _ _) _
                (pullbackIsPullback f 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.35922, u_2} D
J : GrothendieckTopology.{u_3, u_1} C
inst_2 : HasSheafify J (Type u)
F G : Sheaf J (Type u)
f : F ⟶ G
hf : Epi f
⊢ CategoryStruct.comp (Y := image f.hom) (factorThruImage f.hom) (image.ι f.hom) = f.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.RegularEpi
Goal:
C_1 : Type u_1
D : Type u_2
inst : Category.{?u.37946, u_1} C_1
inst_1 : Category.{?u.37950, u_2} D
C : Type u
inst_2 : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
⊢ IsRegularEpiCategory (Sheaf J (Type (max u v)))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X_1 : C
S : Sieve.{v₁, u₁} X_1
R : Presieve.{v₁, u₁} X_1
E : Aᵒᵖ
π : (S.arrows.diagram.op ⋙ P).cones.obj E
X Y : C
f : X ⟶ X_1
g : Y ⟶ X
hf : S.arrows f
⊢ g ≫ (S.arrows.categoryMk f hf).obj (P := fun (f : Over.{v₁, u₁} X_1) ↦ S.arrows f.hom).hom =
    (S.arrows.categoryMk (g ≫ f) ⋯).obj (P := fun (f : Over.{v₁, u₁} X_1) ↦ S.arrows f.hom).hom

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X_1 : C
S : Sieve.{v₁, u₁} X_1
R : Presieve.{v₁, u₁} X_1
E : Aᵒᵖ
π : (S.arrows.diagram.op ⋙ P).cones.obj E
X Y : C
f : X ⟶ X_1
g : Y ⟶ X
hf : S.arrows f
φ : S.arrows.categoryMk (g ≫ f) ⋯ ⟶ S.arrows.categoryMk f hf :=
  ObjectProperty.homMk (P := fun (f : Over.{v₁, u₁} X_1) ↦ S.arrows f.hom) (Over.homMk g ⋯)
⊢ Eq (α := (P ⋙ Functor.obj coyoneda E).obj (op Y))
    ((fun (x : C) (f : x ⟶ X_1) (h : S.arrows f) ↦
          (π.app
              (op
                (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v₁, u₁} X_1) ↦ S.arrows f.hom) (Over.mk f) h)) :
            Functor.obj (C := S.arrows.categoryᵒᵖ)
                (unop (Functor.obj (Functor.op (Functor.const S.arrows.categoryᵒᵖ)) E))
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v₁, u₁} X_1) ↦ S.arrows f.hom) (Over.mk f)
                    h)) ⟶
              (S.arrows.diagram.op ⋙ P).obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v₁, u₁} X_1) ↦ S.arrows f.hom) (Over.mk f)
                    h))))
        Y (g ≫ f) ⋯ :
      Functor.obj (C := S.arrows.categoryᵒᵖ) (unop (Functor.obj (Functor.op (Functor.const S.arrows.categoryᵒᵖ)) E))
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v₁, u₁} X_1) ↦ S.arrows f.hom) (Over.mk (g ≫ f))
              ⋯)) ⟶
        (S.arrows.diagram.op ⋙ P).obj
          (op
            (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v₁, u₁} X_1) ↦ S.arrows f.hom) (Over.mk (g ≫ f))
              ⋯)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((P ⋙ Functor.obj coyoneda E).map g.op) :
          (a : (fun (X : Type v₂) ↦ X) ((P ⋙ coyoneda.obj E).obj (op X))) →
            (fun (X : Type v₂) ↦ X) ((P ⋙ coyoneda.obj E).obj (op Y)))
        ((fun (x : C) (f : x ⟶ X_1) (h : S.arrows f) ↦
            (π.app
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v₁, u₁} X_1) ↦ S.arrows f.hom) (Over.mk f)
                    h)) :
              Functor.obj (C := S.arrows.categoryᵒᵖ)
                  (unop (Functor.obj (Functor.op (Functor.const S.arrows.categoryᵒᵖ)) E))
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v₁, u₁} X_1) ↦ S.arrows f.hom) (Over.mk f)
                      h)) ⟶
                (S.arrows.diagram.op ⋙ P).obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v₁, u₁} X_1) ↦ S.arrows f.hom) (Over.mk f)
                      h))))
          X f hf) :
      (fun (X : Type v₂) ↦ X) ((P ⋙ Functor.obj coyoneda E).obj (op Y)))

Tactic:
simpa using π.naturality φ.op

Premises used: Quiver.Hom.op, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
E : Aᵒᵖ
x : { x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows // x.SieveCompatible }
f f' : S.arrows.categoryᵒᵖ
g : f ⟶ f'
⊢ (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom) ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((P ⋙ Functor.obj coyoneda E).map (Over.Hom.left g.unop.hom).op) :
        (a : (fun (X : Type v₂) ↦ X) ((P ⋙ coyoneda.obj E).obj (op (unop f).obj.left))) →
          (fun (X : Type v₂) ↦ X) ((P ⋙ coyoneda.obj E).obj (op (unop f').obj.left)))
      ((↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯)

Tactic:
have := x.2 f.unop.1.hom g.unop.hom.left f.unop.2
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
E : Aᵒᵖ
x : { x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows // x.SieveCompatible }
f f' : S.arrows.categoryᵒᵖ
g : f ⟶ f'
this :
  (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom) ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((P ⋙ Functor.obj coyoneda E).map (Over.Hom.left g.unop.hom).op) :
        (a : (fun (X : Type v₂) ↦ X) ((P ⋙ coyoneda.obj E).obj (op (unop f).obj.left))) →
          (fun (X : Type v₂) ↦ X) ((P ⋙ coyoneda.obj E).obj (op (unop f').obj.left)))
      ((↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯)
dsimp :
  𝟙 (unop E) ≫
      (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ ≫
      P.map (Over.Hom.left g.unop.hom).op
⊢ Functor.map (unop (Functor.obj (Functor.op (Functor.const S.arrows.categoryᵒᵖ)) E)) g ≫
      (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ ≫
      (S.arrows.diagram.op ⋙ P).map g

Tactic:
dsimp at this ⊢
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
E : Aᵒᵖ
x : { x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows // x.SieveCompatible }
f f' : S.arrows.categoryᵒᵖ
g : f ⟶ f'
this :
  (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom) ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ ≫
      P.map (Over.Hom.left g.unop.hom).op
rw :
  (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom) ⋯
⊢ 𝟙 (unop E) ≫
      (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ ≫
      P.map (Over.Hom.left g.unop.hom).op

Tactic:
rw [id_comp, ← this]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sites.Sheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
J : GrothendieckTopology.{v₁, u₁} C
P : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A
X : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
E : Aᵒᵖ
x : { x : FamilyOfElements (P ⋙ Functor.obj coyoneda E) S.arrows // x.SieveCompatible }
f f' : S.arrows.categoryᵒᵖ
g : f ⟶ f'
this :
  (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (Over.Hom.left g.unop.hom ≫ (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom) ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
        (unop f).obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ ≫
      P.map (Over.Hom.left g.unop.hom).op
⊢ (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯ =
    (↑x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows)
      (unop f').obj (P := fun (f : Over.{v₁, u₁} X) ↦ S.arrows f.hom).hom ⋯

Tactic:
rfl

Premises used: rfl