-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : Cᵒᵖ
F : Sheaf J (Type v)
f : J.yoneda.obj (unop X) ⟶ F
g : X ⟶ Y
rw :
  Eq.{v + 1} (α := (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
    ((J.yonedaEquiv : (a : J.yoneda.obj (unop Y) ⟶ F) → F.obj.obj (op (unop Y))) (J.yoneda.map g.unop ≫ f) :
      F.obj (P := Presheaf.IsSheaf J).obj (op (unop Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj Y)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
        g.unop :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
rw₁ :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op (unop Y))) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj (op (unop Y)))) →
            (fun (X : Type v) ↦ X) (F.obj.obj (op (unop Y))))
        ((J.yonedaEquiv :
              (a : J.yoneda.obj (unop Y) ⟶ J.yoneda.obj (unop X)) → (J.yoneda.obj (unop X)).obj.obj (op (unop Y)))
            (J.yoneda.map g.unop) :
          (J.yoneda.obj (unop X)).obj (P := Presheaf.IsSheaf J).obj (op (unop Y))) :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op (unop Y))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj Y)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
        g.unop :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
rw₂ rw₃ :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op (unop Y))) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj (op (unop Y)))) →
            (fun (X : Type v) ↦ X) (F.obj.obj (op (unop Y))))
        g.unop :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op (unop Y))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj Y)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
        g.unop :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
⊢ Eq (α := (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g) :
          (a : (fun (X : Type v) ↦ X) (F.obj.obj X)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
        ((J.yonedaEquiv : (a : J.yoneda.obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) f :
          F.obj (P := Presheaf.IsSheaf J).obj (op (unop X))) :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj Y)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
        g.unop :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))

Tactic:
rw [yonedaEquiv_naturality', yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Premises used: CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality', CategoryTheory.GrothendieckTopology.yonedaEquiv_comp, CategoryTheory.GrothendieckTopology.yonedaEquiv_yoneda_map