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
M : A
X : C
R : Sieve.{v, u} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
x : Φ.fiber.obj X
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f₁) :
        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y₁)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
      y₁ =
    x
Y₂ : C
f₂ : Y₂ ⟶ X
hf₂ : R.arrows f₂
y₂ : Φ.fiber.obj Y₂
hy₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f₂) :
        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y₂)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
      y₂ =
    x
obtain :
  ∀ (Z : C) (p₁ : Z ⟶ Y₁) (p₂ : Z ⟶ Y₂) (z : Φ.fiber.obj Z) (fac : p₁ ≫ f₁ = p₂ ≫ f₂)
    (hz₁ :
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map p₁) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Z)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj Y₁))
          z =
        y₁)
    (hz₂ :
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map p₂) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Z)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj Y₂))
          z =
        y₂),
    Eq (α := Functor.obj (Functor.obj (Functor.const R.arrows.categoryᵒᵖ) s.pt) (op (R.arrows.categoryMk f₂ hf₂)) ⟶ M)
      (s.π.app (op (R.arrows.categoryMk f₂ hf₂)) ≫
        Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op (R.arrows.categoryMk f₂ hf₂))))) ↦ M) y₂)
      (CategoryStruct.comp (Y :=
        Functor.obj (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M) (op (R.arrows.categoryMk f₁ hf₁)))
        (s.π.app (op (R.arrows.categoryMk f₁ hf₁)))
        (Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op (R.arrows.categoryMk f₁ hf₁))))) ↦ M) y₁))
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const R.arrows.categoryᵒᵖ) s.pt) (op (R.arrows.categoryMk f₂ hf₂)) ⟶ M)
    (s.π.app (op (R.arrows.categoryMk f₂ hf₂)) ≫
      Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op (R.arrows.categoryMk f₂ hf₂))))) ↦ M) y₂)
    (CategoryStruct.comp (Y :=
      Functor.obj (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M) (op (R.arrows.categoryMk f₁ hf₁)))
      (s.π.app (op (R.arrows.categoryMk f₁ hf₁)))
      (Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op (R.arrows.categoryMk f₁ hf₁))))) ↦ M) y₁))

Tactic:
obtain ⟨Z, p₁, p₂, z, fac, hz₁, hz₂⟩ :
      ∃ (Z : C) (p₁ : Z ⟶ Y₁) (p₂ : Z ⟶ Y₂) (z : Φ.fiber.obj Z), p₁ ≫ f₁ = p₂ ≫ f₂ ∧
        Φ.fiber.map p₁ z = y₁ ∧ Φ.fiber.map p₂ z = y₂ := by
    let α₁ : Φ.fiber.elementsMk _ y₁ ⟶ Φ.fiber.elementsMk _ x := ⟨f₁, hy₁⟩
    let α₂ : Φ.fiber.elementsMk _ y₂ ⟶ Φ.fiber.elementsMk _ x := ⟨f₂, hy₂⟩
    obtain ⟨z, q₁, q₂, fac⟩ := IsCofiltered.cospan α₁ α₂
    rw [Subtype.ext_iff] at fac
    refine ⟨z.1, q₁.1, q₂.1, z.2, fac, ?_, ?_⟩
    all_goals rw [CategoryOfElements.map_snd]
-- 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
M : A
X : C
R : Sieve.{v, u} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
x : Φ.fiber.obj X
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f₁) :
        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y₁)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
      y₁ =
    x
Y₂ : C
f₂ : Y₂ ⟶ X
hf₂ : R.arrows f₂
y₂ : Φ.fiber.obj Y₂
hy₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f₂) :
        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y₂)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
      y₂ =
    x
Z : C
p₁ : Z ⟶ Y₁
p₂ : Z ⟶ Y₂
z : Φ.fiber.obj Z
fac : p₁ ≫ f₁ = p₂ ≫ f₂
hz₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map p₁) :
        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Z)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj Y₁))
      z =
    y₁
hz₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map p₂) :
        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Z)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj Y₂))
      z =
    y₂
φ₁ : R.arrows.categoryMk (p₁ ≫ f₁) ⋯ ⟶ R.arrows.categoryMk f₁ hf₁ :=
  ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom) (Over.homMk p₁ ⋯)
φ₂ : R.arrows.categoryMk (p₁ ≫ f₁) ⋯ ⟶ R.arrows.categoryMk f₂ hf₂ :=
  ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom) (Over.homMk p₂ ⋯)
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const R.arrows.categoryᵒᵖ) s.pt) (op (R.arrows.categoryMk f₂ hf₂)) ⟶ M)
    (s.π.app (op (R.arrows.categoryMk f₂ hf₂)) ≫
      Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op (R.arrows.categoryMk f₂ hf₂))))) ↦ M) y₂)
    (CategoryStruct.comp (Y :=
      Functor.obj (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M) (op (R.arrows.categoryMk f₁ hf₁)))
      (s.π.app (op (R.arrows.categoryMk f₁ hf₁)))
      (Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op (R.arrows.categoryMk f₁ hf₁))))) ↦ M) y₁))

Tactic:
simpa [hz₁, hz₂, φ₁, φ₂] using
    (Cone.w s φ₂.op =≫ Pi.π _ z).trans (Cone.w s φ₁.op =≫ Pi.π _ z).symm

Premises used: Quiver.Hom.op, CategoryTheory.eq_whisker, CategoryTheory.Limits.Pi.π, CategoryTheory.Limits.Cone.w, Eq.symm, Eq.trans
-- 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
M : A
rw :
  ∀ ⦃X : C⦄,
    ∀ S ∈ (J : (a : C) → Set (Sieve a)) X,
      Nonempty
        (IsLimit (F := S.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
          (Functor.mapCone (Φ.skyscraperPresheaf M) S.arrows.cocone.op))
⊢ Presheaf.IsSheaf.{v, v', u, u'} J (Φ.skyscraperPresheaf M)

Tactic:
rw [Presheaf.isSheaf_iff_isLimit]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_isLimit
-- 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
M : A
X : C
R : Sieve.{v, u} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
j : R.arrows.categoryᵒᵖ
dsimp :
  (⋯.choose (p := fun (l : s.pt ⟶ piObj.{w, v', u'} fun (x : Φ.fiber.obj X) ↦ M) ↦
        ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left),
          l ≫
              Pi.π (fun (x : Φ.fiber.obj X) ↦ M)
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (Φ.fiber.map j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom) :
                    (a : Φ.fiber.obj j.obj.left) → Φ.fiber.obj X)
                  y) =
            s.π.app (op j) ≫
              Pi.π (fun (t : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M) y) ≫
      Pi.map'
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              (Φ.fiber.map (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom)) :
          (a : Φ.fiber.obj (unop j).obj.left) → Φ.fiber.obj X)
        fun (x : Φ.fiber.obj (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ 𝟙 M) =
    s.π.app j
⊢ ⋯.choose (p := fun (l : s.pt ⟶ piObj.{w, v', u'} fun (x : Φ.fiber.obj X) ↦ M) ↦
        ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left),
          l ≫
              Pi.π (fun (x : Φ.fiber.obj X) ↦ M)
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (Φ.fiber.map j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom) :
                    (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj j.obj.left)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
                  y) =
            s.π.app (op j) ≫ Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op j)))) ↦ M) y) ≫
      NatTrans.app (Cone.π (Functor.mapCone (Φ.skyscraperPresheaf M) R.arrows.cocone.op)) j =
    s.π.app j

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
M : A
X : C
R : Sieve.{v, u} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
j : R.arrows.categoryᵒᵖ
h :
  ∀ (y : Φ.fiber.obj (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left),
    CategoryStruct.comp (Y :=
        piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M)
        (⋯.choose (p := fun (l : s.pt ⟶ piObj.{w, v', u'} fun (x : Φ.fiber.obj X) ↦ M) ↦
            ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left),
              l ≫
                  Pi.π (fun (x : Φ.fiber.obj X) ↦ M)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun)
                          (Φ.fiber.map j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom) :
                        (a : Φ.fiber.obj j.obj.left) → Φ.fiber.obj X)
                      y) =
                s.π.app (op j) ≫
                  Pi.π (fun (t : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M) y) ≫
          Pi.map'
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Φ.fiber.map (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom)) :
              (a : Φ.fiber.obj (unop j).obj.left) → Φ.fiber.obj X)
            fun (x : Φ.fiber.obj (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ 𝟙 M)
        (Pi.π (fun (t : Φ.fiber.obj (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M) y) =
      s.π.app j ≫ Pi.π (fun (t : Φ.fiber.obj (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M) y
⊢ (⋯.choose (p := fun (l : s.pt ⟶ piObj.{w, v', u'} fun (x : Φ.fiber.obj X) ↦ M) ↦
        ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left),
          l ≫
              Pi.π (fun (x : Φ.fiber.obj X) ↦ M)
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (Φ.fiber.map j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom) :
                    (a : Φ.fiber.obj j.obj.left) → Φ.fiber.obj X)
                  y) =
            s.π.app (op j) ≫
              Pi.π (fun (t : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M) y) ≫
      Pi.map'
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              (Φ.fiber.map (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom)) :
          (a : Φ.fiber.obj (unop j).obj.left) → Φ.fiber.obj X)
        fun (x : Φ.fiber.obj (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ 𝟙 M) =
    s.π.app j

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
M : A
X : C
R : Sieve.{v, u} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
j : R.arrows.categoryᵒᵖ
y : Φ.fiber.obj (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left
⊢ CategoryStruct.comp (Y :=
      piObj.{w, v', u'} fun (t : Φ.fiber.obj (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M)
      (⋯.choose (p := fun (l : s.pt ⟶ piObj.{w, v', u'} fun (x : Φ.fiber.obj X) ↦ M) ↦
          ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left),
            l ≫
                Pi.π (fun (x : Φ.fiber.obj X) ↦ M)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun)
                        (Φ.fiber.map j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom) :
                      (a : Φ.fiber.obj j.obj.left) → Φ.fiber.obj X)
                    y) =
              s.π.app (op j) ≫
                Pi.π (fun (t : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M) y) ≫
        Pi.map'
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (Φ.fiber.map (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom)) :
            (a : Φ.fiber.obj (unop j).obj.left) → Φ.fiber.obj X)
          fun (x : Φ.fiber.obj (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ 𝟙 M)
      (Pi.π (fun (t : Φ.fiber.obj (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M) y) =
    s.π.app j ≫ Pi.π (fun (t : Φ.fiber.obj (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M) y

Tactic:
simpa using (isSheaf_skyscraperPresheaf_aux R hR s).choose_spec _ y

Premises used: Exists.choose_spec, _private.0.CategoryTheory.GrothendieckTopology.Point.isSheaf_skyscraperPresheaf_aux
-- 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
M : A
X : C
R : Sieve.{v, u} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
m :
  s.pt ⟶
    Cone.pt (F := R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
      (Functor.mapCone (Φ.skyscraperPresheaf M) R.arrows.cocone.op)
hm :
  ∀ (j : R.arrows.categoryᵒᵖ),
    m ≫ NatTrans.app (Cone.π (Functor.mapCone (Φ.skyscraperPresheaf M) R.arrows.cocone.op)) j = s.π.app j
dsimp :
  m =
    ⋯.choose (p := fun (l : s.pt ⟶ piObj.{w, v', u'} fun (x : Φ.fiber.obj X) ↦ M) ↦
      ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left),
        l ≫
            Pi.π (fun (x : Φ.fiber.obj X) ↦ M)
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (Φ.fiber.map j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom) :
                  (a : Φ.fiber.obj j.obj.left) → Φ.fiber.obj X)
                y) =
          s.π.app (op j) ≫
            Pi.π (fun (t : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M) y)
⊢ m =
    ⋯.choose (p := fun (l : s.pt ⟶ piObj.{w, v', u'} fun (x : Φ.fiber.obj X) ↦ M) ↦
      ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left),
        l ≫
            Pi.π (fun (x : Φ.fiber.obj X) ↦ M)
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (Φ.fiber.map j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom) :
                  (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj j.obj.left)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
                y) =
          s.π.app (op j) ≫ Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op j)))) ↦ M) y)

Tactic:
dsimp at hm ⊢
-- 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
M : A
X : C
R : Sieve.{v, u} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
m :
  s.pt ⟶
    Cone.pt (F := R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
      (Functor.mapCone (Φ.skyscraperPresheaf M) R.arrows.cocone.op)
hm :
  ∀ (j : R.arrows.categoryᵒᵖ),
    (m ≫
        Pi.map'
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (Φ.fiber.map (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom)) :
            (a : Φ.fiber.obj (unop j).obj.left) → Φ.fiber.obj X)
          fun (x : Φ.fiber.obj (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ 𝟙 M) =
      s.π.app j
h :
  ∀ (x : unop (Φ.fiber.op.obj R.arrows.cocone.op.pt)),
    m ≫ Pi.π (fun (t : unop (Φ.fiber.op.obj R.arrows.cocone.op.pt)) ↦ M) x =
      ⋯.choose (p := fun (l : s.pt ⟶ piObj.{w, v', u'} fun (x : Φ.fiber.obj X) ↦ M) ↦
          ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left),
            l ≫
                Pi.π (fun (x : Φ.fiber.obj X) ↦ M)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun)
                        (Φ.fiber.map j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom) :
                      (a : Φ.fiber.obj j.obj.left) → Φ.fiber.obj X)
                    y) =
              s.π.app (op j) ≫
                Pi.π (fun (t : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M) y) ≫
        Pi.π (fun (t : unop (Φ.fiber.op.obj R.arrows.cocone.op.pt)) ↦ M) x
⊢ m =
    ⋯.choose (p := fun (l : s.pt ⟶ piObj.{w, v', u'} fun (x : Φ.fiber.obj X) ↦ M) ↦
      ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left),
        l ≫
            Pi.π (fun (x : Φ.fiber.obj X) ↦ M)
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (Φ.fiber.map j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom) :
                  (a : Φ.fiber.obj j.obj.left) → Φ.fiber.obj X)
                y) =
          s.π.app (op j) ≫
            Pi.π (fun (t : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M) y)

Tactic:
ext x
-- 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
M : A
X : C
R : Sieve.{v, u} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
m :
  s.pt ⟶
    Cone.pt (F := R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
      (Functor.mapCone (Φ.skyscraperPresheaf M) R.arrows.cocone.op)
hm :
  ∀ (j : R.arrows.categoryᵒᵖ),
    (m ≫
        Pi.map'
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (Φ.fiber.map (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom)) :
            (a : Φ.fiber.obj (unop j).obj.left) → Φ.fiber.obj X)
          fun (x : Φ.fiber.obj (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ 𝟙 M) =
      s.π.app j
x : unop (Φ.fiber.op.obj R.arrows.cocone.op.pt)
h :
  ∀ (Y : C) (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y),
    Eq (α := s.pt ⟶ M)
      (m ≫
        Pi.π (fun (t : unop (Φ.fiber.op.obj R.arrows.cocone.op.pt)) ↦ M)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
              (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
            y))
      (⋯.choose (p := fun (l : s.pt ⟶ piObj.{w, v', u'} fun (x : Φ.fiber.obj X) ↦ M) ↦
          ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left),
            l ≫
                Pi.π (fun (x : Φ.fiber.obj X) ↦ M)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun)
                        (Φ.fiber.map j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom) :
                      (a : Φ.fiber.obj j.obj.left) → Φ.fiber.obj X)
                    y) =
              s.π.app (op j) ≫
                Pi.π (fun (t : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M) y) ≫
        Pi.π (fun (t : unop (Φ.fiber.op.obj R.arrows.cocone.op.pt)) ↦ M)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
              (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
            y))
⊢ m ≫ Pi.π (fun (t : unop (Φ.fiber.op.obj R.arrows.cocone.op.pt)) ↦ M) x =
    ⋯.choose (p := fun (l : s.pt ⟶ piObj.{w, v', u'} fun (x : Φ.fiber.obj X) ↦ M) ↦
        ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left),
          l ≫
              Pi.π (fun (x : Φ.fiber.obj X) ↦ M)
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (Φ.fiber.map j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom) :
                    (a : Φ.fiber.obj j.obj.left) → Φ.fiber.obj X)
                  y) =
            s.π.app (op j) ≫
              Pi.π (fun (t : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M) y) ≫
      Pi.π (fun (t : unop (Φ.fiber.op.obj R.arrows.cocone.op.pt)) ↦ M) x

Tactic:
obtain ⟨Y, g, hg, y, rfl⟩ := Φ.jointly_surjective _ hR x

Premises used: CategoryTheory.GrothendieckTopology.Point.jointly_surjective, rfl
-- 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
M : A
X : C
R : Sieve.{v, u} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
m :
  s.pt ⟶
    Cone.pt (F := R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
      (Functor.mapCone (Φ.skyscraperPresheaf M) R.arrows.cocone.op)
hm :
  ∀ (j : R.arrows.categoryᵒᵖ),
    (m ≫
        Pi.map'
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (Φ.fiber.map (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom)) :
            (a : Φ.fiber.obj (unop j).obj.left) → Φ.fiber.obj X)
          fun (x : Φ.fiber.obj (unop j).obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ 𝟙 M) =
      s.π.app j
Y : C
g : Y ⟶ X
hg : R.arrows g
y : Φ.fiber.obj Y
⊢ Eq (α := s.pt ⟶ M)
    (m ≫
      Pi.π (fun (t : unop (Φ.fiber.op.obj R.arrows.cocone.op.pt)) ↦ M)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
          y))
    (⋯.choose (p := fun (l : s.pt ⟶ piObj.{w, v', u'} fun (x : Φ.fiber.obj X) ↦ M) ↦
        ∀ (j : R.arrows.category) (y : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left),
          l ≫
              Pi.π (fun (x : Φ.fiber.obj X) ↦ M)
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (Φ.fiber.map j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).hom) :
                    (a : Φ.fiber.obj j.obj.left) → Φ.fiber.obj X)
                  y) =
            s.π.app (op j) ≫
              Pi.π (fun (t : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left) ↦ M) y) ≫
      Pi.π (fun (t : unop (Φ.fiber.op.obj R.arrows.cocone.op.pt)) ↦ M)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj X))
          y))

Tactic:
simpa [← hm (op (Presieve.categoryMk _ _ hg))] using
        ((isSheaf_skyscraperPresheaf_aux R hR s).choose_spec (Presieve.categoryMk _ _ hg) y).symm

Premises used: Exists.choose_spec, CategoryTheory.Presieve.categoryMk, _private.0.CategoryTheory.GrothendieckTopology.Point.isSheaf_skyscraperPresheaf_aux, Opposite.op, Eq.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
M : A
X : C
R : Sieve.{v, u} X
hR : R ∈ (J : (a : C) → Set (Sieve a)) X
⊢ Nonempty
    (IsLimit (F := R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
      (Functor.mapCone (Φ.skyscraperPresheaf M) R.arrows.cocone.op))

Tactic:
exact ⟨{
    lift s := (isSheaf_skyscraperPresheaf_aux R hR s).choose
    fac s j := by
      dsimp
      ext y
      simpa using (isSheaf_skyscraperPresheaf_aux R hR s).choose_spec _ y
    uniq s m hm := by
      dsimp at hm ⊢
      ext x
      obtain ⟨Y, g, hg, y, rfl⟩ := Φ.jointly_surjective _ hR x
      simpa [← hm (op (Presieve.categoryMk _ _ hg))] using
        ((isSheaf_skyscraperPresheaf_aux R hR s).choose_spec (Presieve.categoryMk _ _ hg) y).symm }⟩