awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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
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))
⊢ 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))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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
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)
⊢ 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:
ext y
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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 (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
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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)
this :
  Eq (α := P.obj X ⟶ Functor.obj Φ.presheafFiber P) (P.map g ≫ Φ.toPresheafFiber (unop Y) y P)
    (Φ.toPresheafFiber (unop X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g.unop) :
          (a : Φ.fiber.obj (unop Y)) → Φ.fiber.obj (unop X))
        y)
      P)
⊢ 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:
simp [reassoc_of% this]
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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
g : P ⟶ Φ.skyscraperPresheaf M
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : Φ.fiber.obj X),
    Eq (α := P.obj (op Y) ⟶ M)
      (P.map f.op ≫
        (fun (X : C) (x : Φ.fiber.obj X) ↦ g.app (op X) ≫ Pi.π (fun (t : unop (Φ.fiber.op.obj (op X))) ↦ M) x) X x)
      ((fun (X : C) (x : Φ.fiber.obj X) ↦ g.app (op X) ≫ Pi.π (fun (t : unop (Φ.fiber.op.obj (op X))) ↦ M) x) Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj X)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj Y))
          x))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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 : A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
g : P ⟶ Φ.skyscraperPresheaf M
X : C
x : Φ.fiber.obj X
⊢ CategoryStruct.comp (Y := Functor.obj Φ.presheafFiber P) (Φ.toPresheafFiber X x P)
      ((Equiv.symm Φ.skyscraperPresheafHomEquiv : (a : P ⟶ Φ.skyscraperPresheaf M) → Φ.presheafFiber.obj P ⟶ M) g) =
    g.app (op X) ≫ Pi.π (fun (t : unop (Φ.fiber.op.obj (op X))) ↦ M) x

Tactic:
simp [skyscraperPresheafHomEquiv_symm_apply]

Premises used: CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_symm_apply
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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 : A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
f : Functor.obj Φ.presheafFiber P ⟶ M
X : C
x : Φ.fiber.obj X
⊢ CategoryStruct.comp (Y := Functor.obj.{v, v', u, u'} (Φ.skyscraperPresheaf M) (op X))
      (NatTrans.app ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheaf M) f)
        (op X))
      (Pi.π (fun (x : Φ.fiber.obj X) ↦ M) x) =
    Φ.toPresheafFiber X x P ≫ f

Tactic:
simp [skyscraperPresheafHomEquiv_apply_app]

Premises used: CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_apply_app
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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ᵒᵖ
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))
⊢ 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:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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ᵒᵖ
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)
⊢ 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:
ext
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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)
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)
⊢ 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:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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)
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)
⊢ 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:
rw [skyscraperPresheafHomEquiv_app_π]

Premises used: CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_app_π
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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)
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)
⊢ Φ.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:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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)
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))
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)
      (Pi.π (fun (t : Φ.fiber.obj (unop x)) ↦ M) b ≫ g)
w₂ w₃ : Φ.toPresheafFiber (unop x) b P ≫ f ≫ g = Φ.toPresheafFiber (unop x) b P ≫ f ≫ g
⊢ Φ.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 [Category.assoc, Pi.map_π, skyscraperPresheafHomEquiv_app_π_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_app_π_assoc, CategoryTheory.Limits.Pi.map_π
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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 : A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
f : P ⟶ Q
g : Functor.obj Φ.presheafFiber Q ⟶ M
⊢ Eq.{v' + 1} (α := Functor.obj Φ.presheafFiber P ⟶ M)
    ((Equiv.symm Φ.skyscraperPresheafHomEquiv : (a : P ⟶ Φ.skyscraperPresheaf M) → Φ.presheafFiber.obj P ⟶ M)
        ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheaf M)
          (Functor.map Φ.presheafFiber f ≫ g)) :
      Functor.obj Φ.presheafFiber P ⟶ M)
    ((Equiv.symm Φ.skyscraperPresheafHomEquiv : (a : P ⟶ Φ.skyscraperPresheaf M) → Φ.presheafFiber.obj P ⟶ M)
        (f ≫ (Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj Q ⟶ M) → Q ⟶ Φ.skyscraperPresheaf M) g) :
      Functor.obj Φ.presheafFiber P ⟶ M)

Tactic:
simp [Φ.skyscraperPresheafHomEquiv_naturality_left_symm]

Premises used: CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left_symm
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
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
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
P : Functor.{v, v', u, u'} Cᵒᵖ A
M : A
f : Functor.obj Φ.presheafFiber P ⟶ M
⊢ Eq (α := P ⟶ Functor.obj Φ.skyscraperPresheafFunctor M)
    ((Adjunction.homEquiv Φ.skyscraperPresheafAdjunction P M :
          (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheafFunctor.obj M)
        f :
      P ⟶ Functor.obj Φ.skyscraperPresheafFunctor M)
    ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P ⟶ M) → P ⟶ Φ.skyscraperPresheaf M) f :
      P ⟶ Φ.skyscraperPresheaf M)

Tactic:
simp [skyscraperPresheafAdjunction]

Premises used: CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafAdjunction