awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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))
⊢ Φ.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)
    (Pi.π (fun (t : Φ.fiber.obj (unop x)) ↦ M) b ≫ g)
Tactic: rw [Category.assoc, Pi.map_π, skyscraperPresheafHomEquiv_app_π_assoc]
-- 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)
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)
⊢ Φ.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 = Φ.toPresheafFiber (unop x) b P ≫ f ≫ g
Tactic: rw [Category.assoc, Pi.map_π, skyscraperPresheafHomEquiv_app_π_assoc]
-- 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
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
⊢ ∃ (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
have 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
Tactic: choose l hl using this
Cleared hypotheses: this
-- 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
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 : 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
have 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
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⟩
-- 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
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨Y₁, f₁, hf₁, y₁, hy₁⟩ := Φ.jointly_surjective _ hR x
-- 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
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
have 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₁))
Tactic: refine ⟨s.π.app (op (Presieve.categoryMk _ _ hf₁)) ≫ Pi.π _ y₁,
    fun Y₂ f₂ hf₂ y₂ hy₂ ↦ ?_⟩
-- 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
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₂ ≫ α₂
⊢ ∃ (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₂
have fac₁ : (↑(q₁ ≫ α₁) : z.fst ⟶ (Φ.fiber.elementsMk X x).fst) = (↑(q₂ ≫ α₂) : z.fst ⟶ (Φ.fiber.elementsMk X x).fst)
Tactic: rw [Subtype.ext_iff] at fac
Cleared hypotheses: fac
-- 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
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₂
have refine_1 : (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: refine ⟨z.1, q₁.1, q₂.1, z.2, fac, ?_, ?_⟩
-- 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
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)
⊢ (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₁
have refine_1 : (Φ.fiber.elementsMk Y₁ y₁).snd (β := fun (c : C) ↦ Φ.fiber.obj c) = y₁
Tactic: rw [CategoryOfElements.map_snd]
-- 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
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)
⊢ (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₂
have refine_2 : (Φ.fiber.elementsMk Y₂ y₂).snd (β := fun (c : C) ↦ Φ.fiber.obj c) = y₂
Tactic: rw [CategoryOfElements.map_snd]