awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X₁ X₂ : C
f : X₂ ⟶ X₁
⊢ Eq (α := F.obj (op X₁) ⟶ G.obj (op X₂))
    (F.map (op f) ≫
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)).app (op (Over.mk f)))
    (F.map f.op ≫
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X₁)).app (op (Over.mk f)))

Tactic:
rfl
-- 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
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
dsimp :
  Subtype.mk (p := fun (x : (j : Cᵒᵖ) → Functor.op (Over.forget (unop j)) ⋙ F ⟶ Functor.op (Over.forget (unop j)) ⋙ G) ↦
      x ∈ (presheafHom F G).sections)
      (fun (x : Cᵒᵖ) ↦
        Functor.whiskerLeft (Functor.op (Over.forget (unop x)))
          {
            app := fun (X : Cᵒᵖ) ↦
              ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) X).app
                (op (Over.mk (𝟙 (unop X)))),
            naturality := ⋯ })
      ⋯ =
    s
⊢ (fun (f : F ⟶ G) ↦
        (Subtype.mk (p := fun (x : (j : Cᵒᵖ) → (presheafHom F G).obj j) ↦ x ∈ (presheafHom F G).sections)
            (fun (x : Cᵒᵖ) ↦ Functor.whiskerLeft (Functor.op (Over.forget (unop x))) f) ⋯ :
          { x : (j : Cᵒᵖ) → (presheafHom F G).obj j // x ∈ (presheafHom F G).sections }))
      ((fun (s : (↑(presheafHom F G).sections : Type (max (max u v) v'))) ↦
          { app := fun (X : Cᵒᵖ) ↦ ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) X).app (op (Over.mk (𝟙 (unop X)))),
            naturality := ⋯ : NatTrans F G })
        s) =
    s

Tactic:
dsimp
-- 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
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
a :
  ∀ (X : C) (Y : Over.{v, u} X),
    NatTrans.app
        ((↑(Subtype.mk (p :=
                fun (x : (j : Cᵒᵖ) → Functor.op (Over.forget (unop j)) ⋙ F ⟶ Functor.op (Over.forget (unop j)) ⋙ G) ↦
                x ∈ (presheafHom F G).sections)
                (fun (x : Cᵒᵖ) ↦
                  Functor.whiskerLeft (Functor.op (Over.forget (unop x)))
                    {
                      app := fun (X : Cᵒᵖ) ↦
                        ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) X).app
                          (op (Over.mk (𝟙 (unop X)))),
                      naturality := ⋯ })
                ⋯) :
            (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G)
          (op X))
        (op Y) =
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)).app (op Y)
⊢ Subtype.mk (p := fun (x : (j : Cᵒᵖ) → Functor.op (Over.forget (unop j)) ⋙ F ⟶ Functor.op (Over.forget (unop j)) ⋙ G) ↦
      x ∈ (presheafHom F G).sections)
      (fun (x : Cᵒᵖ) ↦
        Functor.whiskerLeft (Functor.op (Over.forget (unop x)))
          {
            app := fun (X : Cᵒᵖ) ↦
              ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) X).app
                (op (Over.mk (𝟙 (unop X)))),
            naturality := ⋯ })
      ⋯ =
    s

Tactic:
ext ⟨X⟩ ⟨Y : Over X⟩
-- 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
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X : C
Y : Over.{v, u} X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map Y.hom.op) :
        (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op X))) →
          (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Y.left)))
      ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X)) =
    (↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op Y.left)

Tactic:
have H := s.2 Y.hom.op
-- 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
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X : C
Y : Over.{v, u} X
H :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map Y.hom.op) :
        (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op X))) →
          (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Y.left)))
      ((↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op X)) =
    (↑s : (j : Cᵒᵖ) → (presheafHom F G).obj j) (op Y.left)
a :
  Eq (α := F.obj (op Y.left) ⟶ G.obj (op Y.left))
    (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op Y.left)).app
      (op (Over.mk (𝟙 Y.left))))
    (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)).app (op Y))
⊢ NatTrans.app
      ((↑(Subtype.mk (p :=
              fun (x : (j : Cᵒᵖ) → Functor.op (Over.forget (unop j)) ⋙ F ⟶ Functor.op (Over.forget (unop j)) ⋙ G) ↦
              x ∈ (presheafHom F G).sections)
              (fun (x : Cᵒᵖ) ↦
                Functor.whiskerLeft (Functor.op (Over.forget (unop x)))
                  {
                    app := fun (X : Cᵒᵖ) ↦
                      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) X).app
                        (op (Over.mk (𝟙 (unop X)))),
                    naturality := ⋯ })
              ⋯) :
          (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G)
        (op X))
      (op Y) =
    ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)).app (op Y)

Tactic:
dsimp at H ⊢
-- 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
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X : C
Y : Over.{v, u} X
H :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map Y.hom.op) :
        (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) →
          (Over.forget Y.left).op ⋙ F ⟶ (Over.forget Y.left).op ⋙ G)
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)) =
    (↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op Y.left)
a :
  Eq.{v' + 1} (α := F.obj (op Y.left) ⟶ G.obj (op Y.left))
    (NatTrans.app
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map Y.hom.op) :
            (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) →
              (Over.forget Y.left).op ⋙ F ⟶ (Over.forget Y.left).op ⋙ G)
          ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)))
        (op (Over.mk (𝟙 Y.left))) :
      (Functor.op (Over.forget Y.left) ⋙ F).obj (op (Over.mk (𝟙 Y.left))) ⟶
        (Functor.op (Over.forget Y.left) ⋙ G).obj (op (Over.mk (𝟙 Y.left))))
    (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)).app (op Y))
⊢ Eq (α := F.obj (op Y.left) ⟶ G.obj (op Y.left))
    (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op Y.left)).app
      (op (Over.mk (𝟙 Y.left))))
    (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)).app (op Y))

Tactic:
rw [← H]
-- 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
s : (↑(presheafHom F G).sections : Type (max (max u v) v'))
X : C
Y : Over.{v, u} X
H :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map Y.hom.op) :
        (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) →
          (Over.forget Y.left).op ⋙ F ⟶ (Over.forget Y.left).op ⋙ G)
      ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)) =
    (↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op Y.left)
⊢ Eq.{v' + 1} (α := F.obj (op Y.left) ⟶ G.obj (op Y.left))
    (NatTrans.app
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map Y.hom.op) :
            (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) →
              (Over.forget Y.left).op ⋙ F ⟶ (Over.forget Y.left).op ⋙ G)
          ((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)))
        (op (Over.mk (𝟙 Y.left))) :
      (Functor.op (Over.forget Y.left) ⋙ F).obj (op (Over.mk (𝟙 Y.left))) ⟶
        (Functor.op (Over.forget Y.left) ⋙ G).obj (op (Over.mk (𝟙 Y.left))))
    (((↑s : (j : Cᵒᵖ) → (Over.forget (unop j)).op ⋙ F ⟶ (Over.forget (unop j)).op ⋙ G) (op X)).app (op Y))

Tactic:
apply presheafHom_map_app_op_mk_id

Premises used: CategoryTheory.presheafHom_map_app_op_mk_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
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y : (presheafHom F G).obj (op X)
mp :
  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))))
mpr :
  (∀ (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))))) →
    x.IsAmalgamation (R := S.arrows) y
⊢ 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:
constructor
-- 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 : x.IsAmalgamation (R := S.arrows) y
Y : C
g : Y ⟶ X
hg : S.arrows g
mp :
  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)))
    (NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op X))) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Y)))
        y)
      (op (Over.mk (𝟙 Y))))
⊢ 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 [← h g 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
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y : (presheafHom F G).obj (op X)
h : x.IsAmalgamation (R := S.arrows) y
Y : C
g : Y ⟶ X
hg : S.arrows g
mp :
  Eq (α := F.obj (op Y) ⟶ G.obj (op Y))
    (y.app (op (Over.mk g)) :
      (Functor.op (Over.forget X) ⋙ F).obj (op (Over.mk g)) ⟶ (Functor.op (Over.forget X) ⋙ G).obj (op (Over.mk g)))
    (NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
          (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) → (Over.forget Y).op ⋙ F ⟶ (Over.forget Y).op ⋙ G)
        y)
      (op (Over.mk (𝟙 Y))))
⊢ 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)))
    (NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op X))) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Y)))
        y)
      (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
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible (R := S.arrows)
y : (presheafHom F G).obj (op X)
h : x.IsAmalgamation (R := S.arrows) y
Y : C
g : Y ⟶ X
hg : S.arrows g
mp mp₁ :
  Eq (α := F.obj (op Y) ⟶ G.obj (op Y))
    (y.app (op (Over.mk g)) :
      (Functor.op (Over.forget X) ⋙ F).obj (op (Over.mk g)) ⟶ (Functor.op (Over.forget X) ⋙ G).obj (op (Over.mk g)))
    (y.app (op (Over.mk g)))
⊢ Eq (α := F.obj (op Y) ⟶ G.obj (op Y))
    (y.app (op (Over.mk g)) :
      (Functor.op (Over.forget X) ⋙ F).obj (op (Over.mk g)) ⟶ (Functor.op (Over.forget X) ⋙ G).obj (op (Over.mk g)))
    (NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
          (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) → (Over.forget Y).op ⋙ F ⟶ (Over.forget Y).op ⋙ G)
        y)
      (op (Over.mk (𝟙 Y))))

Tactic:
rw [presheafHom_map_app_op_mk_id]

Premises used: CategoryTheory.presheafHom_map_app_op_mk_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
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
mpr :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
        (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) → (Over.forget Y).op ⋙ F ⟶ (Over.forget Y).op ⋙ G)
      y =
    x g hg
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
        (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op X))) →
          (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Y)))
      y =
    x g hg

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
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
mpr :
  ∀ (W : Over.{v, u} Y),
    NatTrans.app
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
            (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) → (Over.forget Y).op ⋙ F ⟶ (Over.forget Y).op ⋙ G)
          y)
        (op W) =
      (x g hg).app (op W)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
        (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) → (Over.forget Y).op ⋙ F ⟶ (Over.forget Y).op ⋙ G)
      y =
    x g hg

Tactic:
ext ⟨W : Over Y⟩

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
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
⊢ NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
          (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) → (Over.forget Y).op ⋙ F ⟶ (Over.forget Y).op ⋙ G)
        y)
      (op W) =
    (x g hg).app (op W)

Tactic:
(h W.left (W.hom ≫ g) (S.downward_closed hg _)).trans ?_

Premises used: CategoryTheory.Over, CategoryTheory.Over.mk, Quiver.Hom.unop, CategoryTheory.Sieve.downward_closed, CategoryTheory.CostructuredArrow, CategoryTheory.Over.left, CategoryTheory.CategoryStruct.comp, CategoryTheory.CostructuredArrow.mk, CategoryTheory.Over.hom, 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
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
mpr :
  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 (W.hom ≫ g) ⋯).app (op (Over.mk (𝟙 W.left)))) ((x g hg).app (op W))
⊢ NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map g.op) :
          (a : (Over.forget X).op ⋙ F ⟶ (Over.forget X).op ⋙ G) → (Over.forget Y).op ⋙ F ⟶ (Over.forget Y).op ⋙ G)
        y)
      (op W) =
    (x g hg).app (op W)

Tactic:
refine (h W.left (W.hom ≫ g) (S.downward_closed hg _)).trans ?_

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.Over.left, CategoryTheory.CategoryStruct.comp, CategoryTheory.Over.hom, 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
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
⊢ 𝟙 W.left ≫ W.hom ≫ g = W.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
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 :
  Eq (α := (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op W.left)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map (Quiver.Hom.op (𝟙 W.left))) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op W.left))) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op W.left)))
        (x (W.hom ≫ g) ⋯) :
      (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op W.left)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((presheafHom F G).map W.hom.op) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op Y))) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op W.left)))
        (x g hg) :
      (fun (X : Type (max (max u v) v')) ↦ X) ((presheafHom F G).obj (op W.left)))
⊢ 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)

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
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)
⊢ 𝟙 W.left ≫ W.hom = W.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
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)
mpr :
  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))
⊢ 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 (W.hom ≫ g) ⋯).app (op (Over.mk (𝟙 W.left)))) ((x g hg).app (op W))

Tactic:
rw [H, presheafHom_map_app _ _ W.hom (by simp)]

Premises used: CategoryTheory.presheafHom_map_app, CategoryTheory.Over.hom