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