awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
hex :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq.{v' + 1} (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (NatTrans.app { app := fun (Y : (Over.{v, u} (unop (op X)))ᵒᵖ) ↦ app hG x hx (unop Y).hom, naturality := ⋯ }
        (op (Over.mk g)))
      ((x g hg).app (op (Over.mk (𝟙 Y))))
⊢ x.IsAmalgamation (R := S.arrows)
    { app := fun (Y : (Over.{v, u} (unop (op X)))ᵒᵖ) ↦ app hG x hx (unop Y).hom, naturality := ⋯ }

Tactic:
rw [PresheafHom.isAmalgamation_iff _ _ hx]

Premises used: CategoryTheory.PresheafHom.isAmalgamation_iff
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
Y : C
g : Y ⟶ X
hg : S.arrows g
hex : app hG x hx g = (x g hg).app (op (Over.mk (𝟙 Y)))
⊢ Eq.{v' + 1} (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
      (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
    (NatTrans.app { app := fun (Y : (Over.{v, u} (unop (op X)))ᵒᵖ) ↦ app hG x hx (unop Y).hom, naturality := ⋯ }
      (op (Over.mk g)))
    ((x g hg).app (op (Over.mk (𝟙 Y))))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ S.arrows (𝟙 Y ≫ g)

Tactic:
simpa using hg
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ app hG x hx g ≫ G.map (Quiver.Hom.op (𝟙 Y)) = F.map (Quiver.Hom.op (𝟙 Y)) ≫ (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))

Tactic:
have H := app_cond hG x hx g (𝟙 _) (by simpa using hg)
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
Y : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g ≫ G.map (Quiver.Hom.op (𝟙 Y)) = F.map (Quiver.Hom.op (𝟙 Y)) ≫ (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ app hG x hx g = (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))

Tactic:
rw [op_id, G.map_id, comp_id, F.map_id, id_comp] at H

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp, CategoryTheory.op_id
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
Y : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g = (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
e_self : 𝟙 Y ≫ g = g
⊢ Eq (α := F.obj (op Y) ⟶ G.obj (op Y))
    ((x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y))) :
      (Functor.op (Over.forget (unop (op Y))) ⋙ F).obj (op (Over.mk (𝟙 Y))) ⟶
        (Functor.op (Over.forget (unop (op Y))) ⋙ G).obj (op (Over.mk (𝟙 Y))))
    ((x g hg).app (op (Over.mk (𝟙 Y))))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
Y : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g = (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ 𝟙 Y ≫ g = g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
Y : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g = (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ app hG x hx g = (x g hg).app (op (Over.mk (𝟙 Y)))

Tactic:
exact H.trans (by congr; simp)

Premises used: Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ : x.IsAmalgamation (R := S.arrows) y₁
hy₂ : x.IsAmalgamation (R := S.arrows) y₂
⊢ ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))

Tactic:
rw [PresheafHom.isAmalgamation_iff _ _ hx] at hy₁ hy₂

Premises used: CategoryTheory.PresheafHom.isAmalgamation_iff
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ : x.IsAmalgamation (R := S.arrows) y₁
hy₂ : x.IsAmalgamation (R := S.arrows) y₂
hy₃ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
⊢ ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₂.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))

Tactic:
rw [PresheafHom.isAmalgamation_iff _ _ hx] at hy₁ hy₂

Premises used: CategoryTheory.PresheafHom.isAmalgamation_iff
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hy₂ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₂.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hunique : y₁.app = y₂.app
⊢ y₁ = y₂

Tactic:
apply NatTrans.ext

Premises used: CategoryTheory.NatTrans.ext
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hy₂ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₂.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hunique :
  ∀ (Y : Over.{v, u} X),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op Y) ⟶ (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op Y))
      (y₁.app (op Y)) (y₂.app (op Y))
⊢ y₁.app = y₂.app

Tactic:
ext ⟨Y : Over X⟩

Premises used: CategoryTheory.Over
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hy₂ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₂.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
Y : Over.{v, u} X
hunique :
  ∀ (j : (Sieve.pullback Y.hom S).arrows.categoryᵒᵖ),
    y₁.app (op Y) ≫ (G.mapCone (Sieve.pullback Y.hom S).arrows.cocone.op).π.app j =
      y₂.app (op Y) ≫ (G.mapCone (Sieve.pullback Y.hom S).arrows.cocone.op).π.app j
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op Y) ⟶ (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op Y))
    (y₁.app (op Y)) (y₂.app (op Y))

Tactic:
apply (hG Y.hom).hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Over.hom
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hy₂ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₂.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
Y : Over.{v, u} X
Z : Over.{v, u} Y.left
hZ : (Sieve.pullback Y.hom S).arrows Z.hom
hunique : y₁.app (op Y) ≫ G.map Z.hom.op = y₂.app (op Y) ≫ G.map Z.hom.op
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op Y) ⟶
      ((Sieve.pullback Y.hom S).arrows.diagram.op ⋙ G).obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y.left) ↦ (Sieve.pullback Y.hom S).arrows f.hom)
            Z hZ)))
    (y₁.app (op Y) ≫
      (G.mapCone (Sieve.pullback Y.hom S).arrows.cocone.op).π.app
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y.left) ↦ (Sieve.pullback Y.hom S).arrows f.hom)
            Z hZ)))
    (y₂.app (op Y) ≫
      (G.mapCone (Sieve.pullback Y.hom S).arrows.cocone.op).π.app
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y.left) ↦ (Sieve.pullback Y.hom S).arrows f.hom)
            Z hZ)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hy₂ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₂.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
Y : Over.{v, u} X
Z : Over.{v, u} Y.left
hZ : (Sieve.pullback Y.hom S).arrows Z.hom
φ : Over.mk (Z.hom ≫ Y.hom) ⟶ Y := Over.homMk Z.hom ⋯
⊢ y₁.app (op Y) ≫ G.map Z.hom.op = y₂.app (op Y) ≫ G.map Z.hom.op

Tactic:
(y₁.naturality φ.op).symm.trans (Eq.trans ?_ (y₂.naturality φ.op))

Premises used: CategoryTheory.Over, Quiver.Hom.op, CategoryTheory.CostructuredArrow, CategoryTheory.NatTrans.naturality, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hy₂ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₂.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
Y : Over.{v, u} X
Z : Over.{v, u} Y.left
hZ : (Sieve.pullback Y.hom S).arrows Z.hom
φ : Over.mk (Z.hom ≫ Y.hom) ⟶ Y := Over.homMk Z.hom ⋯
hunique :
  (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₁.app (op (Over.mk (Z.hom ≫ Y.hom))) =
    (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₂.app (op (Over.mk (Z.hom ≫ Y.hom)))
⊢ y₁.app (op Y) ≫ G.map Z.hom.op = y₂.app (op Y) ≫ G.map Z.hom.op

Tactic:
refine (y₁.naturality φ.op).symm.trans (Eq.trans ?_ (y₂.naturality φ.op))

Premises used: Quiver.Hom.op, CategoryTheory.NatTrans.naturality, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
X : C
S : Sieve.{v, u} X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₁.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
hy₂ :
  ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    Eq (α :=
      (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk g)) ⟶
        (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk g)))
      (y₂.app (op (Over.mk g))) ((x g hg).app (op (Over.mk (𝟙 Y))))
Y : Over.{v, u} X
Z : Over.{v, u} Y.left
hZ : (Sieve.pullback Y.hom S).arrows Z.hom
φ : Over.mk (Z.hom ≫ Y.hom) ⟶ Y := Over.homMk Z.hom ⋯
hunique :
  (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ (x (Z.hom ≫ Y.hom) hZ).app (op (Over.mk (𝟙 Z.left))) =
    (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₂.app (op (Over.mk (Z.hom ≫ Y.hom)))
hunique₁ hunique₂ :
  (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₂.app (op (Over.mk (Z.hom ≫ Y.hom))) =
    (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₂.app (op (Over.mk (Z.hom ≫ Y.hom)))
⊢ (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₁.app (op (Over.mk (Z.hom ≫ Y.hom))) =
    (Functor.op (Over.forget (unop (op X))) ⋙ F).map φ.op ≫ y₂.app (op (Over.mk (Z.hom ≫ Y.hom)))

Tactic:
rw [(hy₁ _ _ hZ), ← ((hy₂ _ _ hZ))]
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
hG : IsSheaf J G
rw : Presieve.IsSheaf J (presheafHom F G)
⊢ IsSheaf J (presheafHom F G)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
hG : IsSheaf J G
X : C
S : Sieve.{v, u} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Presieve.IsSheafFor (presheafHom F G) S.arrows

Tactic:
presheafHom_isSheafFor F G S
    (fun _ _ => ((Presheaf.isSheaf_iff_isLimit J G).1 hG _ (J.pullback_stable _ hS)).some)

Premises used: Nonempty.some, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Presheaf.isSheaf_iff_isLimit, Iff.mp, CategoryTheory.presheafHom_isSheafFor, CategoryTheory.Sieve.pullback
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
hG : IsSheaf J G
X : C
S : Sieve.{v, u} X
hS : S ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Presieve.IsSheafFor (presheafHom F G) S.arrows

Tactic:
exact presheafHom_isSheafFor F G S
    (fun _ _ => ((Presheaf.isSheaf_iff_isLimit J G).1 hG _ (J.pullback_stable _ hS)).some)

Premises used: Nonempty.some, CategoryTheory.GrothendieckTopology.pullback_stable, CategoryTheory.Presheaf.isSheaf_iff_isLimit, Iff.mp, CategoryTheory.presheafHom_isSheafFor, CategoryTheory.Sieve.pullback
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F_1 G_1 : Functor.{v, v', u, u'} Cᵒᵖ A
F G : Sheaf.{v, v', u, u'} J A
X : Cᵒᵖ
h :
  ∀
    (φ :
      Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
        (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G)),
    InducedCategory.Hom.hom
        (TypeCat.Fun.toFun
          (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (↾Functor.map (J.overMapPullback A (Quiver.Hom.unop (𝟙 X)))))
          φ) =
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (𝟙
                (Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
                  (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G)))).toFun
          φ).hom
⊢ Eq (α :=
    Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A) (Functor.obj (J.overPullback A (unop X)) F)
        (Functor.obj (J.overPullback A (unop X)) G) ⟶
      Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
        (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G))
    (↾Functor.map (J.overMapPullback A (Quiver.Hom.unop (𝟙 X))) :
      Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
          (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G) ⟶
        Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
          (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G))
    (𝟙
        (Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
          (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G)) :
      Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
          (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G) ⟶
        Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
          (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G))

Tactic:
ext φ : 4
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F_1 G_1 : Functor.{v, v', u, u'} Cᵒᵖ A
F G : Sheaf.{v, v', u, u'} J A
X : Cᵒᵖ
φ :
  Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A) (Functor.obj (J.overPullback A (unop X)) F)
    (Functor.obj (J.overPullback A (unop X)) G)
⊢ InducedCategory.Hom.hom
      (TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (↾Functor.map (J.overMapPullback A (Quiver.Hom.unop (𝟙 X)))))
        φ) =
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (𝟙
              (Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
                (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G)))).toFun
        φ).hom

Tactic:
ConcreteCategory.congr_hom ((presheafHom F.1 G.1).map_id X) φ.1

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.presheafHom, CategoryTheory.Functor.map_id, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Sites.SheafHom
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
F_1 G_1 : Functor.{v, v', u, u'} Cᵒᵖ A
F G : Sheaf.{v, v', u, u'} J A
X : Cᵒᵖ
φ :
  Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A) (Functor.obj (J.overPullback A (unop X)) F)
    (Functor.obj (J.overPullback A (unop X)) G)
⊢ InducedCategory.Hom.hom
      (TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (↾Functor.map (J.overMapPullback A (Quiver.Hom.unop (𝟙 X)))))
        φ) =
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (𝟙
              (Quiver.Hom (V := Sheaf (C := Over.{v, u} (unop X)) (J.over (unop X)) A)
                (Functor.obj (J.overPullback A (unop X)) F) (Functor.obj (J.overPullback A (unop X)) G)))).toFun
        φ).hom

Tactic:
exact ConcreteCategory.congr_hom ((presheafHom F.1 G.1).map_id X) φ.1

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.presheafHom, CategoryTheory.Functor.map_id, CategoryTheory.ConcreteCategory.congr_hom