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)
this :
  ∀ (x : Φ.fiber.obj X),
    ∃ (l : s.pt ⟶ M),
      ∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y)
        (hy :
          (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 =
            x),
        s.π.app (op (R.arrows.categoryMk g hg)) ≫
            Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op (R.arrows.categoryMk g hg))))) ↦ M) y =
          l
choose :
  ∀ (l : (x : Φ.fiber.obj X) → s.pt ⟶ M)
    (hl :
      ∀ (x : Φ.fiber.obj X) ⦃Y : C⦄ (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y)
        (hy :
          (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 =
            x),
        s.π.app (op (R.arrows.categoryMk g hg)) ≫
            Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op (R.arrows.categoryMk g hg))))) ↦ M) y =
          l x),
    ∃ (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
⊢ ∃ (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:
choose l hl using 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
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)
l : (x : Φ.fiber.obj X) → s.pt ⟶ M
hl :
  ∀ (x : Φ.fiber.obj X) ⦃Y : C⦄ (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y)
    (hy :
      (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 =
        x),
    s.π.app (op (R.arrows.categoryMk g hg)) ≫
        Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op (R.arrows.categoryMk g hg))))) ↦ M) y =
      l x
j : R.arrows.category
y : Φ.fiber.obj j.obj (P := fun (f : Over.{v, u} X) ↦ R.arrows f.hom).left
⊢ CategoryStruct.comp (Y := piObj.{w, v', u'} fun (x : Φ.fiber.obj X) ↦ M) (Pi.lift 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:
simpa using (hl _ j.obj.hom  j.property y rfl).symm

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, Eq.symm, CategoryTheory.Over.hom, 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)
l : (x : Φ.fiber.obj X) → s.pt ⟶ M
hl :
  ∀ (x : Φ.fiber.obj X) ⦃Y : C⦄ (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y)
    (hy :
      (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 =
        x),
    s.π.app (op (R.arrows.categoryMk g hg)) ≫
        Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op (R.arrows.categoryMk g hg))))) ↦ M) y =
      l x
⊢ ∃ (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:
exact ⟨Pi.lift l, fun j y ↦ by simpa using (hl _ j.obj.hom  j.property y rfl).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
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
suffices :
  ∀ (x : Φ.fiber.obj X),
    ∃ (l : s.pt ⟶ M),
      ∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y)
        (hy :
          (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 =
            x),
        s.π.app (op (R.arrows.categoryMk g hg)) ≫
            Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op (R.arrows.categoryMk g hg))))) ↦ M) y =
          l
⊢ ∃ (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:
suffices ∀ (x : Φ.fiber.obj X), ∃ (l : s.pt ⟶ M),
      ∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R g) (y : Φ.fiber.obj Y) (hy : Φ.fiber.map g y = x),
        s.π.app (op (Presieve.categoryMk _ _ hg)) ≫ Pi.π _ y = l by
    choose l hl using this
    exact ⟨Pi.lift l, fun j y ↦ by simpa using (hl _ j.obj.hom  j.property y rfl).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
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
x : Φ.fiber.obj X
obtain :
  ∀ (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),
    ∃ (l : s.pt ⟶ M),
      ∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y)
        (hy :
          (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 =
            x),
        s.π.app (op (R.arrows.categoryMk g hg)) ≫
            Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op (R.arrows.categoryMk g hg))))) ↦ M) y =
          l
⊢ ∃ (l : s.pt ⟶ M),
    ∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y)
      (hy :
        (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 =
          x),
      s.π.app (op (R.arrows.categoryMk g hg)) ≫
          Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op (R.arrows.categoryMk g hg))))) ↦ M) y =
        l

Tactic:
obtain ⟨Y₁, f₁, hf₁, y₁, hy₁⟩ := Φ.jointly_surjective _ hR x

Premises used: CategoryTheory.GrothendieckTopology.Point.jointly_surjective
-- 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
⊢ ∃ (l : s.pt ⟶ M),
    ∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y)
      (hy :
        (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 =
          x),
      s.π.app (op (R.arrows.categoryMk g hg)) ≫
          Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op (R.arrows.categoryMk g hg))))) ↦ M) y =
        l

Tactic:
⟨s.π.app (op (Presieve.categoryMk _ _ hf₁)) ≫ Pi.π _ y₁,
    fun Y₂ f₂ hf₂ y₂ hy₂ ↦ ?_⟩

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Presieve.categoryMk, CategoryTheory.Limits.Pi.π, Opposite.op, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.NatTrans.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
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
refine :
  ∀ (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),
    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₁))
⊢ ∃ (l : s.pt ⟶ M),
    ∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y)
      (hy :
        (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 =
          x),
      s.π.app (op (R.arrows.categoryMk g hg)) ≫
          Pi.π (fun (t : unop (Φ.fiber.op.obj (R.arrows.diagram.op.obj (op (R.arrows.categoryMk g hg))))) ↦ M) y =
        l

Tactic:
refine ⟨s.π.app (op (Presieve.categoryMk _ _ hf₁)) ≫ Pi.π _ y₁,
    fun Y₂ f₂ hf₂ y₂ hy₂ ↦ ?_⟩
-- 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
α₁ : Φ.fiber.elementsMk Y₁ y₁ ⟶ Φ.fiber.elementsMk X x :=
  Subtype.mk (p :=
    fun
      (f :
        (Φ.fiber.elementsMk Y₁ y₁).fst (β := fun (c : C) ↦ Φ.fiber.obj c) ⟶
          (Φ.fiber.elementsMk X x).fst (β := fun (c : C) ↦ Φ.fiber.obj c)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk Y₁ y₁).fst)) →
            (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk X x).fst))
        ((Φ.fiber.elementsMk Y₁ y₁).snd (β := fun (c : C) ↦ Φ.fiber.obj c)) =
      (Φ.fiber.elementsMk X x).snd (β := fun (c : C) ↦ Φ.fiber.obj c))
    f₁ hy₁
α₂ : Φ.fiber.elementsMk Y₂ y₂ ⟶ Φ.fiber.elementsMk X x :=
  Subtype.mk (p :=
    fun
      (f :
        (Φ.fiber.elementsMk Y₂ y₂).fst (β := fun (c : C) ↦ Φ.fiber.obj c) ⟶
          (Φ.fiber.elementsMk X x).fst (β := fun (c : C) ↦ Φ.fiber.obj c)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk Y₂ y₂).fst)) →
            (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk X x).fst))
        ((Φ.fiber.elementsMk Y₂ y₂).snd (β := fun (c : C) ↦ Φ.fiber.obj c)) =
      (Φ.fiber.elementsMk X x).snd (β := fun (c : C) ↦ Φ.fiber.obj c))
    f₂ hy₂
z : Φ.fiber.Elements
q₁ : z ⟶ Φ.fiber.elementsMk Y₁ y₁
q₂ : z ⟶ Φ.fiber.elementsMk Y₂ y₂
fac : q₁ ≫ α₁ = q₂ ≫ α₂
⊢ (↑(q₁ ≫ α₁) : z.fst ⟶ (Φ.fiber.elementsMk X x).fst) = (↑(q₂ ≫ α₂) : z.fst ⟶ (Φ.fiber.elementsMk X x).fst)

Tactic:
rw [Subtype.ext_iff] at fac

Premises used: Subtype.ext_iff
-- 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
α₁ : Φ.fiber.elementsMk Y₁ y₁ ⟶ Φ.fiber.elementsMk X x :=
  Subtype.mk (p :=
    fun
      (f :
        (Φ.fiber.elementsMk Y₁ y₁).fst (β := fun (c : C) ↦ Φ.fiber.obj c) ⟶
          (Φ.fiber.elementsMk X x).fst (β := fun (c : C) ↦ Φ.fiber.obj c)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk Y₁ y₁).fst)) →
            (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk X x).fst))
        ((Φ.fiber.elementsMk Y₁ y₁).snd (β := fun (c : C) ↦ Φ.fiber.obj c)) =
      (Φ.fiber.elementsMk X x).snd (β := fun (c : C) ↦ Φ.fiber.obj c))
    f₁ hy₁
α₂ : Φ.fiber.elementsMk Y₂ y₂ ⟶ Φ.fiber.elementsMk X x :=
  Subtype.mk (p :=
    fun
      (f :
        (Φ.fiber.elementsMk Y₂ y₂).fst (β := fun (c : C) ↦ Φ.fiber.obj c) ⟶
          (Φ.fiber.elementsMk X x).fst (β := fun (c : C) ↦ Φ.fiber.obj c)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk Y₂ y₂).fst)) →
            (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk X x).fst))
        ((Φ.fiber.elementsMk Y₂ y₂).snd (β := fun (c : C) ↦ Φ.fiber.obj c)) =
      (Φ.fiber.elementsMk X x).snd (β := fun (c : C) ↦ Φ.fiber.obj c))
    f₂ hy₂
z : Φ.fiber.Elements
q₁ : z ⟶ Φ.fiber.elementsMk Y₁ y₁
q₂ : z ⟶ Φ.fiber.elementsMk Y₂ y₂
fac : (↑(q₁ ≫ α₁) : z.fst ⟶ (Φ.fiber.elementsMk X x).fst) = (↑(q₂ ≫ α₂) : z.fst ⟶ (Φ.fiber.elementsMk X x).fst)
⊢ ∃ (Z : C) (p₁ : Z ⟶ Y₁) (p₂ : Z ⟶ Y₂) (z : Φ.fiber.obj Z),
    p₁ ≫ f₁ = p₂ ≫ f₂ ∧
      (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₁ ∧
        (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₂

Tactic:
⟨z.1, q₁.1, q₂.1, z.2, fac, ?_, ?_⟩

Premises used: Sigma.fst, And.intro, Exists.intro, Sigma.snd, Subtype.val
-- 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
α₁ : Φ.fiber.elementsMk Y₁ y₁ ⟶ Φ.fiber.elementsMk X x :=
  Subtype.mk (p :=
    fun
      (f :
        (Φ.fiber.elementsMk Y₁ y₁).fst (β := fun (c : C) ↦ Φ.fiber.obj c) ⟶
          (Φ.fiber.elementsMk X x).fst (β := fun (c : C) ↦ Φ.fiber.obj c)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk Y₁ y₁).fst)) →
            (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk X x).fst))
        ((Φ.fiber.elementsMk Y₁ y₁).snd (β := fun (c : C) ↦ Φ.fiber.obj c)) =
      (Φ.fiber.elementsMk X x).snd (β := fun (c : C) ↦ Φ.fiber.obj c))
    f₁ hy₁
α₂ : Φ.fiber.elementsMk Y₂ y₂ ⟶ Φ.fiber.elementsMk X x :=
  Subtype.mk (p :=
    fun
      (f :
        (Φ.fiber.elementsMk Y₂ y₂).fst (β := fun (c : C) ↦ Φ.fiber.obj c) ⟶
          (Φ.fiber.elementsMk X x).fst (β := fun (c : C) ↦ Φ.fiber.obj c)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk Y₂ y₂).fst)) →
            (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk X x).fst))
        ((Φ.fiber.elementsMk Y₂ y₂).snd (β := fun (c : C) ↦ Φ.fiber.obj c)) =
      (Φ.fiber.elementsMk X x).snd (β := fun (c : C) ↦ Φ.fiber.obj c))
    f₂ hy₂
z : Φ.fiber.Elements
q₁ : z ⟶ Φ.fiber.elementsMk Y₁ y₁
q₂ : z ⟶ Φ.fiber.elementsMk Y₂ y₂
fac : (↑(q₁ ≫ α₁) : z.fst ⟶ (Φ.fiber.elementsMk X x).fst) = (↑(q₂ ≫ α₂) : z.fst ⟶ (Φ.fiber.elementsMk X x).fst)
refine_1 refine_1₁ : (Φ.fiber.elementsMk Y₁ y₁).snd (β := fun (c : C) ↦ Φ.fiber.obj c) = y₁
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map (↑q₁ : z.fst ⟶ (Φ.fiber.elementsMk Y₁ y₁).fst)) :
        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj z.fst)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj Y₁))
      (z.snd (β := fun (c : C) ↦ Φ.fiber.obj c)) =
    y₁

Tactic:
rw [CategoryOfElements.map_snd]

Premises used: CategoryTheory.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
α₁ : Φ.fiber.elementsMk Y₁ y₁ ⟶ Φ.fiber.elementsMk X x :=
  Subtype.mk (p :=
    fun
      (f :
        (Φ.fiber.elementsMk Y₁ y₁).fst (β := fun (c : C) ↦ Φ.fiber.obj c) ⟶
          (Φ.fiber.elementsMk X x).fst (β := fun (c : C) ↦ Φ.fiber.obj c)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk Y₁ y₁).fst)) →
            (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk X x).fst))
        ((Φ.fiber.elementsMk Y₁ y₁).snd (β := fun (c : C) ↦ Φ.fiber.obj c)) =
      (Φ.fiber.elementsMk X x).snd (β := fun (c : C) ↦ Φ.fiber.obj c))
    f₁ hy₁
α₂ : Φ.fiber.elementsMk Y₂ y₂ ⟶ Φ.fiber.elementsMk X x :=
  Subtype.mk (p :=
    fun
      (f :
        (Φ.fiber.elementsMk Y₂ y₂).fst (β := fun (c : C) ↦ Φ.fiber.obj c) ⟶
          (Φ.fiber.elementsMk X x).fst (β := fun (c : C) ↦ Φ.fiber.obj c)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk Y₂ y₂).fst)) →
            (fun (X : Type w) ↦ X) (Φ.fiber.obj (Φ.fiber.elementsMk X x).fst))
        ((Φ.fiber.elementsMk Y₂ y₂).snd (β := fun (c : C) ↦ Φ.fiber.obj c)) =
      (Φ.fiber.elementsMk X x).snd (β := fun (c : C) ↦ Φ.fiber.obj c))
    f₂ hy₂
z : Φ.fiber.Elements
q₁ : z ⟶ Φ.fiber.elementsMk Y₁ y₁
q₂ : z ⟶ Φ.fiber.elementsMk Y₂ y₂
fac : (↑(q₁ ≫ α₁) : z.fst ⟶ (Φ.fiber.elementsMk X x).fst) = (↑(q₂ ≫ α₂) : z.fst ⟶ (Φ.fiber.elementsMk X x).fst)
refine_2 refine_2₁ : (Φ.fiber.elementsMk Y₂ y₂).snd (β := fun (c : C) ↦ Φ.fiber.obj c) = y₂
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map (↑q₂ : z.fst ⟶ (Φ.fiber.elementsMk Y₂ y₂).fst)) :
        (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj z.fst)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj Y₂))
      (z.snd (β := fun (c : C) ↦ Φ.fiber.obj c)) =
    y₂

Tactic:
rw [CategoryOfElements.map_snd]

Premises used: CategoryTheory.CategoryOfElements.map_snd