-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
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))
⊢ 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))
have 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))
Tactic: rw [uliftYonedaEquiv_naturality', uliftYonedaEquiv_comp, uliftYonedaEquiv_uliftYoneda_map]