awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
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'
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'))
⊢ 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')

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
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.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:
Φ.skyscraperPresheafHomEquiv_naturality_right f g

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_right
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
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.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:
exact Φ.skyscraperPresheafHomEquiv_naturality_right f g

Premises used: CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_right
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
⊢ Functor.IsLeftAdjoint (C := Sheaf.{v, v', u, u'} J A) Φ.sheafFiber

Tactic:
Φ.skyscraperSheafAdjunction.isLeftAdjoint

Premises used: CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
⊢ Functor.IsRightAdjoint (C := Sheaf.{v, v', u, u'} J A) Φ.skyscraperSheafFunctor

Tactic:
Φ.skyscraperSheafAdjunction.isRightAdjoint

Premises used: CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction, CategoryTheory.Adjunction.isRightAdjoint
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
F : Sheaf.{v, v', u, u'} J A
M : A
f : Functor.obj Φ.presheafFiber (F.obj (P := Presheaf.IsSheaf J)) ⟶ M
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf J) ⟶ Φ.skyscraperPresheaf M)
    (InducedCategory.Hom.hom
        (((Adjunction.homEquiv Φ.skyscraperSheafAdjunction F M :
              (Functor.obj Φ.sheafFiber F ⟶ M) ≃ (F ⟶ Functor.obj Φ.skyscraperSheafFunctor M)) :
            (a : Φ.presheafFiber.obj F.obj ⟶ M) → F ⟶ Φ.skyscraperSheafFunctor.obj M)
          f) :
      F.obj (P := Presheaf.IsSheaf J) ⟶
        ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J) (Functor.obj Φ.skyscraperSheafFunctor M))
    ((Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj F.obj ⟶ M) → F.obj ⟶ Φ.skyscraperPresheaf M) f :
      F.obj (P := Presheaf.IsSheaf J) ⟶ Φ.skyscraperPresheaf M)

Tactic:
simp [skyscraperSheafAdjunction, Functor.FullyFaithful.homEquiv]

Premises used: CategoryTheory.Functor.FullyFaithful.homEquiv, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
F : Sheaf.{v, v', u, u'} J A
M : A
f : F ⟶ Φ.skyscraperSheaf M
⊢ Eq.{v' + 1} (α := Functor.obj Φ.presheafFiber (F.obj (P := Presheaf.IsSheaf J)) ⟶ M)
    (((Equiv.symm (Adjunction.homEquiv Φ.skyscraperSheafAdjunction F M) :
            (F ⟶ Functor.obj Φ.skyscraperSheafFunctor M) ≃
              (Functor.obj Φ.presheafFiber (F.obj (P := Presheaf.IsSheaf J)) ⟶ M)) :
          (a : F ⟶ Φ.skyscraperSheafFunctor.obj M) → Φ.presheafFiber.obj F.obj ⟶ M)
        f :
      Functor.obj Φ.presheafFiber (F.obj (P := Presheaf.IsSheaf J)) ⟶ M)
    ((Equiv.symm Φ.skyscraperPresheafHomEquiv : (a : F.obj ⟶ Φ.skyscraperPresheaf M) → Φ.presheafFiber.obj F.obj ⟶ M)
        f.hom :
      Functor.obj Φ.presheafFiber (F.obj (P := Presheaf.IsSheaf J)) ⟶ M)

Tactic:
simp [skyscraperSheafAdjunction, Functor.FullyFaithful.homEquiv]

Premises used: CategoryTheory.Functor.FullyFaithful.homEquiv, CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ : Functor.{v, v', u, u'} Cᵒᵖ A
f : P₁ ⟶ P₂
hf : J.W f
rw :
  ∀ (T : A),
    Function.Bijective (β := Functor.obj Φ.presheafFiber P₁ ⟶ T) fun (x : Functor.obj Φ.presheafFiber P₂ ⟶ T) ↦
      Functor.map Φ.presheafFiber f ≫ x
⊢ IsIso (X := Functor.obj Φ.presheafFiber P₁) (Functor.map Φ.presheafFiber f)

Tactic:
rw [isIso_iff_coyoneda_map_bijective]

Premises used: CategoryTheory.isIso_iff_coyoneda_map_bijective
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
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
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)
⊢ Function.Bijective (β := Functor.obj Φ.presheafFiber P₁ ⟶ M) fun (x : Functor.obj Φ.presheafFiber P₂ ⟶ M) ↦
    Functor.map Φ.presheafFiber f ≫ x

Tactic:
rw [← Function.Bijective.of_comp_iff' Φ.skyscraperPresheafHomEquiv.bijective]

Premises used: Equiv.bijective, CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv, Function.Bijective.of_comp_iff'
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
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)
    ((fun (g : P₂ ⟶ Φ.skyscraperPresheaf M) ↦ f ≫ g) ∘
      (⇑Φ.skyscraperPresheafHomEquiv : (a : Φ.presheafFiber.obj P₂ ⟶ M) → P₂ ⟶ Φ.skyscraperPresheaf M))

Tactic:
(hf _ (Φ.isSheaf_skyscraperPresheaf M)).comp Φ.skyscraperPresheafHomEquiv.bijective

Premises used: Equiv.bijective, CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv, CategoryTheory.GrothendieckTopology.Point.isSheaf_skyscraperPresheaf, Function.Bijective.comp
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
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
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))
⊢ 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:
convert! (hf _ (Φ.isSheaf_skyscraperPresheaf M)).comp Φ.skyscraperPresheafHomEquiv.bijective

Premises used: Equiv.bijective, CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv, CategoryTheory.GrothendieckTopology.Point.isSheaf_skyscraperPresheaf, Function.Bijective.comp
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
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
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)
⊢ 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:
ext g : 1
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
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
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:
simp [skyscraperPresheafHomEquiv_naturality_left]

Premises used: CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
P : Functor.{v, v', u, u'} Cᵒᵖ A
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
⊢ IsIso (X := Functor.obj Φ.presheafFiber P) (Y := Functor.obj Φ.presheafFiber (CategoryTheory.sheafify J P))
    (Functor.map Φ.presheafFiber (CategoryTheory.toSheafify J P))

Tactic:
W_isInvertedBy_presheafFiber _ _ (W_toSheafify J P)

Premises used: CategoryTheory.GrothendieckTopology.Point.W_isInvertedBy_presheafFiber, CategoryTheory.GrothendieckTopology.W_toSheafify
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
⊢ ∀ {X Y : Functor.{v, v', u, u'} Cᵒᵖ A} (f : X ⟶ Y),
    Eq (α := Functor.obj Φ.presheafFiber X ⟶ Functor.obj (presheafToSheaf J A ⋙ Φ.sheafFiber) Y)
      (Functor.map Φ.presheafFiber f ≫
        Iso.hom
          ((fun (P : Functor.{v, v', u, u'} Cᵒᵖ A) ↦
              (asIso (Functor.map Φ.presheafFiber (CategoryTheory.toSheafify J P)) :
                Functor.obj Φ.presheafFiber P ≅ Functor.obj (presheafToSheaf J A ⋙ Φ.sheafFiber) P))
            Y))
      (Iso.hom
          ((fun (P : Functor.{v, v', u, u'} Cᵒᵖ A) ↦
              (asIso (Functor.map Φ.presheafFiber (CategoryTheory.toSheafify J P)) :
                Functor.obj Φ.presheafFiber P ≅ Functor.obj (presheafToSheaf J A ⋙ Φ.sheafFiber) P))
            X) ≫
        Functor.map (presheafToSheaf J A ⋙ Φ.sheafFiber) f)

Tactic:
simp [sheafFiber, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.GrothendieckTopology.Point.sheafFiber
-- Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
Φ : Point.{w, v, u} J
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasProducts.{w, v', u'} A
inst_3 : HasColimitsOfSize.{w, w, v', u'} A
⊢ PreservesFiniteColimits (C := Sheaf.{v, v', u, u'} J A) Φ.sheafFiber

Tactic:
have : PreservesColimitsOfSize.{w, w} (Φ.sheafFiber (A := A)) := inferInstance
  PreservesColimitsOfSize.preservesFiniteColimits _

Premises used: inferInstance, CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits, CategoryTheory.GrothendieckTopology.Point.sheafFiber
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) →
  ι :=
  fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
    Sum.elim (fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯)
      (fun (i : (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯) i
h₁ :
  Presieve.ofArrows P p₁ =
    Presieve.ofArrows (P ∘ a)
      fun
        (i :
          (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
      p₁ (a i)
convert_4 :
  (Presieve.ofArrows (P ∘ a)
      fun
        (i :
          (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
      p₁ (a i)) ∈
    J.coverings Y
⊢ Presieve.ofArrows P p₁ ∈ J.coverings Y

Tactic:
convert_to Presieve.ofArrows (P ∘ a) (fun i ↦ p₁ (a i)) ∈ _

Premises used: Function.comp, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) →
  ι :=
  fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
    Sum.elim (fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯)
      (fun (i : (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯) i
⊢ Presieve.ofArrows P p₁ =
    Presieve.ofArrows (P ∘ a)
      fun
        (i :
          (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
      p₁ (a i)

Tactic:
le_antisymm (fun Z g hg ↦ ?_) fun Z g ⟨i⟩ ↦ ⟨a i⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, le_antisymm, _private.0.CategoryTheory.Precoverage.mem_coverings_of_isPullback.match_1, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) →
  ι :=
  fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
    Sum.elim (fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯)
      (fun (i : (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯) i
h₁ :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : Presieve.ofArrows P p₁ g),
    Presieve.ofArrows (P ∘ a)
      (fun
          (i :
            (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕
              (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
        p₁ (a i))
      g
⊢ Presieve.ofArrows P p₁ =
    Presieve.ofArrows (P ∘ a)
      fun
        (i :
          (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
      p₁ (a i)

Tactic:
refine le_antisymm (fun Z g hg ↦ ?_) fun Z g ⟨i⟩ ↦ ⟨a i⟩

Premises used: le_antisymm