-- Mathlib/CategoryTheory/Sites/SheafHom.lean
lemma presheafHom_isSheafFor  :
    Presieve.IsSheafFor (presheafHom F G) S.arrows

Proof state:
case hex
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve 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
Y : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g ≫ G.map (𝟙 Y).op = F.map (𝟙 Y).op ≫ (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ app hG x hx g = (x g hg).app (op (Over.mk (𝟙 Y)))

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

Result:
case hex
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve 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
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)))

Proof state:
case hex
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve 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
⊢ ∃ x_1, x.IsAmalgamation 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 }, ?_⟩

Result:
case hex
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve 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
⊢ x.IsAmalgamation { app := fun Y => app hG x hx (unop Y).hom, naturality := ⋯ }

Proof state:
case op.op.op
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve 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
Y₁ Y₂ : Over X
φ : Y₂ ⟶ Y₁
⊢ ∀ (j : (Sieve.pullback Y₂.hom S).arrows.categoryᵒᵖ),
    (((Over.forget (unop (op X))).op ⋙ F).map (op φ) ≫ (fun Y => app hG x hx (unop Y).hom) (op Y₂)) ≫
        (G.mapCone (Sieve.pullback Y₂.hom S).arrows.cocone.op).π.app j =
      ((fun Y => app hG x hx (unop Y).hom) (op Y₁) ≫ ((Over.forget (unop (op X))).op ⋙ G).map (op φ)) ≫
        (G.mapCone (Sieve.pullback Y₂.hom S).arrows.cocone.op).π.app j

Tactic:
rintro ⟨Z : Over Y₂.left, hZ⟩

Result:
case op.op.op.op.mk
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve 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
Y₁ Y₂ : Over X
φ : Y₂ ⟶ Y₁
Z : Over Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
⊢ (((Over.forget (unop (op X))).op ⋙ F).map (op φ) ≫ (fun Y => app hG x hx (unop Y).hom) (op Y₂)) ≫
      (G.mapCone (Sieve.pullback Y₂.hom S).arrows.cocone.op).π.app (op { obj := Z, property := hZ }) =
    ((fun Y => app hG x hx (unop Y).hom) (op Y₁) ≫ ((Over.forget (unop (op X))).op ⋙ G).map (op φ)) ≫
      (G.mapCone (Sieve.pullback Y₂.hom S).arrows.cocone.op).π.app (op { obj := Z, property := hZ })

Proof state:
case op.op.op
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve 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
Y₁ Y₂ : Over X
φ : Y₂ ⟶ Y₁
⊢ ((Over.forget (unop (op X))).op ⋙ F).map (op φ) ≫ (fun Y => app hG x hx (unop Y).hom) (op Y₂) =
    (fun Y => app hG x hx (unop Y).hom) (op Y₁) ≫ ((Over.forget (unop (op X))).op ⋙ G).map (op φ)

Tactic:
apply (hG Y₂.hom).hom_ext

Result:
case op.op.op
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve 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
Y₁ Y₂ : Over X
φ : Y₂ ⟶ Y₁
⊢ ∀ (j : (Sieve.pullback Y₂.hom S).arrows.categoryᵒᵖ),
    (((Over.forget (unop (op X))).op ⋙ F).map (op φ) ≫ (fun Y => app hG x hx (unop Y).hom) (op Y₂)) ≫
        (G.mapCone (Sieve.pullback Y₂.hom S).arrows.cocone.op).π.app j =
      ((fun Y => app hG x hx (unop Y).hom) (op Y₁) ≫ ((Over.forget (unop (op X))).op ⋙ G).map (op φ)) ≫
        (G.mapCone (Sieve.pullback Y₂.hom S).arrows.cocone.op).π.app j

Proof state:
case hunique.app.h.op.op.mk
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve 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
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows 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), y₂.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : Over X
Z : Over Y.left
hZ : (Sieve.pullback Y.hom S).arrows Z.hom
⊢ y₁.app (op Y) ≫ G.map Z.hom.op = y₂.app (op Y) ≫ G.map Z.hom.op

Tactic:
let φ : Over.mk (Z.hom ≫ Y.hom) ⟶ Y := Over.homMk Z.hom

Result:
case hunique.app.h.op.op.mk
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve 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
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows 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), y₂.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : Over X
Z : Over 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

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve 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
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ S.arrows (𝟙 Y ≫ g)

Tactic:
simpa using hg

Result:
no goals

Proof state:
case hex
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve 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
⊢ x.IsAmalgamation { app := fun Y => app hG x hx (unop Y).hom, naturality := ⋯ }

Tactic:
rw [PresheafHom.isAmalgamation_iff _ _ hx]

Result:
case hex
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve 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
⊢ ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g),
    { app := fun Y => app hG x hx (unop Y).hom, naturality := ⋯ }.app (op (Over.mk g)) =
      (x g hg).app (op (Over.mk (𝟙 Y)))