awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
hγ : CategoryStruct.comp (Y := J.plusObj Q) (J.toPlus P ≫ J.plusMap η) (J.plusLift γ hR) = η ≫ γ
⊢ CategoryStruct.comp (Y := J.plusObj P) (J.toPlus P) (J.plusMap η ≫ J.plusLift γ hR) = η ≫ γ
have hγ₁ : CategoryStruct.comp (Y := J.plusObj Q) (η ≫ J.toPlus Q) (J.plusLift γ hR) = η ≫ γ
Tactic: rw [← Category.assoc, ← J.toPlus_naturality, Category.assoc, J.toPlus_plusLift]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
hγ : CategoryStruct.comp (Y := J.plusObj Q) (J.toPlus P ≫ J.plusMap η) (J.plusLift γ hR) = η ≫ γ
hγ₁ : CategoryStruct.comp (Y := J.plusObj Q) (η ≫ J.toPlus Q) (J.plusLift γ hR) = η ≫ γ
⊢ CategoryStruct.comp (Y := J.plusObj P) (J.toPlus P) (J.plusMap η ≫ J.plusLift γ hR) = η ≫ γ
have hγ₂ : η ≫ CategoryStruct.comp (Y := J.plusObj Q) (J.toPlus Q) (J.plusLift γ hR) = η ≫ γ
Tactic: rw [← Category.assoc, ← J.toPlus_naturality, Category.assoc, J.toPlus_plusLift]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Functor.{v, w', u, w} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
hγ : CategoryStruct.comp (Y := J.plusObj Q) (J.toPlus P ≫ J.plusMap η) (J.plusLift γ hR) = η ≫ γ
hγ₁ : CategoryStruct.comp (Y := J.plusObj Q) (η ≫ J.toPlus Q) (J.plusLift γ hR) = η ≫ γ
hγ₂ : η ≫ CategoryStruct.comp (Y := J.plusObj Q) (J.toPlus Q) (J.plusLift γ hR) = η ≫ γ
⊢ CategoryStruct.comp (Y := J.plusObj P) (J.toPlus P) (J.plusMap η ≫ J.plusLift γ hR) = η ≫ γ
have hγ₃ : η ≫ γ = η ≫ γ
Tactic: rw [← Category.assoc, ← J.toPlus_naturality, Category.assoc, J.toPlus_plusLift]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_4 : Preadditive.{w', w} D
F G : Functor.{v, w', u, w} Cᵒᵖ D
⊢ Eq (α := Functor.obj (J.plusFunctor D) F ⟶ Functor.obj (J.plusFunctor D) G) (Functor.map (J.plusFunctor D) 0) 0
have w : ∀ (x : Cᵒᵖ),
  Eq.{w' + 1} (α := (Functor.obj (J.plusFunctor D) F).obj x ⟶ (Functor.obj (J.plusFunctor D) G).obj x)
    (NatTrans.app (Functor.map (J.plusFunctor D) 0) x) (NatTrans.app 0 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_4 : Preadditive.{w', w} D
F G : Functor.{v, w', u, w} Cᵒᵖ D
x : Cᵒᵖ
⊢ Eq.{w' + 1} (α := (Functor.obj (J.plusFunctor D) F).obj x ⟶ (Functor.obj (J.plusFunctor D) G).obj x)
    (NatTrans.app (Functor.map (J.plusFunctor D) 0) x) (NatTrans.app 0 x)
have w : Eq.{w' + 1} (α := (J.plusObj F).obj x ⟶ (J.plusObj G).obj x) (NatTrans.app (J.plusMap 0) x) 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_4 : Preadditive.{w', w} D
F G : Functor.{v, w', u, w} Cᵒᵖ D
x : Cᵒᵖ
⊢ Eq.{w' + 1} (α := (J.plusObj F).obj x ⟶ (J.plusObj G).obj x) (NatTrans.app (J.plusMap 0) x) 0
have w : Eq.{w' + 1} (α := (J.plusObj F).obj x ⟶ (J.plusObj G).obj x) (NatTrans.app 0 x) 0
Tactic: rw [J.plusMap_zero, NatTrans.app_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Plus (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
D : Type w
inst_1 : Category.{w', w} D
inst_2 : ∀ (P : Functor.{v, w', u, w} Cᵒᵖ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Functor.{v, w', u, w} Cᵒᵖ D
inst_3 : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst_4 : Preadditive.{w', w} D
F G : Functor.{v, w', u, w} Cᵒᵖ D
x : Cᵒᵖ
w : Eq.{w' + 1} (α := (J.plusObj F).obj x ⟶ (J.plusObj G).obj x) (NatTrans.app 0 x) 0
⊢ Eq.{w' + 1} (α := (J.plusObj F).obj x ⟶ (J.plusObj G).obj x) (NatTrans.app (J.plusMap 0) x) 0
have w₁ : Eq.{w' + 1} (α := (J.plusObj F).obj x ⟶ (J.plusObj G).obj x) 0 0
Tactic: rw [J.plusMap_zero, NatTrans.app_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
inst_1 : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
x : Φ.fiber.obj X
⊢ Eq (α := (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map Φ.presheafFiber (Functor.map shrinkYoneda.{w, v, u} f)) :
          (a : (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X))) →
            (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.toPresheafFiber X x (Functor.obj shrinkYoneda.{w, v, u} X)) :
              (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).obj (op X))) →
                (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj X)))
            ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X))
                (𝟙 X) :
              Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X)) :
          (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} X))) :
      (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.toPresheafFiber X x (Functor.obj shrinkYoneda.{w, v, u} Y)) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj Y).obj (op X))) →
            (fun (X : Type w) ↦ X) (Φ.presheafFiber.obj (shrinkYoneda.{w, v, u}.obj Y)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) f :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X)) :
      (fun (X : Type w) ↦ X) (Functor.obj Φ.presheafFiber (Functor.obj shrinkYoneda.{w, v, u} Y)))
have refine : Eq (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Functor.map shrinkYoneda.{w, v, u} f) (op X)) :
        (a : (shrinkYoneda.{w, v, u}.obj X).obj (op X)) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X))
      ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op X)) (𝟙 X) :
        Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op X)) :
    Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X))
  ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) f :
    Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X))
Tactic: refine (Φ.toPresheafFiber_naturality_apply (shrinkYoneda.{w}.map f) _ x
    (shrinkYonedaObjObjEquiv.symm (𝟙 X))).trans (congr_arg _ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Basic (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 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst_3 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory.{w', v', u', u_1} A FC (CC := CC)
P : Functor.{v, v', u, u'} Cᵒᵖ A
inst_5 : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A (FC := FC) (CC := CC))
inst_6 : LocallySmall.{w, v, u} C
p : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (Functor.obj Φ.presheafFiber P)
⊢ ∃ (X : C) (x : Φ.fiber.obj X) (z : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op X))),
    (ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
          (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
        z =
      p
have obtain : ∀ (X : C) (x : Φ.fiber.obj X)
  (z :
    (((CategoryOfElements.π Φ.fiber).op ⋙ P) ⋙ forget A (FC := FC) (CC := CC)).obj
      (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x))),
  ∃ (X_1 : C) (x_1 : Φ.fiber.obj X_1) (z_1 : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op X_1))),
    Eq (α := CC (Functor.obj Φ.presheafFiber P))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X_1 x_1 P) :
            (a : CC (P.obj (op X_1))) → CC (Φ.presheafFiber.obj P))
          z_1 :
        CC (Functor.obj Φ.presheafFiber P))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (Cocone.ι
                  (Functor.mapCocone (forget A (FC := FC) (CC := CC))
                    (colimit.cocone ((CategoryOfElements.π Φ.fiber).op ⋙ P))))
                (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x))) :
            (a : (fun (X : Type w') ↦ X) ((((CategoryOfElements.π Φ.fiber).op ⋙ P) ⋙ forget A).obj (op ⟨X, x⟩))) →
              (fun (X : Type w') ↦ X)
                (((Functor.const Φ.fiber.Elementsᵒᵖ).obj
                      ((forget A).mapCocone (colimit.cocone ((CategoryOfElements.π Φ.fiber).op ⋙ P))).pt).obj
                  (op ⟨X, x⟩)))
          z :
        (fun (X : Type w') ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const Φ.fiber.Elementsᵒᵖ)
              (Cocone.pt (F := ((CategoryOfElements.π Φ.fiber).op ⋙ P) ⋙ forget A (FC := FC) (CC := CC))
                (Functor.mapCocone (forget A (FC := FC) (CC := CC))
                  (colimit.cocone ((CategoryOfElements.π Φ.fiber).op ⋙ P)))))
            (op (Sigma.mk (β := fun (c : C) ↦ Φ.fiber.obj c) X x))))
Tactic: obtain ⟨⟨X, x⟩, z, rfl⟩ := Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves (forget A)
      (colimit.isColimit ((CategoryOfElements.π Φ.fiber).op ⋙ P))) p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Basic (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 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst_3 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory.{w', v', u', u_1} A FC (CC := CC)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
inst_5 : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A (FC := FC) (CC := CC))
inst_6 : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst_7 : Presheaf.IsLocallySurjective J (FA := FC) (CA := CC) f
p : CC (Functor.obj Φ.presheafFiber Q)
⊢ ∃ (a : CC (Functor.obj Φ.presheafFiber P)),
    (ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.presheafFiber f) :
          (a : CC (Φ.presheafFiber.obj P)) → CC (Φ.presheafFiber.obj Q))
        a =
      p
have obtain : ∀ (X : C) (x : Φ.fiber.obj X) (z : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (Q.obj (op X))),
  ∃ (a : CC (Functor.obj Φ.presheafFiber P)),
    Eq (α := CC (Functor.obj Φ.presheafFiber Q))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.presheafFiber f) :
            (a : CC (Φ.presheafFiber.obj P)) → CC (Φ.presheafFiber.obj Q))
          a :
        CC (Functor.obj Φ.presheafFiber Q))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x Q) :
            (a : CC (Q.obj (op X))) → CC (Φ.presheafFiber.obj Q))
          z :
        CC (Functor.obj Φ.presheafFiber Q))
Tactic: obtain ⟨X, x, z, rfl⟩ := Φ.toPresheafFiber_jointly_surjective p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Basic (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 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst_3 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory.{w', v', u', u_1} A FC (CC := CC)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
inst_5 : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A (FC := FC) (CC := CC))
inst_6 : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst_7 : Presheaf.IsLocallySurjective J (FA := FC) (CA := CC) f
X : C
x : Φ.fiber.obj X
z : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (Q.obj (op X))
⊢ ∃ (a : CC (Functor.obj Φ.presheafFiber P)),
    Eq (α := CC (Functor.obj Φ.presheafFiber Q))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.presheafFiber f) :
            (a : CC (Φ.presheafFiber.obj P)) → CC (Φ.presheafFiber.obj Q))
          a :
        CC (Functor.obj Φ.presheafFiber Q))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x Q) :
            (a : CC (Q.obj (op X))) → CC (Φ.presheafFiber.obj Q))
          z :
        CC (Functor.obj Φ.presheafFiber Q))
have obtain : ∀ (Y : C) (g : Y ⟶ unop (op X)) (t : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op Y)))
  (ht :
    Eq (α := CC (Q.obj (op Y)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op Y)) : (a : CC (P.obj (op Y))) → CC (Q.obj (op Y))) t :
        CC (Q.obj (op Y)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Q.map g.op) :
            (a : CC (Q.obj (op (unop (op X))))) → CC (Q.obj (op Y)))
          z :
        CC (Q.obj (op Y))))
  (y : Φ.fiber.obj Y),
  ∃ (a : CC (Functor.obj Φ.presheafFiber P)),
    Eq (α := CC (Functor.obj Φ.presheafFiber Q))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.presheafFiber f) :
            (a : CC (Φ.presheafFiber.obj P)) → CC (Φ.presheafFiber.obj Q))
          a :
        CC (Functor.obj Φ.presheafFiber Q))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (Φ.toPresheafFiber X
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
                    (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj (unop (op X))))
                  y)
                Q) :
            (a : CC (Q.obj (op X))) → CC (Φ.presheafFiber.obj Q))
          z :
        CC (Functor.obj Φ.presheafFiber Q))
Tactic: obtain ⟨Y, g, ⟨t, ht⟩, y, rfl⟩ := Φ.jointly_surjective _ (Presheaf.imageSieve_mem J f z) x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Basic (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 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst_3 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory.{w', v', u', u_1} A FC (CC := CC)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
inst_5 : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A (FC := FC) (CC := CC))
inst_6 : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst_7 : Presheaf.IsLocallyInjective (FD := FC) (CD := CC) J f
⊢ Function.Injective.{w' + 1, w' + 1} (α := CC (Functor.obj Φ.presheafFiber P)) (β :=
    CC (Functor.obj Φ.presheafFiber Q))
    (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (Functor.map Φ.presheafFiber f)) :
      (a : CC (Φ.presheafFiber.obj P)) → CC (Φ.presheafFiber.obj Q))
have suffices : ∀ (X : C) (x : Φ.fiber.obj X) (p₁ p₂ : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op X)))
  (hp :
    Eq (α := CC (Q.obj (op X)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op X)) : (a : CC (P.obj (op X))) → CC (Q.obj (op X))) p₁ :
        CC (Q.obj (op X)))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op X)) : (a : CC (P.obj (op X))) → CC (Q.obj (op X))) p₂ :
        CC (Q.obj (op X)))),
  Eq (α := CC (Functor.obj Φ.presheafFiber P))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
          (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
        p₁ :
      CC (Functor.obj Φ.presheafFiber P))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
          (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
        p₂ :
      CC (Functor.obj Φ.presheafFiber P))
Tactic: suffices ∀ (X : C) (x : Φ.fiber.obj X) (p₁ p₂ : ToType (P.obj (op X)))
      (hp : f.app _ p₁ = f.app _ p₂), Φ.toPresheafFiber X x P p₁ = Φ.toPresheafFiber X x P p₂ by
    rintro q₁ q₂ h
    obtain ⟨X, x, p₁, p₂, rfl, rfl⟩ := Φ.toPresheafFiber_jointly_surjective₂ q₁ q₂
    simp only [toPresheafFiber_naturality_apply, toPresheafFiber_eq_iff'] at h
    obtain ⟨Y, g, y, rfl, h⟩ := h
    simp only [← NatTrans.naturality_apply] at h
    simpa using this _ y _ _ h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Basic (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 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst_3 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory.{w', v', u', u_1} A FC (CC := CC)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
inst_5 : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A (FC := FC) (CC := CC))
inst_6 : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst_7 : Presheaf.IsLocallyInjective (FD := FC) (CD := CC) J f
X : C
x : Φ.fiber.obj X
p₁ p₂ : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op X))
h :
  Eq (α := CC (Q.obj (op X)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op X)) : (a : CC (P.obj (op X))) → CC (Q.obj (op X))) p₁ :
      CC (Q.obj (op X)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.app (op X)) : (a : CC (P.obj (op X))) → CC (Q.obj (op X))) p₂ :
      CC (Q.obj (op X)))
⊢ Eq (α := CC (Functor.obj Φ.presheafFiber P))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
          (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
        p₁ :
      CC (Functor.obj Φ.presheafFiber P))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (Φ.toPresheafFiber X x P) :
          (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
        p₂ :
      CC (Functor.obj Φ.presheafFiber P))
have obtain : ∀ (Y : C) (g : Y ⟶ unop (op X)) (hg : (Presheaf.equalizerSieve (FD := FC) (CD := CC) p₁ p₂).arrows g)
  (y : Φ.fiber.obj Y),
  Eq (α := CC (Functor.obj Φ.presheafFiber P))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (Φ.toPresheafFiber X
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
                  (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj (unop (op X))))
                y)
              P) :
          (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
        p₁ :
      CC (Functor.obj Φ.presheafFiber P))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (Φ.toPresheafFiber X
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) :
                  (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj Y)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj (unop (op X))))
                y)
              P) :
          (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
        p₂ :
      CC (Functor.obj Φ.presheafFiber P))
Tactic: obtain ⟨Y, g, hg, y, rfl⟩ := Φ.jointly_surjective _ (Presheaf.equalizerSieve_mem J f _ _ h) x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Basic (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 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst_3 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory.{w', v', u', u_1} A FC (CC := CC)
inst_5 : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A (FC := FC) (CC := CC))
inst_6 : LocallySmall.{w, v, u} C
inst_7 : WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FC) (CA := CC)
inst_8 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FC) (CC := CC))
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
f : P ⟶ Q
hf : J.W f
⊢ IsIso (X := Functor.obj Φ.presheafFiber P) (Functor.map Φ.presheafFiber f)
have left : Presheaf.IsLocallyInjective (FD := FC) (CD := CC) J f
Tactic: obtain ⟨_, _⟩ := (J.W_iff_isLocallyBijective f).1 hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Basic (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 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst_3 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory.{w', v', u', u_1} A FC (CC := CC)
inst_5 : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A (FC := FC) (CC := CC))
inst_6 : LocallySmall.{w, v, u} C
inst_7 : WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FC) (CA := CC)
inst_8 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FC) (CC := CC))
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
f : P ⟶ Q
hf : J.W f
left : Presheaf.IsLocallyInjective (FD := FC) (CD := CC) J f
⊢ IsIso (X := Functor.obj Φ.presheafFiber P) (Functor.map Φ.presheafFiber f)
have right : Presheaf.IsLocallySurjective J (FA := FC) (CA := CC) f
Tactic: obtain ⟨_, _⟩ := (J.W_iff_isLocallyBijective f).1 hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Point.Basic (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 : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst_3 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FC X Y) (CC X) (CC Y)
inst_4 : ConcreteCategory.{w', v', u', u_1} A FC (CC := CC)
inst_5 : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A (FC := FC) (CC := CC))
inst_6 : LocallySmall.{w, v, u} C
inst_7 : WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FC) (CA := CC)
inst_8 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FC) (CC := CC))
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
f : P ⟶ Q
hf : J.W f
left : Presheaf.IsLocallyInjective (FD := FC) (CD := CC) J f
right : Presheaf.IsLocallySurjective J (FA := FC) (CA := CC) f
⊢ IsIso (X := Functor.obj Φ.presheafFiber P) (Functor.map Φ.presheafFiber f)
have rw : Function.Bijective (α :=
  (fun (X : Type w') ↦ X)
    (Functor.obj.{v', w', u', w' + 1} (forget A (FC := FC) (CC := CC)) (Functor.obj Φ.presheafFiber P)))
  (β :=
  (fun (X : Type w') ↦ X)
    (Functor.obj.{v', w', u', w' + 1} (forget A (FC := FC) (CC := CC)) (Functor.obj Φ.presheafFiber Q)))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (forget A (FC := FC) (CC := CC)) (Functor.map Φ.presheafFiber f))) :
    (a : (fun (X : Type w') ↦ X) ((forget A).obj (Φ.presheafFiber.obj P))) →
      (fun (X : Type w') ↦ X) ((forget A).obj (Φ.presheafFiber.obj Q)))
Tactic: rw [← isIso_iff_of_reflects_iso _ (forget A), isIso_iff_bijective]