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
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
⊢ 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₁))
have 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₁))
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]
-- 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
⊢ Presheaf.IsSheaf.{v, v', u, u'} J (Φ.skyscraperPresheaf M)
have 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))
Tactic: rw [Presheaf.isSheaf_iff_isLimit]
-- 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)
j : R.arrows.categoryᵒᵖ
⊢ ⋯.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
have dsimp : (sorry.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: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Skyscraper (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
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ᵒᵖ
⊢ (⋯.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
have 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)
      (sorry.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: ext y
-- 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)
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
⊢ 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)
have dsimp : m =
  sorry.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: dsimp at hm ⊢
-- 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)
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
⊢ 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)
have 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 =
    sorry.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: ext 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)
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)
⊢ 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
have 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))
    (sorry.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: obtain ⟨Y, g, hg, y, rfl⟩ := Φ.jointly_surjective _ hR x
Cleared hypotheses: 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
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
X : Sheaf.{v, v', u, u'} J A
Y Y' : A
f : Functor.obj Φ.sheafFiber X ⟶ Y
g : Y ⟶ Y'
⊢ Eq (α := X ⟶ Functor.obj Φ.skyscraperSheafFunctor Y')
    (((Equiv.trans (β := Functor.obj (sheafToPresheaf J A) X ⟶ Φ.skyscraperPresheaf Y') Φ.skyscraperPresheafHomEquiv
              (Equiv.symm (Functor.FullyFaithful.homEquiv (fullyFaithfulSheafToPresheaf J A))) :
            (Functor.obj Φ.presheafFiber (Functor.obj (sheafToPresheaf J A) X) ⟶ Y') ≃
              (X ⟶ Functor.obj Φ.skyscraperSheafFunctor Y')) :
          (a : Φ.sheafFiber.obj X ⟶ Y') → X ⟶ Φ.skyscraperSheafFunctor.obj Y')
        (f ≫ g) :
      X ⟶ Functor.obj Φ.skyscraperSheafFunctor Y')
    (((Equiv.trans (β := Functor.obj (sheafToPresheaf J A) X ⟶ Φ.skyscraperPresheaf Y) Φ.skyscraperPresheafHomEquiv
                (Equiv.symm (Functor.FullyFaithful.homEquiv (fullyFaithfulSheafToPresheaf J A))) :
              (Functor.obj Φ.presheafFiber (Functor.obj (sheafToPresheaf J A) X) ⟶ Y) ≃
                (X ⟶ Functor.obj Φ.skyscraperSheafFunctor Y)) :
            (a : Φ.sheafFiber.obj X ⟶ Y) → X ⟶ Φ.skyscraperSheafFunctor.obj Y)
          f ≫
        Functor.map Φ.skyscraperSheafFunctor g :
      X ⟶ Functor.obj Φ.skyscraperSheafFunctor Y')
have h : Eq (α :=
  X.obj (P := Presheaf.IsSheaf J) ⟶
    ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J) (Functor.obj Φ.skyscraperSheafFunctor Y'))
  (InducedCategory.Hom.hom
      (((Equiv.trans (β := Functor.obj (sheafToPresheaf J A) X ⟶ Φ.skyscraperPresheaf Y') Φ.skyscraperPresheafHomEquiv
              (Equiv.symm (Functor.FullyFaithful.homEquiv (fullyFaithfulSheafToPresheaf J A))) :
            (Functor.obj Φ.presheafFiber (Functor.obj (sheafToPresheaf J A) X) ⟶ Y') ≃
              (X ⟶ Functor.obj Φ.skyscraperSheafFunctor Y')) :
          (a : Φ.sheafFiber.obj X ⟶ Y') → X ⟶ Φ.skyscraperSheafFunctor.obj Y')
        (f ≫ g)) :
    X.obj (P := Presheaf.IsSheaf J) ⟶
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J) (Functor.obj Φ.skyscraperSheafFunctor Y'))
  (InducedCategory.Hom.hom
      (((Equiv.trans (β := Functor.obj (sheafToPresheaf J A) X ⟶ Φ.skyscraperPresheaf Y) Φ.skyscraperPresheafHomEquiv
                (Equiv.symm (Functor.FullyFaithful.homEquiv (fullyFaithfulSheafToPresheaf J A))) :
              (Functor.obj Φ.presheafFiber (Functor.obj (sheafToPresheaf J A) X) ⟶ Y) ≃
                (X ⟶ Functor.obj Φ.skyscraperSheafFunctor Y)) :
            (a : Φ.sheafFiber.obj X ⟶ Y) → X ⟶ Φ.skyscraperSheafFunctor.obj Y)
          f ≫
        Functor.map Φ.skyscraperSheafFunctor g) :
    X.obj (P := Presheaf.IsSheaf J) ⟶
      ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J) (Functor.obj Φ.skyscraperSheafFunctor Y'))
Tactic: ext : 1
-- 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
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ : Functor.{v, v', u, u'} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : J.W f
⊢ IsIso (X := Functor.obj Φ.presheafFiber P₁) (Functor.map Φ.presheafFiber f)
have rw : ∀ (T : A),
  Function.Bijective (β := Functor.obj Φ.presheafFiber P₁ ⟶ T) fun (x : Functor.obj Φ.presheafFiber P₂ ⟶ T) ↦
    Functor.map Φ.presheafFiber f ≫ x
Tactic: rw [isIso_iff_coyoneda_map_bijective]
-- 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
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ : Functor.{v, v', u, u'} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : J.W f
M : A
⊢ Function.Bijective (β := Functor.obj Φ.presheafFiber P₁ ⟶ M) fun (x : Functor.obj Φ.presheafFiber P₂ ⟶ M) ↦
    Functor.map Φ.presheafFiber f ≫ x
have rw : Function.Bijective (α := Functor.obj Φ.presheafFiber P₂ ⟶ M) (β := P₁ ⟶ Φ.skyscraperPresheaf M)
  (Function.comp (β := Functor.obj Φ.presheafFiber P₁ ⟶ M)
    (⇑Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P₁ ⟶ M) → P₁ ⟶ Φ.skyscraperPresheaf M)
    fun (x : Functor.obj Φ.presheafFiber P₂ ⟶ M) ↦ Functor.map Φ.presheafFiber f ≫ x)
Tactic: rw [← Function.Bijective.of_comp_iff' Φ.skyscraperPresheafHomEquiv.bijective]
-- 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
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ : Functor.{v, v', u, u'} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : J.W f
M : A
⊢ Function.Bijective (α := Functor.obj Φ.presheafFiber P₂ ⟶ M) (β := P₁ ⟶ Φ.skyscraperPresheaf M)
    (Function.comp (β := Functor.obj Φ.presheafFiber P₁ ⟶ M)
      (⇑Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P₁ ⟶ M) → P₁ ⟶ Φ.skyscraperPresheaf M)
      fun (x : Functor.obj Φ.presheafFiber P₂ ⟶ M) ↦ Functor.map Φ.presheafFiber f ≫ x)
have h : Eq (α := (Functor.obj Φ.presheafFiber P₂ ⟶ M) → (P₁ ⟶ Φ.skyscraperPresheaf M))
  (Function.comp (β := Functor.obj Φ.presheafFiber P₁ ⟶ M)
    (⇑Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P₁ ⟶ M) → P₁ ⟶ Φ.skyscraperPresheaf M)
    fun (x : Functor.obj Φ.presheafFiber P₂ ⟶ M) ↦ Functor.map Φ.presheafFiber f ≫ x)
  ((fun (g : P₂ ⟶ Φ.skyscraperPresheaf M) ↦ f ≫ g) ∘
    (⇑Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P₂ ⟶ M) → P₂ ⟶ Φ.skyscraperPresheaf M))
Tactic: convert! (hf _ (Φ.isSheaf_skyscraperPresheaf M)).comp Φ.skyscraperPresheafHomEquiv.bijective
-- 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
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ : Functor.{v, v', u, u'} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : J.W f
M : A
⊢ Eq (α := (Functor.obj Φ.presheafFiber P₂ ⟶ M) → (P₁ ⟶ Φ.skyscraperPresheaf M))
    (Function.comp (β := Functor.obj Φ.presheafFiber P₁ ⟶ M)
      (⇑Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P₁ ⟶ M) → P₁ ⟶ Φ.skyscraperPresheaf M)
      fun (x : Functor.obj Φ.presheafFiber P₂ ⟶ M) ↦ Functor.map Φ.presheafFiber f ≫ x)
    ((fun (g : P₂ ⟶ Φ.skyscraperPresheaf M) ↦ f ≫ g) ∘
      (⇑Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P₂ ⟶ M) → P₂ ⟶ Φ.skyscraperPresheaf M))
have h : ∀ (g : Functor.obj Φ.presheafFiber P₂ ⟶ M),
  Eq (α := P₁ ⟶ Φ.skyscraperPresheaf M)
    (Function.comp (β := Functor.obj Φ.presheafFiber P₁ ⟶ M)
      (⇑Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P₁ ⟶ M) → P₁ ⟶ Φ.skyscraperPresheaf M)
      (fun (x : Functor.obj Φ.presheafFiber P₂ ⟶ M) ↦ Functor.map Φ.presheafFiber f ≫ x) g)
    (((fun (g : P₂ ⟶ Φ.skyscraperPresheaf M) ↦ f ≫ g) ∘
        (⇑Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P₂ ⟶ M) → P₂ ⟶ Φ.skyscraperPresheaf M))
      g)
Tactic: ext g : 1