awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt) f
hgf₁ : S.arrows (g₁ ≫ f₁)
⊢ S.arrows (g₂ ≫ f₂)

Tactic:
exact Sieve.downward_closed S hf₂ g₂

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt) f
hgf₁ : S.arrows (g₁ ≫ f₁)
⊢ S.arrows (g₂ ≫ f₂)

Tactic:
have hgf₂ : S.arrows (g₂ ≫ f₂) := by exact Sieve.downward_closed S hf₂ g₂
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt) f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z) ⋯
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁ ⋯
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂ ⋯
⊢ Eq (α :=
    S.arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ⟶
      Functor.obj (C := S.arrows.category) (Functor.obj (Functor.const S.arrows.category) s.pt)
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₂ ≫ f₂)) hgf₂))
    (S.arrows.diagram.map (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F) ≫
      s.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₂ ≫ f₂)) hgf₂))
    (s.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ≫
      Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt)
        (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F))

Tactic:
have hF := @Hs ⟨Over.mk (g₁ ≫ f₁), hgf₁⟩ ⟨Over.mk (g₂ ≫ f₂), hgf₂⟩ (ObjectProperty.homMk F)
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y =
      s.ι.app X_1 ≫ Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt) f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z) ⋯
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁ ⋯
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂ ⋯
hF :
  Eq (α :=
    S.arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ⟶
      Functor.obj (C := S.arrows.category) (Functor.obj (Functor.const S.arrows.category) s.pt)
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₂ ≫ f₂)) hgf₂))
    (S.arrows.diagram.map (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F) ≫
      s.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₂ ≫ f₂)) hgf₂))
    (s.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ≫
      Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt)
        (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F))
⊢ Eq (α :=
    S.arrows.diagram.obj
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ⟶
      Functor.obj (C := S.arrows.category) (Functor.obj (Functor.const S.arrows.category) s.pt)
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₁) hf₁))
    (S.arrows.diagram.map (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F₁) ≫
      s.ι.app (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk f₁) hf₁))
    (s.ι.app
        (ObjectProperty.FullSubcategory.mk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) (Over.mk (g₁ ≫ f₁)) hgf₁) ≫
      Functor.map (Functor.obj (Functor.const S.arrows.category) s.pt)
        (ObjectProperty.homMk (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom) F₁))

Tactic:
have hF₁ := @Hs ⟨Over.mk (g₁ ≫ f₁), hgf₁⟩ ⟨Over.mk f₁, hf₁⟩ (ObjectProperty.homMk F₁)
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
mp : (∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows) → Nonempty (IsColimit S.arrows.cocone)
mpr : Nonempty (IsColimit S.arrows.cocone) → ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
⊢ (∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows) ↔ Nonempty (IsColimit S.arrows.cocone)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H : ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
⊢ Nonempty (IsColimit S.arrows.cocone)

Tactic:
Nonempty.intro ?_

Premises used: Nonempty.intro
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H : ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
mp : IsColimit S.arrows.cocone
⊢ Nonempty (IsColimit S.arrows.cocone)

Tactic:
refine Nonempty.intro ?_

Premises used: Nonempty.intro
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H : ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
s : Cocone S.arrows.diagram
f : S.arrows.category
⊢ ∃! t : Functor.obj (Functor.obj yoneda s.pt) (op X),
    (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t

Tactic:
replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
          (yonedaFamily_fromCocone_compatible S s)
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H_1 : ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
s : Cocone S.arrows.diagram
f : S.arrows.category
H :
  ∃! t : Functor.obj (Functor.obj yoneda s.pt) (op X),
    (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (Functor.obj yoneda s.pt) f.obj (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom).hom.op) :
        (a : (fun (X : Type v) ↦ X) ((yoneda.obj s.pt).obj (op X))) →
          (fun (X : Type v) ↦ X) ((yoneda.obj s.pt).obj (op f.obj.left)))
      (Exists.choose (p := fun (x : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
        (fun (t : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
              (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t)
            x ∧
          ∀ (y : Functor.obj (Functor.obj yoneda s.pt) (op X)),
            (fun (t : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
                  (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t)
                y →
              y = x)
        H) =
    S.arrows.yonedaFamilyOfElements_fromCocone s f.obj (P := fun (f : Over.{v, u} X) ↦ S.arrows f.hom).hom ⋯

Tactic:
have ht := H.choose_spec.1 f.obj.hom f.property
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H : ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
⊢ ∃! t : Functor.obj (Functor.obj yoneda s.pt) (op X),
    (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t

Tactic:
replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
          (yonedaFamily_fromCocone_compatible S s)
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H_1 : ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
H :
  ∃! t : Functor.obj (Functor.obj yoneda s.pt) (op X),
    (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t
apply : (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) Fs
⊢ Fs =
    Exists.choose (p := fun (x : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
      (fun (t : Functor.obj (Functor.obj yoneda s.pt) (op X)) ↦
            (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t)
          x ∧
        ∀ (y : Functor.obj (Functor.obj yoneda s.pt) (op X)),
          (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) y → y = x)
      ⋯

Tactic:
apply H.choose_spec.2 Fs

Premises used: Exists.choose_spec, And.right
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H_1 : ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
H :
  ∃! t : Functor.obj (Functor.obj yoneda s.pt) (op X),
    (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t
⊢ (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) Fs

Tactic:
fun _ f hf => HFs ⟨Over.mk f, hf⟩

Premises used: CategoryTheory.Presieve.yonedaFamilyOfElements_fromCocone, CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Over.mk, Quiver.Hom.unop, CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H_1 : ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
s : Cocone S.arrows.diagram
Fs : S.arrows.cocone.pt ⟶ s.pt
HFs : ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Fs = s.ι.app j
H :
  ∃! t : Functor.obj (Functor.obj yoneda s.pt) (op X),
    (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) t
⊢ (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation (R := S.arrows) Fs

Tactic:
exact fun _ f hf => HFs ⟨Over.mk f, hf⟩

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Over.mk
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H : ∀ (W : C), IsSheafFor (Functor.obj yoneda W) S.arrows
⊢ IsColimit S.arrows.cocone

Tactic:
exact
    { desc := fun s => H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
        (yonedaFamily_fromCocone_compatible S s) |>.choose
      fac := by
        intro s f
        replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
          (yonedaFamily_fromCocone_compatible S s)
        have ht := H.choose_spec.1 f.obj.hom f.property
        cat_disch
      uniq := by
        intro s Fs HFs
        replace H := H s.pt (yonedaFamilyOfElements_fromCocone S.arrows s)
          (yonedaFamily_fromCocone_compatible S s)
        apply H.choose_spec.2 Fs
        exact fun _ f hf => HFs ⟨Over.mk f, hf⟩ }
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
H : Nonempty (IsColimit S.arrows.cocone)
W : C
x : FamilyOfElements (Functor.obj yoneda W) S.arrows
hx : x.Compatible (R := S.arrows)
mpr :
  ∀ (H : IsColimit S.arrows.cocone),
    ∃! t : Functor.obj (Functor.obj yoneda W) (op X), x.IsAmalgamation (R := S.arrows) t
⊢ ∃! t : Functor.obj (Functor.obj yoneda W) (op X), x.IsAmalgamation (R := S.arrows) t

Tactic:
replace H := Classical.choice H
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
W : C
x : FamilyOfElements (Functor.obj yoneda W) S.arrows
hx : x.Compatible (R := S.arrows)
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
h :
  (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) (H.desc s) ∧
    ∀ (y : Functor.obj (Functor.obj yoneda W) (op X)),
      (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) y → y = H.desc s
⊢ ∃! t : Functor.obj (Functor.obj yoneda W) (op X), x.IsAmalgamation (R := S.arrows) t

Tactic:
use H.desc s

Premises used: CategoryTheory.Limits.IsColimit.desc
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
W : C
x : FamilyOfElements (Functor.obj yoneda W) S.arrows
hx : x.Compatible (R := S.arrows)
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
h : (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) (H.desc s)
h₁ :
  ∀ (y : Functor.obj (Functor.obj yoneda W) (op X)),
    (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) y → y = H.desc s
⊢ (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) (H.desc s) ∧
    ∀ (y : Functor.obj (Functor.obj yoneda W) (op X)),
      (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) y → y = H.desc s

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
W : C
x : FamilyOfElements (Functor.obj yoneda W) S.arrows
hx : x.Compatible (R := S.arrows)
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
⊢ (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) (H.desc s)

Tactic:
fun _ f hf => (H.fac s) ⟨Over.mk f, hf⟩

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Over.mk, Quiver.Hom.unop, CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
W : C
x : FamilyOfElements (Functor.obj yoneda W) S.arrows
hx : x.Compatible (R := S.arrows)
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
⊢ (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) (H.desc s)

Tactic:
exact fun _ f hf => (H.fac s) ⟨Over.mk f, hf⟩

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.ObjectProperty.FullSubcategory.mk, CategoryTheory.Over.mk
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
W : C
x : FamilyOfElements (Functor.obj yoneda W) S.arrows
hx : x.Compatible (R := S.arrows)
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
⊢ ∀ (y : Functor.obj (Functor.obj yoneda W) (op X)),
    (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) y → y = H.desc s

Tactic:
fun g hg => H.uniq s g (fun ⟨⟨f, _, hom⟩, hf⟩ => hg hom hf)

Premises used: CategoryTheory.Presieve.cocone, CategoryTheory.Sieve.arrows, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Limits.Cocone.ι, CategoryTheory.CategoryStruct.comp, Eq, CategoryTheory.NatTrans.app, _private.0.CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit.match_2
-- Module: Mathlib.CategoryTheory.Sites.SheafOfTypes
Goal:
C : Type u
inst : Category.{v, u} C
X : C
S : Sieve.{v, u} X
W : C
x : FamilyOfElements (Functor.obj yoneda W) S.arrows
hx : x.Compatible (R := S.arrows)
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := S.arrows.compatibleYonedaFamily_toCocone W x hx
⊢ ∀ (y : Functor.obj (Functor.obj yoneda W) (op X)),
    (fun (t : Functor.obj (Functor.obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := S.arrows) t) y → y = H.desc s

Tactic:
exact fun g hg => H.uniq s g (fun ⟨⟨f, _, hom⟩, hf⟩ => hg hom hf)

Premises used: CategoryTheory.Presieve.cocone, CategoryTheory.Sieve.arrows, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Limits.Cocone.ι, CategoryTheory.CategoryStruct.comp, Eq, CategoryTheory.NatTrans.app, _private.0.CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit.match_2
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasSheafify.{v₁, v₂, u₁, u₂} J A
⊢ HasWeakSheafify.{v₁, v₂, u₁, u₂} J A

Tactic:
HasSheafify.isRightAdjoint

Premises used: CategoryTheory.HasSheafify.isRightAdjoint
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasSheafify.{v₁, v₂, u₁, u₂} J A
⊢ PreservesFiniteLimits (C := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) (Functor.leftAdjoint (sheafToPresheaf J A))

Tactic:
HasSheafify.isLeftExact

Premises used: CategoryTheory.HasSheafify.isLeftExact
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A ⥤ Sheaf.{v₁, v₂, u₁, u₂} J A
adj : F ⊣ sheafToPresheaf J A
inst_2 : PreservesFiniteLimits F
⊢ Functor.IsRightAdjoint (C := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) (sheafToPresheaf J A)

Tactic:
have : (sheafToPresheaf J A).IsRightAdjoint := ⟨_, ⟨adj⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A ⥤ Sheaf.{v₁, v₂, u₁, u₂} J A
adj : F ⊣ sheafToPresheaf J A
inst_2 : PreservesFiniteLimits F
this : Functor.IsRightAdjoint (C := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) (sheafToPresheaf J A)
⊢ ∀ (J_1 : Type) [inst_3 : SmallCategory J_1] [FinCategory J_1],
    PreservesLimitsOfShape (C := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) J_1 (Functor.leftAdjoint (sheafToPresheaf J A))

Tactic:
fun _ _ _ ↦ preservesLimitsOfShape_of_natIso
      (adj.leftAdjointUniq (Adjunction.ofIsRightAdjoint (sheafToPresheaf J A)))

Premises used: CategoryTheory.Adjunction.leftAdjointUniq, CategoryTheory.Limits.preservesLimitsOfShape_of_natIso, CategoryTheory.Adjunction.ofIsRightAdjoint, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A ⥤ Sheaf.{v₁, v₂, u₁, u₂} J A
adj : F ⊣ sheafToPresheaf J A
inst_2 : PreservesFiniteLimits F
this : Functor.IsRightAdjoint (C := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) (sheafToPresheaf J A)
⊢ ∀ (J_1 : Type) [inst_3 : SmallCategory J_1] [FinCategory J_1],
    PreservesLimitsOfShape (C := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) J_1 (Functor.leftAdjoint (sheafToPresheaf J A))

Tactic:
exact fun _ _ _ ↦ preservesLimitsOfShape_of_natIso
      (adj.leftAdjointUniq (Adjunction.ofIsRightAdjoint (sheafToPresheaf J A)))

Premises used: CategoryTheory.Adjunction.leftAdjointUniq, CategoryTheory.Limits.preservesLimitsOfShape_of_natIso, CategoryTheory.Adjunction.ofIsRightAdjoint, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
⊢ HasSheafify.{v₁, v₂, u₁, u₂} (C := C) ⊥ A

Tactic:
HasSheafify.mk' _ _
    (sheafBotEquivalence A).symm.toAdjunction

Premises used: CategoryTheory.sheafBotEquivalence, CategoryTheory.HasSheafify.mk', CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
F G : Sheaf.{v₁, v₂, u₁, u₂} J A
inst_2 : HasWeakSheafify.{v₁, v₂, u₁, u₂} J A
f : F ⟶ G
inst_3 : Mono f
⊢ Mono f.hom

Tactic:
inferInstanceAs (Mono ((sheafToPresheaf J A).map f))

Premises used: _private.0.CategoryTheory.instMonoFunctorOppositeHomFullSubcategoryIsSheafOfHasWeakSheafifyOfSheaf._proof_1
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasSheafify.{v₁, v₂, u₁, u₂} J A
⊢ PreservesFiniteLimits (C := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) (presheafToSheaf J A)

Tactic:
HasSheafify.isLeftExact

Premises used: CategoryTheory.HasSheafify.isLeftExact, CategoryTheory.presheafToSheaf
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasWeakSheafify.{v₁, v₂, u₁, u₂} J A
⊢ Functor.IsLeftAdjoint (C := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) (presheafToSheaf J A)

Tactic:
⟨_, ⟨sheafificationAdjunction J A⟩⟩

Premises used: CategoryTheory.sheafificationAdjunction, Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₂
inst_1 : Category.{v₂, u₂} A
inst_2 : HasSheafify.{v₁, v₂, u₁, u₂} J A
⊢ PreservesFiniteLimits (C := Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ A) (reflector (sheafToPresheaf J A))

Tactic:
inferInstanceAs (PreservesFiniteLimits (presheafToSheaf _ _))

Premises used: _private.0.CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafReflectorSheafToPresheaf._proof_1
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
⊢ Eq (α :=
    Functor.obj (𝟭 (Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D)) P ⟶ Functor.obj (presheafToSheaf J D ⋙ sheafToPresheaf J D) P)
    (NatTrans.app (Adjunction.unit (sheafificationAdjunction J D)) P) (toSheafify J P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
⊢ sheafifyMap J (𝟙 P) = 𝟙 (sheafify J P)

Tactic:
simp [sheafifyMap, sheafify]

Premises used: CategoryTheory.sheafifyMap, CategoryTheory.sheafify
-- Module: Mathlib.CategoryTheory.Sites.Sheafification
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : HasWeakSheafify.{v₁, v_1, u₁, u_1} J D
P Q R : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ D
η : P ⟶ Q
γ : Q ⟶ R
⊢ Eq (α := sheafify J P ⟶ sheafify J R) (sheafifyMap J (η ≫ γ)) (sheafifyMap J η ≫ sheafifyMap J γ)

Tactic:
simp [sheafifyMap, sheafify]

Premises used: CategoryTheory.sheafifyMap, CategoryTheory.sheafify