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

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
⊢ ∀ ⦃X_1 Y : (Over (unop (op X)))ᵒᵖ⦄ (f : X_1 ⟶ Y),
    ((Over.forget (unop (op X))).op ⋙ F).map f ≫ (fun Y => app hG x hx (unop Y).hom) Y =
      (fun Y => app hG x hx (unop Y).hom) X_1 ≫ ((Over.forget (unop (op X))).op ⋙ G).map f

Tactic:
rintro ⟨Y₁ : Over X⟩ ⟨Y₂ : Over X⟩ ⟨φ : Y₂ ⟶ Y₁⟩

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₁
⊢ ((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 φ)

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)
⊢ Presieve.IsSheafFor (presheafHom F G) S.arrows

Tactic:
intro x hx

Result:
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
⊢ ∃! t, x.IsAmalgamation t

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),
    { app := fun Y => app hG x hx (unop Y).hom, naturality := ⋯ }.app (op (Over.mk g)) =
      (x g hg).app (op (Over.mk (𝟙 Y)))

Tactic:
intro Y g hg

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)))

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
φ : 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:
refine (y₁.naturality φ.op).symm.trans (Eq.trans ?_ (y₂.naturality φ.op))

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 ⋯
⊢ ((Over.forget (unop (op X))).op ⋙ F).map φ.op ≫ y₁.app (op (Over.mk (Z.hom ≫ Y.hom))) =
    ((Over.forget (unop (op X))).op ⋙ F).map φ.op ≫ y₂.app (op (Over.mk (Z.hom ≫ Y.hom)))

Proof state:
case hunique.app.h.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₂ : (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
⊢ y₁.app (op Y) = y₂.app (op Y)

Tactic:
apply (hG Y.hom).hom_ext

Result:
case hunique.app.h.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₂ : (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
⊢ ∀ (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

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.mapCone (Sieve.pullback Y.hom S).arrows.cocone.op).π.app (op { obj := Z, property := hZ }) =
    y₂.app (op Y) ≫ (G.mapCone (Sieve.pullback Y.hom S).arrows.cocone.op).π.app (op { obj := Z, property := hZ })

Tactic:
dsimp

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
⊢ y₁.app (op Y) ≫ G.map Z.hom.op = y₂.app (op Y) ≫ G.map Z.hom.op

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 = (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)

Result:
no goals