awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
this :
  ∀ (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))
X : C
p₁ p₂ : ToType.{w', v', u', u_1} (FC := FC) (CC := CC) (P.obj (op X))
Y : C
g : Y ⟶ X
y : Φ.fiber.obj Y
h :
  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)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (P.map g.op) : (a : CC (P.obj (op X))) → CC (P.obj (op Y))) p₁ :
          CC (P.obj (op Y))) :
      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)))
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (P.map g.op) : (a : CC (P.obj (op X))) → CC (P.obj (op Y))) p₂ :
          CC (P.obj (op Y))) :
      CC (Q.obj (op Y)))
⊢ Eq (α := CC (Functor.obj Φ.presheafFiber P))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (Φ.toPresheafFiber X
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map g) : (a : Φ.fiber.obj Y) → Φ.fiber.obj 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 : Φ.fiber.obj Y) → Φ.fiber.obj X) y) P) :
          (a : CC (P.obj (op X))) → CC (Φ.presheafFiber.obj P))
        p₂ :
      CC (Functor.obj Φ.presheafFiber P))

Tactic:
simpa using this _ y _ _ h
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
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))
⊢ 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))

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
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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)))
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))
⊢ 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:
obtain ⟨Y, g, hg, y, rfl⟩ := Φ.jointly_surjective _ (Presheaf.equalizerSieve_mem J f _ _ h) x

Premises used: CategoryTheory.GrothendieckTopology.Point.jointly_surjective, CategoryTheory.Presheaf.equalizerSieve_mem, rfl
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
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)))
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:
simp_all [← toPresheafFiber_w_apply]

Premises used: CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_w_apply
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
inst_8 : Presheaf.IsLocallySurjective J (FA := FC) (CA := CC) f
⊢ Function.Bijective.{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))

Tactic:
⟨Φ.toPresheafFiber_map_injective f, Φ.toPresheafFiber_map_surjective f⟩

Premises used: And.intro, Function.Bijective, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_injective, CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_surjective
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
⊢ Presheaf.IsLocallyInjective (FD := FC) (CD := CC) J f

Tactic:
obtain ⟨_, _⟩ := (J.W_iff_isLocallyBijective f).1 hf

Premises used: Iff.mp, CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
⊢ Presheaf.IsLocallySurjective J (FA := FC) (CA := CC) f

Tactic:
obtain ⟨_, _⟩ := (J.W_iff_isLocallyBijective f).1 hf

Premises used: Iff.mp, CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
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)))
⊢ IsIso (X := Functor.obj Φ.presheafFiber P) (Functor.map Φ.presheafFiber f)

Tactic:
rw [← isIso_iff_of_reflects_iso _ (forget A), isIso_iff_bijective]

Premises used: CategoryTheory.isIso_iff_bijective, CategoryTheory.isIso_iff_of_reflects_iso, CategoryTheory.forget
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
⊢ 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:
Φ.toPresheafFiber_map_bijective f

Premises used: CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_bijective
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
⊢ 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:
exact Φ.toPresheafFiber_map_bijective f

Premises used: CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_bijective
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
B : Type u''
inst_2 : Category.{v'', u''} B
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v'', u''} B
FC : A → A → Type u_1
CC : A → Type w'
inst_5 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FC X Y) (CC X) (CC Y)
inst_6 : ConcreteCategory.{w', v', u', u_1} A FC (CC := CC)
inst_7 : LocallySmall.{w, v, u} C
inst_8 : HasFiniteLimits.{v', u'} A
inst_9 : AB5OfSize.{w, w, v', u'} A
⊢ PreservesFiniteLimits (C := Functor.{v, v', u, u'} Cᵒᵖ A) Φ.presheafFiber

Tactic:
comp_preservesFiniteLimits _ _

Premises used: CategoryTheory.GrothendieckTopology.Point.presheafFiber, CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
B : Type u''
inst_2 : Category.{v'', u''} B
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v'', u''} B
FC : A → A → Type u_1
CC : A → Type w'
inst_5 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FC X Y) (CC X) (CC Y)
inst_6 : ConcreteCategory.{w', v', u', u_1} A FC (CC := CC)
inst_7 : LocallySmall.{w, v, u} C
inst_8 : HasFiniteLimits.{v', u'} A
inst_9 : AB5OfSize.{w, w, v', u'} A
⊢ PreservesFiniteLimits (C := Sheaf.{v, v', u, u'} J A) Φ.sheafFiber

Tactic:
comp_preservesFiniteLimits _ _

Premises used: CategoryTheory.GrothendieckTopology.Point.sheafFiber, CategoryTheory.Limits.comp_preservesFiniteLimits
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
B : Type u''
inst_2 : Category.{v'', u''} B
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v'', u''} B
FC : A → A → Type u_1
CC : A → Type w'
inst_5 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FC X Y) (CC X) (CC Y)
inst_6 : ConcreteCategory.{w', v', u', u_1} A FC (CC := CC)
⊢ ∀ {J_1 : Type w} [inst_7 : Category.{w, w} J_1],
    PreservesColimitsOfShape (C := Functor.{v, v', u, u'} Cᵒᵖ A) J_1
      (Functor.obj (Functor.whiskeringLeft Φ.fiber.Elementsᵒᵖ Cᵒᵖ A) (CategoryOfElements.π Φ.fiber).op ⋙ colim)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
B : Type u''
inst_2 : Category.{v'', u''} B
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : HasColimitsOfSize.{w, w, v'', u''} B
FC : A → A → Type u_1
CC : A → Type w'
inst_5 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FC X Y) (CC X) (CC Y)
inst_6 : ConcreteCategory.{w', v', u', u_1} A FC (CC := CC)
inst_7 : LocallySmall.{w, v, u} C
⊢ PreservesFiniteLimits Φ.fiber

Tactic:
preservesFiniteLimits_of_natIso Φ.shrinkYonedaCompPresheafFiberIso

Premises used: CategoryTheory.GrothendieckTopology.Point.shrinkYonedaCompPresheafFiberIso, CategoryTheory.Limits.preservesFiniteLimits_of_natIso
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
U T : C
f : U ⟶ T
inst_2 : Mono f
rw : Mono (Φ.fiber.map f)
⊢ Function.Injective (α := (fun (X : Type w) ↦ X) (Φ.fiber.obj U)) (β := (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f)) :
      (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj U)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj T))

Tactic:
rw [← mono_iff_injective]

Premises used: CategoryTheory.mono_iff_injective
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
U T : C
f : U ⟶ T
inst_2 : Mono f
⊢ Mono (Φ.fiber.map f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Point.Basic
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
U T : C
f : U ⟶ T
inst_2 : Mono f
hT : IsTerminal.{v, u} T
x x_1 : Φ.fiber.obj U
have :
  ∀ (this : Unique (Φ.fiber.obj T)),
    Eq (α := (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj U)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
          x :
        (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
            (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj U)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
          x_1 :
        (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
⊢ Eq (α := (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj U)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
        x :
      (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Φ.fiber.map f) :
          (a : (fun (X : Type w) ↦ X) (Φ.fiber.obj U)) → (fun (X : Type w) ↦ X) (Φ.fiber.obj T))
        x_1 :
      (fun (X : Type w) ↦ X) (Φ.fiber.obj T))

Tactic:
have := Φ.uniqueFiberObj T hT