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
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y : (presheafHom F G).obj (op X)
h :
  ∀ (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
W : Over.{v, u} Y
H :
  x (W.hom ≫ g) ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map W.hom.op) :
        (a : (presheafHom F G).obj (op Y)) → (presheafHom F G).obj (op W.left))
      (x g hg)
⊢ Eq (α :=
    (Functor.op (Over.forget (unop (op X))) ⋙ F).obj (op (Over.mk (W.hom ≫ g))) ⟶
      (Functor.op (Over.forget (unop (op X))) ⋙ G).obj (op (Over.mk (W.hom ≫ g))))
    ((x g hg).app (op (Over.mk W.hom))) ((x g hg).app (op W))

Tactic:
rfl
-- 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
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z₁ : Over.{v, u} Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over.{v, u} Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
dsimp :
  𝟙 (F.obj (op Y)) ≫ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    (F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left)))) ≫ G.map (Over.Hom.left f).op
⊢ Eq.{v' + 1} (α :=
    Functor.obj (C := (Sieve.pullback g S).arrows.categoryᵒᵖ)
        (Functor.obj (Functor.const (Sieve.pullback g S).arrows.categoryᵒᵖ) (F.obj (op Y)))
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y) ↦ (Sieve.pullback g S).arrows f.hom) Z₁
            hZ₁)) ⟶
      ((Sieve.pullback g S).arrows.diagram.op ⋙ G).obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y) ↦ (Sieve.pullback g S).arrows f.hom) Z₂
            hZ₂)))
    (CategoryStruct.comp (Y :=
      Functor.obj (C := (Sieve.pullback g S).arrows.categoryᵒᵖ)
        (Functor.obj (Functor.const (Sieve.pullback g S).arrows.categoryᵒᵖ) (F.obj (op Y)))
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y) ↦ (Sieve.pullback g S).arrows f.hom) Z₂
            hZ₂)))
      (Functor.map (Functor.obj (Functor.const (Sieve.pullback g S).arrows.categoryᵒᵖ) (F.obj (op Y)))
        (op { hom := f }))
      (match (motive :=
        (x : (Sieve.pullback g S).arrows.categoryᵒᵖ) →
          Functor.obj (Functor.obj (Functor.const (Sieve.pullback g S).arrows.categoryᵒᵖ) (F.obj (op Y))) x ⟶
            ((Sieve.pullback g S).arrows.diagram.op ⋙ G).obj x)
        op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y) ↦ (Sieve.pullback g S).arrows f.hom) Z₂
            hZ₂) with
      | op { obj := Z, property := hZ } =>
        F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left)))))))
    (CategoryStruct.comp (Y :=
      ((Sieve.pullback g S).arrows.diagram.op ⋙ G).obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y) ↦ (Sieve.pullback g S).arrows f.hom) Z₁
            hZ₁)))
      (match (motive :=
        (x : (Sieve.pullback g S).arrows.categoryᵒᵖ) →
          Functor.obj (Functor.obj (Functor.const (Sieve.pullback g S).arrows.categoryᵒᵖ) (F.obj (op Y))) x ⟶
            ((Sieve.pullback g S).arrows.diagram.op ⋙ G).obj x)
        op
          (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} Y) ↦ (Sieve.pullback g S).arrows f.hom) Z₁
            hZ₁) with
      | op { obj := Z, property := hZ } =>
        F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left))))))
      (((Sieve.pullback g S).arrows.diagram.op ⋙ G).map (op { hom := f })))

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
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z₁ : Over.{v, u} Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over.{v, u} Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
rw :
  F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left f).op
⊢ 𝟙 (F.obj (op Y)) ≫ F.map Z₂.hom.op ≫ (x (Z₂.hom ≫ g) hZ₂).app (op (Over.mk (𝟙 Z₂.left))) =
    (F.map Z₁.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left)))) ≫ G.map (Over.Hom.left f).op

Tactic:
rw [id_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.id_comp
-- 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
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z₁ : Over.{v, u} Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over.{v, u} Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
⊢ Over.Hom.left f ≫ Z₁.hom ≫ g = 𝟙 Z₂.left ≫ Z₂.hom ≫ 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
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z₁ : Over.{v, u} Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over.{v, u} Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
⊢ Eq (α := (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₁.left))) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
        (x (Z₁.hom ≫ g) hZ₁) :
      (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Quiver.Hom.op (𝟙 Z₂.left))) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left))) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
        (x (Z₂.hom ≫ g) hZ₂) :
      (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))

Tactic:
have H := hx f.left (𝟙 _) hZ₁ hZ₂ (by 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
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z₁ : Over.{v, u} Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over.{v, u} Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H :
  Eq (α := (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₁.left))) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
        (x (Z₁.hom ≫ g) hZ₁) :
      (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Quiver.Hom.op (𝟙 Z₂.left))) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left))) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
        (x (Z₂.hom ≫ g) hZ₂) :
      (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Z₂.left)))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
        (a : (presheafHom F G).obj (op Z₁.left)) → (presheafHom F G).obj (op Z₂.left))
      (x (Z₁.hom ≫ g) hZ₁) =
    x (Z₂.hom ≫ g) hZ₂

Tactic:
simp only [op_id, Functor.map_id, id_apply] at H

Premises used: CategoryTheory.id_apply, CategoryTheory.Functor.map_id, 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
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z₁ : Over.{v, u} Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over.{v, u} Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Over.Hom.left f).op) :
        (a : (presheafHom F G).obj (op Z₁.left)) → (presheafHom F G).obj (op Z₂.left))
      (x (Z₁.hom ≫ g) hZ₁) =
    x (Z₂.hom ≫ g) hZ₂
φ : Over.mk (Over.Hom.left f) ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk (Over.Hom.left f) ⋯
⊢ (Functor.op (Over.forget (unop (op Z₁.left))) ⋙ F).map φ.op ≫
      (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ (Functor.op (Over.forget (unop (op Z₁.left))) ⋙ G).map φ.op

Tactic:
have H' := (x (Z₁.hom ≫ g) hZ₁).naturality φ.op
-- 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
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
c : Cone ((Sieve.pullback g S).arrows.diagram.op ⋙ G) :=
  { pt := F.obj (op Y),
    π :=
      {
        app := fun (x_1 : (Sieve.pullback g S).arrows.categoryᵒᵖ) ↦
          match (motive :=
            (x : (Sieve.pullback g S).arrows.categoryᵒᵖ) →
              Functor.obj (Functor.obj (Functor.const (Sieve.pullback g S).arrows.categoryᵒᵖ) (F.obj (op Y))) x ⟶
                ((Sieve.pullback g S).arrows.diagram.op ⋙ G).obj x)
            x_1 with
          | op { obj := Z, property := hZ } =>
            F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left))))),
        naturality := ⋯ } }
h :
  ∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (p ≫ g)),
    (hG g).lift c ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))
⊢ ∃ (φ : F.obj (op Y) ⟶ G.obj (op Y)),
    ∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (p ≫ g)), φ ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))

Tactic:
use (hG g).lift c

Premises used: CategoryTheory.Limits.IsLimit.lift
-- 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
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
c : Cone ((Sieve.pullback g S).arrows.diagram.op ⋙ G) :=
  { pt := F.obj (op Y),
    π :=
      {
        app := fun (x_1 : (Sieve.pullback g S).arrows.categoryᵒᵖ) ↦
          match (motive :=
            (x : (Sieve.pullback g S).arrows.categoryᵒᵖ) →
              Functor.obj (Functor.obj (Functor.const (Sieve.pullback g S).arrows.categoryᵒᵖ) (F.obj (op Y))) x ⟶
                ((Sieve.pullback g S).arrows.diagram.op ⋙ G).obj x)
            x_1 with
          | op { obj := Z, property := hZ } =>
            F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left))))),
        naturality := ⋯ } }
Z : C
p : Z ⟶ Y
hp : S.arrows (p ≫ g)
⊢ (hG g).lift c ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))

Tactic:
((hG g).fac c ⟨Over.mk p, hp⟩)

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, Quiver.Hom.op, CategoryTheory.Over.mk, Opposite.op, CategoryTheory.Limits.IsLimit.fac
-- 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
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
c : Cone ((Sieve.pullback g S).arrows.diagram.op ⋙ G) :=
  { pt := F.obj (op Y),
    π :=
      {
        app := fun (x_1 : (Sieve.pullback g S).arrows.categoryᵒᵖ) ↦
          match (motive :=
            (x : (Sieve.pullback g S).arrows.categoryᵒᵖ) →
              Functor.obj (Functor.obj (Functor.const (Sieve.pullback g S).arrows.categoryᵒᵖ) (F.obj (op Y))) x ⟶
                ((Sieve.pullback g S).arrows.diagram.op ⋙ G).obj x)
            x_1 with
          | op { obj := Z, property := hZ } =>
            F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op Z.left))))),
        naturality := ⋯ } }
Z : C
p : Z ⟶ Y
hp : S.arrows (p ≫ g)
⊢ (hG g).lift c ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))

Tactic:
exact ((hG g).fac c ⟨Over.mk p, hp⟩)

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Over.mk, Opposite.op, CategoryTheory.Limits.IsLimit.fac
-- 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
Y : C
hx : x.Compatible (R := S.arrows)
g : Y ⟶ X
Z : C
p : Z ⟶ Y
hp : S.arrows (p ≫ g)
⊢ app hG x hx g ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))

Tactic:
(exists_app hG x hx g).choose_spec p hp

Premises used: Exists.choose_spec, CategoryTheory.PresheafHom.IsSheafFor.app, CategoryTheory.PresheafHom.IsSheafFor.exists_app
-- 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 : ∃ (x_1 : (presheafHom F G).obj (op X)), x.IsAmalgamation (R := S.arrows) x_1
hunique :
  ∀ (y₁ y₂ : (presheafHom F G).obj (op X)),
    x.IsAmalgamation (R := S.arrows) y₁ → x.IsAmalgamation (R := S.arrows) y₂ → y₁ = y₂
⊢ ∃! t : (presheafHom F G).obj (op X), x.IsAmalgamation (R := S.arrows) t

Tactic:
apply existsUnique_of_exists_of_unique

Premises used: existsUnique_of_exists_of_unique
-- 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₂ : Over.{v, u} X
φ : Y₂ ⟶ Y₁
apply :
  ∀ (j : (Sieve.pullback Y₂.hom S).arrows.categoryᵒᵖ),
    ((Functor.op (Over.forget (unop (op X))) ⋙ F).map (op φ) ≫ app hG x hx (unop (op Y₂)).hom) ≫
        (G.mapCone (Sieve.pullback Y₂.hom S).arrows.cocone.op).π.app j =
      (app hG x hx (unop (op Y₁)).hom ≫ (Functor.op (Over.forget (unop (op X))) ⋙ G).map (op φ)) ≫
        (G.mapCone (Sieve.pullback Y₂.hom S).arrows.cocone.op).π.app j
⊢ (Functor.op (Over.forget (unop (op X))) ⋙ F).map (op φ) ≫ app hG x hx (unop (op Y₂)).hom =
    app hG x hx (unop (op Y₁)).hom ≫ (Functor.op (Over.forget (unop (op X))) ⋙ G).map (op φ)

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₂ : Over.{v, u} X
φ : Y₂ ⟶ Y₁
Z : Over.{v, u} Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
dsimp :
  (F.map (Over.Hom.left φ).op ≫ app hG x hx Y₂.hom) ≫ G.map Z.hom.op =
    (app hG x hx Y₁.hom ≫ G.map (Over.Hom.left φ).op) ≫ 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)))
    (((Functor.op (Over.forget (unop (op X))) ⋙ F).map (op φ) ≫ app hG x hx (unop (op Y₂)).hom) ≫
      (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)))
    ((app hG x hx (unop (op Y₁)).hom ≫ (Functor.op (Over.forget (unop (op X))) ⋙ G).map (op φ)) ≫
      (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₂ : Over.{v, u} X
φ : Y₂ ⟶ Y₁
Z : Over.{v, u} Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
rw :
  F.map (Over.Hom.left φ).op ≫ F.map Z.hom.op ≫ (x (Z.hom ≫ Y₂.hom) hZ).app (op (Over.mk (𝟙 Z.left))) =
    app hG x hx Y₁.hom ≫ G.map (Z.hom ≫ Over.Hom.left φ).op
⊢ (F.map (Over.Hom.left φ).op ≫ app hG x hx Y₂.hom) ≫ G.map Z.hom.op =
    (app hG x hx Y₁.hom ≫ G.map (Over.Hom.left φ).op) ≫ G.map Z.hom.op

Tactic:
rw [assoc, assoc, app_cond hG x hx Y₂.hom Z.hom hZ, ← G.map_comp, ← op_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.PresheafHom.IsSheafFor.app_cond, CategoryTheory.Functor.map_comp, 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₂ : Over.{v, u} X
φ : Y₂ ⟶ Y₁
Z : Over.{v, u} Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
⊢ S.arrows ((Z.hom ≫ Over.Hom.left φ) ≫ Y₁.hom)

Tactic:
simpa using hZ
-- 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₂ : Over.{v, u} X
φ : Y₂ ⟶ Y₁
Z : Over.{v, u} Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
rw :
  Eq (α := F.obj (op Y₁.left) ⟶ G.obj (op Z.left))
    (F.map ((Over.Hom.left φ).op ≫ Z.hom.op) ≫ (x (Z.hom ≫ Y₂.hom) hZ).app (op (Over.mk (𝟙 Z.left))))
    (F.map ((Over.Hom.left φ).op ≫ Z.hom.op) ≫ (x ((Z.hom ≫ Over.Hom.left φ) ≫ Y₁.hom) ⋯).app (op (Over.mk (𝟙 Z.left))))
⊢ F.map (Over.Hom.left φ).op ≫ F.map Z.hom.op ≫ (x (Z.hom ≫ Y₂.hom) hZ).app (op (Over.mk (𝟙 Z.left))) =
    app hG x hx Y₁.hom ≫ G.map (Z.hom ≫ Over.Hom.left φ).op

Tactic:
rw [app_cond hG x hx Y₁.hom (Z.hom ≫ φ.left) (by simpa using hZ),
            ← F.map_comp_assoc, op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Over.Hom.left, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.CategoryStruct.comp, CategoryTheory.PresheafHom.IsSheafFor.app_cond, 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₂ : Over.{v, u} X
φ : Y₂ ⟶ Y₁
Z : Over.{v, u} Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
e_a : Z.hom ≫ Y₂.hom = (Z.hom ≫ Over.Hom.left φ) ≫ Y₁.hom
⊢ Eq (α := F.obj (op Y₁.left) ⟶ G.obj (op Z.left))
    (F.map ((Over.Hom.left φ).op ≫ Z.hom.op) ≫ (x (Z.hom ≫ Y₂.hom) hZ).app (op (Over.mk (𝟙 Z.left))))
    (F.map ((Over.Hom.left φ).op ≫ Z.hom.op) ≫ (x ((Z.hom ≫ Over.Hom.left φ) ≫ Y₁.hom) ⋯).app (op (Over.mk (𝟙 Z.left))))

Tactic:
congr 3
-- 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₂ : Over.{v, u} X
φ : Y₂ ⟶ Y₁
Z : Over.{v, u} Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
⊢ Z.hom ≫ Y₂.hom = (Z.hom ≫ Over.Hom.left φ) ≫ Y₁.hom

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)
hex :
  x.IsAmalgamation (R := S.arrows)
    { app := fun (Y : (Over.{v, u} (unop (op X)))ᵒᵖ) ↦ app hG x hx (unop Y).hom, naturality := ⋯ }
⊢ ∃ (x_1 : (presheafHom F G).obj (op X)), x.IsAmalgamation (R := S.arrows) x_1

Tactic:
refine ⟨
      { app := fun Y => app hG x hx Y.unop.hom
        naturality := by
          rintro ⟨Y₁ : Over X⟩ ⟨Y₂ : Over X⟩ ⟨φ : Y₂ ⟶ Y₁⟩
          apply (hG Y₂.hom).hom_ext
          rintro ⟨Z : Over Y₂.left, hZ⟩
          dsimp
          rw [assoc, assoc, app_cond hG x hx Y₂.hom Z.hom hZ, ← G.map_comp, ← op_comp]
          rw [app_cond hG x hx Y₁.hom (Z.hom ≫ φ.left) (by simpa using hZ),
            ← F.map_comp_assoc, op_comp]
          congr 3
          simp }, ?_⟩