awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y_1 : C
f : Y_1 ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y_1 := fun (a : α) ↦ pullback.fst f (π a)
Y : C
a : α
⊢ Presieve.ofArrows Z π (π a)

Tactic:
Presieve.ofArrows.mk a

Premises used: CategoryTheory.Presieve.ofArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y_1 : C
f : Y_1 ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y_1 := fun (a : α) ↦ pullback.fst f (π a)
Y : C
a : α
⊢ Presieve.ofArrows Z π (π a)

Tactic:
exact Presieve.ofArrows.mk a

Premises used: CategoryTheory.Presieve.ofArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
P : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
mp :
  Presieve.IsSheaf (coherentTopology C) P →
    ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
mpr :
  (∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)) →
    Presieve.IsSheaf (coherentTopology C) P
⊢ Presieve.IsSheaf (coherentTopology C) P ↔
    ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
P : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf (coherentTopology C) P
B : C
α : Type
mp :
  ∀ [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
⊢ ∀ [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
P : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
hP : Presieve.IsSheaf (coherentTopology C) P
B : C
α : Type
inst_2 : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
⊢ ∀ {X : C} (R : Presieve.{v_1, u_1} X),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
        (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) R →
      Presieve.IsSheafFor P R

Tactic:
simp only [coherentTopology, Presieve.isSheaf_coverage] at hP

Premises used: CategoryTheory.Presieve.isSheaf_coverage, CategoryTheory.coherentTopology
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
P : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
B : C
α : Type
inst_2 : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
hP :
  ∀ {X : C} (R : Presieve.{v_1, u_1} X),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
        (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) R →
      Presieve.IsSheafFor P R
mp :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} B))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) B) (Presieve.ofArrows X π)
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
apply hP
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
P : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
B : C
α : Type
inst_2 : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
hP :
  ∀ {X : C} (R : Presieve.{v_1, u_1} X),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
        (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) R →
      Presieve.IsSheafFor P R
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} B))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) B) (Presieve.ofArrows X π)

Tactic:
⟨α, inferInstance, X, π, rfl, h⟩

Premises used: Set.Mem, setOf, inferInstance, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
P : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
B : C
α : Type
inst_2 : Finite α
X : α → C
π : (a : α) → X a ⟶ B
h : EffectiveEpiFamily X π
hP :
  ∀ {X : C} (R : Presieve.{v_1, u_1} X),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
        (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) R →
      Presieve.IsSheafFor P R
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} B))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) B) (Presieve.ofArrows X π)

Tactic:
exact ⟨α, inferInstance, X, π, rfl, h⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
P : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
h :
  ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
mpr :
  ∀ {X : C} (R : Presieve.{v_1, u_1} X),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
        (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) R →
      Presieve.IsSheafFor P R
⊢ Presieve.IsSheaf (coherentTopology C) P

Tactic:
simp only [coherentTopology, Presieve.isSheaf_coverage]

Premises used: CategoryTheory.Presieve.isSheaf_coverage, CategoryTheory.coherentTopology
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
P : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
h :
  ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
B : C
α : Type
w : Finite α
X : α → C
π : (a : α) → X a ⟶ B
hS : EffectiveEpiFamily X π
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
h _ _ _ _ hS
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
P : Functor.{v_1, w, u_1, w + 1} Cᵒᵖ (Type w)
h :
  ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)
B : C
α : Type
w : Finite α
X : α → C
π : (a : α) → X a ⟶ B
hS : EffectiveEpiFamily X π
⊢ Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
exact h _ _ _ _ hS
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W : C
rw :
  ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor (Functor.obj yoneda W) (Presieve.ofArrows X π)
⊢ Presieve.IsSheaf.{v_1, v_1, u_1} (coherentTopology C) (Functor.obj yoneda W)

Tactic:
rw [isSheaf_coherent]

Premises used: CategoryTheory.isSheaf_coherent
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
_ :
  ∀ [Finite α] (X_1 : α → C) (π : (a : α) → X_1 a ⟶ X),
    EffectiveEpiFamily X_1 π → Presieve.IsSheafFor (Functor.obj yoneda W) (Presieve.ofArrows X_1 π)
⊢ ∀ [Finite α] (X_1 : α → C) (π : (a : α) → X_1 a ⟶ X),
    EffectiveEpiFamily X_1 π → Presieve.IsSheafFor (Functor.obj yoneda W) (Presieve.ofArrows X_1 π)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
have :
  ∀ (h_colim : Limits.IsColimit (Sieve.generateFamily Y π).arrows.cocone),
    Presieve.IsSheafFor (Functor.obj yoneda W) (Presieve.ofArrows Y π)
⊢ Presieve.IsSheafFor (Functor.obj yoneda W) (Presieve.ofArrows Y π)

Tactic:
have h_colim := isColimitOfEffectiveEpiFamilyStruct Y π H.effectiveEpiFamily.some
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generateFamily Y π).arrows.cocone
rw :
  ∀ (h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone),
    Presieve.IsSheafFor (Functor.obj yoneda W) (Presieve.ofArrows Y π)
⊢ Presieve.IsSheafFor (Functor.obj yoneda W) (Presieve.ofArrows Y π)

Tactic:
rw [← Sieve.generateFamily_eq] at h_colim

Premises used: CategoryTheory.Sieve.generateFamily_eq
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (Functor.obj yoneda W) (Presieve.ofArrows Y π)
hx : x.Compatible (R := Presieve.ofArrows Y π)
x_ext : Presieve.FamilyOfElements (Functor.obj yoneda W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  x.sieveExtend (R := Presieve.ofArrows Y π)
⊢ x.sieveExtend (R := Presieve.ofArrows Y π).Compatible (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows)

Tactic:
have hx_ext := Presieve.FamilyOfElements.Compatible.sieveExtend hx
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (Functor.obj yoneda W) (Presieve.ofArrows Y π)
hx : x.Compatible (R := Presieve.ofArrows Y π)
x_ext : Presieve.FamilyOfElements (Functor.obj yoneda W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  x.sieveExtend (R := Presieve.ofArrows Y π)
hx_ext : x.sieveExtend (R := Presieve.ofArrows Y π).Compatible (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows)
S : Sieve.{v_1, u_1} X := Sieve.generate (Presieve.ofArrows Y π)
⊢ ∃! t : Functor.obj (Functor.obj yoneda W) (Opposite.op X),
    x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t

Tactic:
(Sieve.forallYonedaIsSheaf_iff_colimit S).mpr ⟨h_colim⟩ W x_ext hx_ext

Premises used: Iff.mpr, Nonempty.intro, CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (Functor.obj yoneda W) (Presieve.ofArrows Y π)
hx : x.Compatible (R := Presieve.ofArrows Y π)
x_ext : Presieve.FamilyOfElements (Functor.obj yoneda W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  x.sieveExtend (R := Presieve.ofArrows Y π)
hx_ext : x.sieveExtend (R := Presieve.ofArrows Y π).Compatible (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows)
S : Sieve.{v_1, u_1} X := Sieve.generate (Presieve.ofArrows Y π)
obtain :
  ∀ (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X))
    (t_amalg : x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t)
    (t_uniq :
      ∀ (y : Functor.obj (Functor.obj yoneda W) (Opposite.op X)),
        (fun (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)) ↦
              x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t)
            y →
          y = t),
    ∃! t : Functor.obj (Functor.obj yoneda W) (Opposite.op X), x.IsAmalgamation (R := Presieve.ofArrows Y π) t
⊢ ∃! t : Functor.obj (Functor.obj yoneda W) (Opposite.op X), x.IsAmalgamation (R := Presieve.ofArrows Y π) t

Tactic:
obtain ⟨t, t_amalg, t_uniq⟩ : ∃! t, x_ext.IsAmalgamation t :=
    (Sieve.forallYonedaIsSheaf_iff_colimit S).mpr ⟨h_colim⟩ W x_ext hx_ext

Premises used: Iff.mpr, Nonempty.intro, CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (Functor.obj yoneda W) (Presieve.ofArrows Y π)
hx : x.Compatible (R := Presieve.ofArrows Y π)
x_ext : Presieve.FamilyOfElements (Functor.obj yoneda W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  x.sieveExtend (R := Presieve.ofArrows Y π)
hx_ext : x.sieveExtend (R := Presieve.ofArrows Y π).Compatible (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows)
S : Sieve.{v_1, u_1} X := Sieve.generate (Presieve.ofArrows Y π)
t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)
t_amalg : x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t
t_uniq :
  ∀ (y : Functor.obj (Functor.obj yoneda W) (Opposite.op X)),
    (fun (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)) ↦
          x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t)
        y →
      y = t
⊢ ∃! t : Functor.obj (Functor.obj yoneda W) (Opposite.op X), x.IsAmalgamation (R := Presieve.ofArrows Y π) t

Tactic:
⟨t, ?_, ?_⟩

Premises used: ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (Functor.obj yoneda W) (Presieve.ofArrows Y π)
hx : x.Compatible (R := Presieve.ofArrows Y π)
x_ext : Presieve.FamilyOfElements (Functor.obj yoneda W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  x.sieveExtend (R := Presieve.ofArrows Y π)
hx_ext : x.sieveExtend (R := Presieve.ofArrows Y π).Compatible (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows)
S : Sieve.{v_1, u_1} X := Sieve.generate (Presieve.ofArrows Y π)
t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)
t_amalg : x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t
t_uniq :
  ∀ (y : Functor.obj (Functor.obj yoneda W) (Opposite.op X)),
    (fun (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)) ↦
          x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t)
        y →
      y = t
refine_1 :
  (fun (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)) ↦ x.IsAmalgamation (R := Presieve.ofArrows Y π) t) t
refine_2 :
  ∀ (y : Functor.obj (Functor.obj yoneda W) (Opposite.op X)),
    (fun (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)) ↦ x.IsAmalgamation (R := Presieve.ofArrows Y π) t) y →
      y = t
⊢ ∃! t : Functor.obj (Functor.obj yoneda W) (Opposite.op X), x.IsAmalgamation (R := Presieve.ofArrows Y π) t

Tactic:
refine ⟨t, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (Functor.obj yoneda W) (Presieve.ofArrows Y π)
hx : x.Compatible (R := Presieve.ofArrows Y π)
x_ext : Presieve.FamilyOfElements (Functor.obj yoneda W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  x.sieveExtend (R := Presieve.ofArrows Y π)
hx_ext : x.sieveExtend (R := Presieve.ofArrows Y π).Compatible (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows)
S : Sieve.{v_1, u_1} X := Sieve.generate (Presieve.ofArrows Y π)
t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)
t_amalg : x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t
t_uniq :
  ∀ (y : Functor.obj (Functor.obj yoneda W) (Opposite.op X)),
    (fun (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)) ↦
          x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t)
        y →
      y = t
⊢ (Presieve.FamilyOfElements.restrict (R₁ := Presieve.ofArrows Y π) (R₂ :=
        (Sieve.generate (Presieve.ofArrows Y π)).arrows) ⋯ x_ext).IsAmalgamation
    (R := Presieve.ofArrows Y π) t

Tactic:
Presieve.isAmalgamation_restrict (Sieve.le_generate (Presieve.ofArrows Y π)) _ _ t_amalg

Premises used: CategoryTheory.Sieve.le_generate, CategoryTheory.Presieve.isAmalgamation_restrict, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (Functor.obj yoneda W) (Presieve.ofArrows Y π)
hx : x.Compatible (R := Presieve.ofArrows Y π)
x_ext : Presieve.FamilyOfElements (Functor.obj yoneda W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  x.sieveExtend (R := Presieve.ofArrows Y π)
hx_ext : x.sieveExtend (R := Presieve.ofArrows Y π).Compatible (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows)
S : Sieve.{v_1, u_1} X := Sieve.generate (Presieve.ofArrows Y π)
t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)
t_amalg : x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t
t_uniq :
  ∀ (y : Functor.obj (Functor.obj yoneda W) (Opposite.op X)),
    (fun (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)) ↦
          x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t)
        y →
      y = t
h :
  x =
    Presieve.FamilyOfElements.restrict (R₁ := Presieve.ofArrows Y π) (R₂ :=
      (Sieve.generate (Presieve.ofArrows Y π)).arrows) ⋯ x_ext
⊢ (fun (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)) ↦ x.IsAmalgamation (R := Presieve.ofArrows Y π) t) t

Tactic:
convert!
    Presieve.isAmalgamation_restrict (Sieve.le_generate (Presieve.ofArrows Y π)) _ _ t_amalg

Premises used: CategoryTheory.Sieve.le_generate, CategoryTheory.Presieve.isAmalgamation_restrict, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (Functor.obj yoneda W) (Presieve.ofArrows Y π)
hx : x.Compatible (R := Presieve.ofArrows Y π)
x_ext : Presieve.FamilyOfElements (Functor.obj yoneda W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  x.sieveExtend (R := Presieve.ofArrows Y π)
hx_ext : x.sieveExtend (R := Presieve.ofArrows Y π).Compatible (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows)
S : Sieve.{v_1, u_1} X := Sieve.generate (Presieve.ofArrows Y π)
t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)
t_amalg : x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t
t_uniq :
  ∀ (y : Functor.obj (Functor.obj yoneda W) (Opposite.op X)),
    (fun (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)) ↦
          x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t)
        y →
      y = t
⊢ x =
    Presieve.FamilyOfElements.restrict (R₁ := Presieve.ofArrows Y π) (R₂ :=
      (Sieve.generate (Presieve.ofArrows Y π)).arrows) ⋯ x_ext

Tactic:
(Presieve.restrict_extend hx).symm

Premises used: CategoryTheory.Presieve.restrict_extend, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (Functor.obj yoneda W) (Presieve.ofArrows Y π)
hx : x.Compatible (R := Presieve.ofArrows Y π)
x_ext : Presieve.FamilyOfElements (Functor.obj yoneda W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  x.sieveExtend (R := Presieve.ofArrows Y π)
hx_ext : x.sieveExtend (R := Presieve.ofArrows Y π).Compatible (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows)
S : Sieve.{v_1, u_1} X := Sieve.generate (Presieve.ofArrows Y π)
t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)
t_amalg : x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t
t_uniq :
  ∀ (y : Functor.obj (Functor.obj yoneda W) (Opposite.op X)),
    (fun (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)) ↦
          x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t)
        y →
      y = t
⊢ x =
    Presieve.FamilyOfElements.restrict (R₁ := Presieve.ofArrows Y π) (R₂ :=
      (Sieve.generate (Presieve.ofArrows Y π)).arrows) ⋯ x_ext

Tactic:
exact (Presieve.restrict_extend hx).symm

Premises used: CategoryTheory.Presieve.restrict_extend, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
W X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (Functor.obj yoneda W) (Presieve.ofArrows Y π)
hx : x.Compatible (R := Presieve.ofArrows Y π)
x_ext : Presieve.FamilyOfElements (Functor.obj yoneda W) (Sieve.generate (Presieve.ofArrows Y π)).arrows :=
  x.sieveExtend (R := Presieve.ofArrows Y π)
hx_ext : x.sieveExtend (R := Presieve.ofArrows Y π).Compatible (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows)
S : Sieve.{v_1, u_1} X := Sieve.generate (Presieve.ofArrows Y π)
t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)
t_amalg : x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t
t_uniq :
  ∀ (y : Functor.obj (Functor.obj yoneda W) (Opposite.op X)),
    (fun (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)) ↦
          x_ext.IsAmalgamation (R := (Sieve.generate (Presieve.ofArrows Y π)).arrows) t)
        y →
      y = t
⊢ ∀ (y : Functor.obj (Functor.obj yoneda W) (Opposite.op X)),
    (fun (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)) ↦ x.IsAmalgamation (R := Presieve.ofArrows Y π) t) y →
      y = t

Tactic:
fun y hy ↦ t_uniq y <| Presieve.isAmalgamation_sieveExtend x y hy

Premises used: CategoryTheory.Presieve.isAmalgamation_sieveExtend