-- 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 (max v v'))
f : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
g : X ⟶ Y
rw :
  Eq (α := (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
    ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F) → F.obj.obj (op (unop Y)))
        ((uliftYoneda.{v', v, u} J).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 (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj (unop X)).obj.obj Y)) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
        { down := g.unop } :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
rw₁ :
  Eq (α := (fun (X : Type (max v 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 (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj (unop X)).obj.obj (op (unop Y)))) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op (unop Y))))
        ((J.uliftYonedaEquiv :
            (a : (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ (uliftYoneda.{v', v, u} J).obj (unop X)) →
              ((uliftYoneda.{v', v, u} J).obj (unop X)).obj.obj (op (unop Y)))
          ((uliftYoneda.{v', v, u} J).map g.unop)) :
      (fun (X : Type (max v 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 (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj (unop X)).obj.obj Y)) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
        { down := g.unop } :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
rw₂ rw₃ :
  Eq (α := (fun (X : Type (max v 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 (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj (unop X)).obj.obj (op (unop Y)))) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op (unop Y))))
        { down := g.unop } :
      (fun (X : Type (max v 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 (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj (unop X)).obj.obj Y)) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
        { down := g.unop } :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
⊢ Eq (α := (fun (X : Type (max v 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 (max v v')) ↦ X) (F.obj.obj X)) → (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
        ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) f) :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
          (a : (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj (unop X)).obj.obj Y)) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
        { down := g.unop } :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))

Tactic:
rw [uliftYonedaEquiv_naturality', uliftYonedaEquiv_comp, uliftYonedaEquiv_uliftYoneda_map]

Premises used: CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality', CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_uliftYoneda_map, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp