awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
A : Type u_1
inst_2 : Category.{u_2, u_1} A
inst_3 : HasColimitsOfSize.{w, w, u_2, u_1} A
⊢ IsIso (C := Functor.{v, u_2, u, u_1} Cᵒᵖ A ⥤ A) (Y := Point.presheafFiber (pointBot X))
    (Point.toPresheafFiberNatTrans (pointBot X) X
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (𝟙 X)))
have rw : ∀ (X_1 : Functor.{v, u_2, u, u_1} Cᵒᵖ A),
  IsIso (Y := Functor.obj (Point.presheafFiber (pointBot X)) X_1)
    (NatTrans.app
      (Point.toPresheafFiberNatTrans (pointBot X) X
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
          (𝟙 X)))
      X_1)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
S : Sieve.{v, u} X
hS :
  ∀ (Φ : ObjectProperty.FullSubcategory (C := Point.{w, v, u} (C := C) ⊥) (pointsBot C))
    (x : Φ.obj (P := pointsBot C).fiber.obj X),
    ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := pointsBot C).fiber.obj Y),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := pointsBot C).fiber.map g) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
⊢ S ∈ (⊥ : (a : C) → Set (Sieve a)) X
have obtain : ∀ (Y : C) (a : Y ⟶ X) (ha : S.arrows a)
  (b :
    Functor.obj.{v, w, u, w + 1}
      (Point.fiber
        (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
          (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) sorry)))
      Y)
  (hb :
    Eq (α :=
      (fun (X : Type w) ↦ X)
        (Functor.obj.{v, w, u, w + 1}
          (Point.fiber
            (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
              (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) sorry)))
          X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Functor.map
                (Point.fiber
                  (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
                    (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) sorry)))
                a) :
            (a : (fun (X : Type w) ↦ X) ({ obj := pointBot X, property := sorry }.obj.fiber.obj Y)) →
              (fun (X : Type w) ↦ X) ({ obj := pointBot X, property := sorry }.obj.fiber.obj X))
          b :
        (fun (X : Type w) ↦ X)
          (Functor.obj.{v, w, u, w + 1}
            (Point.fiber
              (ObjectProperty.FullSubcategory.obj (P := pointsBot C)
                (ObjectProperty.FullSubcategory.mk (P := pointsBot C) (pointBot X) sorry)))
            X))
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (𝟙 X) :
        Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))),
  S ∈ (⊥ : (a : C) → Set (Sieve a)) X
Tactic: obtain ⟨Y, a, ha, b, hb⟩ := hS ⟨_, ⟨X⟩⟩ (shrinkYonedaObjObjEquiv.symm (𝟙 X))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
S : Sieve.{v, u} X
hS :
  ∀ (Φ : ObjectProperty.FullSubcategory (C := Point.{w, v, u} (C := C) ⊥) (pointsBot C))
    (x : Φ.obj (P := pointsBot C).fiber.obj X),
    ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := pointsBot C).fiber.obj Y),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := pointsBot C).fiber.map g) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
Y : C
a : Y ⟶ X
ha : S.arrows a
b : X ⟶ Y
hb :
  Eq (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Functor.map shrinkYoneda.{w, v, u} a) (op X)) :
          (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : X ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) b :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X)) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : X ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (𝟙 X) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
⊢ Eq.{w + 1} (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (b ≫ a) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (𝟙 X) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
have rw : Eq.{w + 1} (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
  ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (b ≫ a) :
    Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Functor.map shrinkYoneda.{w, v, u} a) (op X)) :
        (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : X ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) b :
        Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X)) :
    Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
Tactic: rw [← hb, shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Presheaf (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
S : Sieve.{v, u} X
hS :
  ∀ (Φ : ObjectProperty.FullSubcategory (C := Point.{w, v, u} (C := C) ⊥) (pointsBot C))
    (x : Φ.obj (P := pointsBot C).fiber.obj X),
    ∃ (Y : C) (g : Y ⟶ X) (_ : S.arrows g) (y : Φ.obj (P := pointsBot C).fiber.obj Y),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.obj (P := pointsBot C).fiber.map g) :
            (a : (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.obj.fiber.obj X))
          y =
        x
Y : C
a : Y ⟶ X
ha : S.arrows a
b : X ⟶ Y
hb :
  Eq (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Functor.map shrinkYoneda.{w, v, u} a) (op X)) :
          (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : X ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) b :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X)) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : X ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (𝟙 X) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X))
⊢ S ∈ (⊥ : (a : C) → Set (Sieve a)) X
have this : b ≫ a = 𝟙 X
Tactic: have : b ≫ a = 𝟙 _ :=
      shrinkYonedaObjObjEquiv.symm.injective (by
        rw [← hb, shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm])
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Skyscraper (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
M N : A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
f : Functor.obj Φ.presheafFiber P ⟶ M
X Y : Cᵒᵖ
g : X ⟶ Y
⊢ Eq (α := P.obj X ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf M) Y)
    (P.map g ≫ Pi.lift fun (x : unop (Φ.fiber.op.obj Y)) ↦ Φ.toPresheafFiber (unop Y) x P ≫ f)
    (CategoryStruct.comp (Y := Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf M) X)
      (Pi.lift fun (x : unop (Φ.fiber.op.obj X)) ↦ Φ.toPresheafFiber (unop X) x P ≫ f)
      (Functor.map (Φ.skyscraperPresheaf M) g))
have dsimp : Eq (α := P.obj X ⟶ piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop Y)) ↦ M)
  (P.map g ≫ Pi.lift fun (x : Φ.fiber.obj (unop Y)) ↦ Φ.toPresheafFiber (unop Y) x P ≫ f)
  (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop X)) ↦ M)
    (Pi.lift fun (x : Φ.fiber.obj (unop X)) ↦ Φ.toPresheafFiber (unop X) x P ≫ f)
    (Pi.map'
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g.unop)) :
        (a : Φ.fiber.obj (unop Y)) → Φ.fiber.obj (unop X))
      fun (x : Φ.fiber.obj (unop Y)) ↦ 𝟙 M))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Skyscraper (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
M N : A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
f : Functor.obj Φ.presheafFiber P ⟶ M
X Y : Cᵒᵖ
g : X ⟶ Y
⊢ Eq (α := P.obj X ⟶ piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop Y)) ↦ M)
    (P.map g ≫ Pi.lift fun (x : Φ.fiber.obj (unop Y)) ↦ Φ.toPresheafFiber (unop Y) x P ≫ f)
    (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop X)) ↦ M)
      (Pi.lift fun (x : Φ.fiber.obj (unop X)) ↦ Φ.toPresheafFiber (unop X) x P ≫ f)
      (Pi.map'
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g.unop)) :
          (a : Φ.fiber.obj (unop Y)) → Φ.fiber.obj (unop X))
        fun (x : Φ.fiber.obj (unop Y)) ↦ 𝟙 M))
have h : ∀ (y : Φ.fiber.obj (unop Y)),
  Eq (α := P.obj X ⟶ M)
    (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop Y)) ↦ M)
        (P.map g ≫ Pi.lift fun (x : Φ.fiber.obj (unop Y)) ↦ Φ.toPresheafFiber (unop Y) x P ≫ f)
        (Pi.π (fun (t : Φ.fiber.obj (unop Y)) ↦ M) y) :
      P.obj X ⟶ M)
    (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop Y)) ↦ M)
        (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop X)) ↦ M)
          (Pi.lift fun (x : Φ.fiber.obj (unop X)) ↦ Φ.toPresheafFiber (unop X) x P ≫ f)
          (Pi.map'
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g.unop)) :
              (a : Φ.fiber.obj (unop Y)) → Φ.fiber.obj (unop X))
            fun (x : Φ.fiber.obj (unop Y)) ↦ 𝟙 M))
        (Pi.π (fun (t : Φ.fiber.obj (unop Y)) ↦ M) y) :
      P.obj X ⟶ M)
Tactic: ext y
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Skyscraper (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
M N : A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
f : Functor.obj Φ.presheafFiber P ⟶ M
X Y : Cᵒᵖ
g : X ⟶ Y
y : Φ.fiber.obj (unop Y)
⊢ Eq (α := P.obj X ⟶ M)
    (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop Y)) ↦ M)
        (P.map g ≫ Pi.lift fun (x : Φ.fiber.obj (unop Y)) ↦ Φ.toPresheafFiber (unop Y) x P ≫ f)
        (Pi.π (fun (t : Φ.fiber.obj (unop Y)) ↦ M) y) :
      P.obj X ⟶ M)
    (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop Y)) ↦ M)
        (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop X)) ↦ M)
          (Pi.lift fun (x : Φ.fiber.obj (unop X)) ↦ Φ.toPresheafFiber (unop X) x P ≫ f)
          (Pi.map'
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g.unop)) :
              (a : Φ.fiber.obj (unop Y)) → Φ.fiber.obj (unop X))
            fun (x : Φ.fiber.obj (unop Y)) ↦ 𝟙 M))
        (Pi.π (fun (t : Φ.fiber.obj (unop Y)) ↦ M) y) :
      P.obj X ⟶ M)
have this : Eq (α := P.obj (op (unop X)) ⟶ Functor.obj Φ.presheafFiber P) (P.map g.unop.op ≫ Φ.toPresheafFiber (unop Y) y P)
  (Φ.toPresheafFiber (unop X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g.unop) :
        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj (unop Y))) → (fun (X : Type w) ↦ X) (Φ.fiber.obj (unop X)))
      y)
    P)
Tactic: have := Φ.toPresheafFiber_w g.unop y P
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Skyscraper (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
P : Functor.{v, v', u, u'} Cᵒᵖ A
M N : A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
f : Functor.obj Φ.presheafFiber P ⟶ M
g : M ⟶ N
⊢ Eq (α := P ⟶ Φ.skyscraperPresheaf N)
    ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ N) → P ⟶ Φ.skyscraperPresheaf N) (f ≫ g) :
      P ⟶ Φ.skyscraperPresheaf N)
    ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheaf M) f ≫
        Functor.map Φ.skyscraperPresheafFunctor g :
      P ⟶ Functor.obj Φ.skyscraperPresheafFunctor N)
have w : ∀ (x : Cᵒᵖ),
  Eq.{v' + 1} (α := P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf N) x)
    (NatTrans.app
      ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ N) → P ⟶ Φ.skyscraperPresheaf N) (f ≫ g)) x)
    (NatTrans.app
      ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheaf M) f ≫
        Functor.map Φ.skyscraperPresheafFunctor g)
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Skyscraper (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
P : Functor.{v, v', u, u'} Cᵒᵖ A
M N : A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
f : Functor.obj Φ.presheafFiber P ⟶ M
g : M ⟶ N
x : Cᵒᵖ
⊢ Eq.{v' + 1} (α := P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf N) x)
    (NatTrans.app
      ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ N) → P ⟶ Φ.skyscraperPresheaf N) (f ≫ g)) x)
    (NatTrans.app
      ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheaf M) f ≫
        Functor.map Φ.skyscraperPresheafFunctor g)
      x)
have w : Eq.{v' + 1} (α := P.obj x ⟶ piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ N)
  (NatTrans.app ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ N) → P ⟶ Φ.skyscraperPresheaf N) (f ≫ g))
      x :
    P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf N) x)
  (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ M)
    (NatTrans.app ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheaf M) f) x :
      P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf M) x)
    (Limits.Pi.map fun (x : Φ.fiber.obj (unop x)) ↦ g))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Skyscraper (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
P : Functor.{v, v', u, u'} Cᵒᵖ A
M N : A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
f : Functor.obj Φ.presheafFiber P ⟶ M
g : M ⟶ N
x : Cᵒᵖ
⊢ Eq.{v' + 1} (α := P.obj x ⟶ piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ N)
    (NatTrans.app
        ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ N) → P ⟶ Φ.skyscraperPresheaf N) (f ≫ g)) x :
      P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf N) x)
    (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ M)
      (NatTrans.app ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheaf M) f)
          x :
        P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf M) x)
      (Limits.Pi.map fun (x : Φ.fiber.obj (unop x)) ↦ g))
have w : ∀ (b : unop (Φ.fiber.op.obj x)),
  Eq.{v' + 1} (α := P.obj x ⟶ N)
    (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : unop (Φ.fiber.op.obj x)) ↦ N)
        (NatTrans.app
            ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ N) → P ⟶ Φ.skyscraperPresheaf N) (f ≫ g)) x :
          P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf N) x)
        (Pi.π (fun (t : unop (Φ.fiber.op.obj x)) ↦ N) b) :
      P.obj x ⟶ N)
    (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : unop (Φ.fiber.op.obj x)) ↦ N)
        (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ M)
          (NatTrans.app
              ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheaf M) f) x :
            P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf M) x)
          (Limits.Pi.map fun (x : Φ.fiber.obj (unop x)) ↦ g))
        (Pi.π (fun (t : unop (Φ.fiber.op.obj x)) ↦ N) b) :
      P.obj x ⟶ N)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Skyscraper (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
P : Functor.{v, v', u, u'} Cᵒᵖ A
M N : A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
f : Functor.obj Φ.presheafFiber P ⟶ M
g : M ⟶ N
x : Cᵒᵖ
b : unop (Φ.fiber.op.obj x)
⊢ Eq.{v' + 1} (α := P.obj x ⟶ N)
    (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : unop (Φ.fiber.op.obj x)) ↦ N)
        (NatTrans.app
            ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ N) → P ⟶ Φ.skyscraperPresheaf N) (f ≫ g)) x :
          P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf N) x)
        (Pi.π (fun (t : unop (Φ.fiber.op.obj x)) ↦ N) b) :
      P.obj x ⟶ N)
    (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : unop (Φ.fiber.op.obj x)) ↦ N)
        (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ M)
          (NatTrans.app
              ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheaf M) f) x :
            P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf M) x)
          (Limits.Pi.map fun (x : Φ.fiber.obj (unop x)) ↦ g))
        (Pi.π (fun (t : unop (Φ.fiber.op.obj x)) ↦ N) b) :
      P.obj x ⟶ N)
have w : Eq.{v' + 1} (α := P.obj x ⟶ N)
  (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ N)
      (NatTrans.app
          ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ N) → P ⟶ Φ.skyscraperPresheaf N) (f ≫ g)) x :
        P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf N) x)
      (Pi.π (fun (t : Φ.fiber.obj (unop x)) ↦ N) b) :
    P.obj x ⟶ N)
  (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ N)
      (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ M)
        (NatTrans.app ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheaf M) f)
            x :
          P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf M) x)
        (Limits.Pi.map fun (x : Φ.fiber.obj (unop x)) ↦ g))
      (Pi.π (fun (t : Φ.fiber.obj (unop x)) ↦ N) b) :
    P.obj x ⟶ N)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Skyscraper (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
P : Functor.{v, v', u, u'} Cᵒᵖ A
M N : A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
f : Functor.obj Φ.presheafFiber P ⟶ M
g : M ⟶ N
x : Cᵒᵖ
b : unop (Φ.fiber.op.obj x)
⊢ Eq.{v' + 1} (α := P.obj x ⟶ N)
    (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ N)
        (NatTrans.app
            ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ N) → P ⟶ Φ.skyscraperPresheaf N) (f ≫ g)) x :
          P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf N) x)
        (Pi.π (fun (t : Φ.fiber.obj (unop x)) ↦ N) b) :
      P.obj x ⟶ N)
    (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ N)
        (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ M)
          (NatTrans.app
              ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheaf M) f) x :
            P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf M) x)
          (Limits.Pi.map fun (x : Φ.fiber.obj (unop x)) ↦ g))
        (Pi.π (fun (t : Φ.fiber.obj (unop x)) ↦ N) b) :
      P.obj x ⟶ N)
have w : Φ.toPresheafFiber (unop x) b P ≫ f ≫ g =
  CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ N)
    (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ M)
      (NatTrans.app ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheaf M) f)
          x :
        P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf M) x)
      (Limits.Pi.map fun (x : Φ.fiber.obj (unop x)) ↦ g))
    (Pi.π (fun (t : Φ.fiber.obj (unop x)) ↦ N) b)
Tactic: rw [skyscraperPresheafHomEquiv_app_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Skyscraper (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
P : Functor.{v, v', u, u'} Cᵒᵖ A
M N : A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
f : Functor.obj Φ.presheafFiber P ⟶ M
g : M ⟶ N
x : Cᵒᵖ
b : unop (Φ.fiber.op.obj x)
⊢ Φ.toPresheafFiber (unop x) b P ≫ f ≫ g =
    CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ N)
      (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ M)
        (NatTrans.app ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheaf M) f)
            x :
          P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf M) x)
        (Limits.Pi.map fun (x : Φ.fiber.obj (unop x)) ↦ g))
      (Pi.π (fun (t : Φ.fiber.obj (unop x)) ↦ N) b)
have w : Φ.toPresheafFiber (unop x) b P ≫ f ≫ g =
  CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ M)
    (NatTrans.app ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheaf M) f) x :
      P.obj x ⟶ Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf M) x)
    (CategoryStruct.comp (Y := piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop x)) ↦ N)
      (Limits.Pi.map fun (x : Φ.fiber.obj (unop x)) ↦ g) (Pi.π (fun (t : Φ.fiber.obj (unop x)) ↦ N) b))
Tactic: rw [Category.assoc, Pi.map_π, skyscraperPresheafHomEquiv_app_π_assoc]