awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact fun y hy ↦ t_uniq y <| Presieve.isAmalgamation_sieveExtend x y hy

Premises used: CategoryTheory.Presieve.isAmalgamation_sieveExtend
-- 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
⊢ GrothendieckTopology.Subcanonical.{v_1, u_1} (coherentTopology C)

Tactic:
GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ isSheaf_yoneda_obj

Premises used: CategoryTheory.coherentTopology.isSheaf_yoneda_obj, CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
h : Presieve.ofArrows Y π ≤ S.arrows
hR :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) (Presieve.ofArrows Y π)
⊢ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X

Tactic:
apply (coherentCoverage C).mem_toGrothendieck_sieves_of_superset (R := Presieve.ofArrows Y π)

Premises used: CategoryTheory.Coverage.mem_toGrothendieck_sieves_of_superset, CategoryTheory.coherentCoverage
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
x : C
x_1 : x ⟶ X
h : Presieve.ofArrows Y π x_1
mk : ∀ (i : α), S.arrows (π i)
⊢ S.arrows x_1

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
i : α
⊢ S.arrows (π i)

Tactic:
hπ.2 _

Premises used: And.right
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
i : α
⊢ S.arrows (π i)

Tactic:
exact hπ.2 _

Premises used: And.right
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ≤ S.arrows

Tactic:
exact fun _ _ h ↦ by cases h; exact hπ.2 _
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) (Presieve.ofArrows Y π)

Tactic:
⟨_, inferInstance, Y, π, rfl, hπ.1⟩

Premises used: Set.Mem, setOf, inferInstance, And.left, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
α : Type
w : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) (Presieve.ofArrows Y π)

Tactic:
exact ⟨_, inferInstance, Y, π, rfl, hπ.1⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst_3 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
rw :
  Presieve.EffectiveEpimorphic.{v_1, u_1} (C := C) (X := X)
    (Presieve.ofArrows (fun (c : (a : α) × β a) ↦ Y_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)))
      fun (c : (a : α) × β a) ↦
      π_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)) ≫ π (c.fst (β := fun (a : α) ↦ β a)))
⊢ EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := X)
    (fun (c : (a : α) × β a) ↦ Y_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)))
    fun (c : (a : α) × β a) ↦
    π_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)) ≫ π (c.fst (β := fun (a : α) ↦ β a))

Tactic:
rw [← Sieve.effectiveEpimorphic_family]

Premises used: CategoryTheory.Sieve.effectiveEpimorphic_family
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst_3 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (Presieve.ofArrows
        (fun (x : (x : α) × β x) ↦
          match (motive := (x : α) × β x → C) x with
          | ⟨a, b⟩ => Y_n a b)
        fun (x : (x : α) × β x) ↦
        match (motive :=
          (x : (x : α) × β x) →
            (fun (x : (x : α) × β x) ↦
                  (match (motive := (x : α) × β x → C) x with
                    | ⟨a, b⟩ => Y_n a b :
                    C))
                x ⟶
              X)
          x with
        | ⟨a, b⟩ => π_n a b ≫ π a) ∈
    (coherentTopology C : (a : C) → Set (Sieve a)) X
rw :
  ∀ (W : C),
    Presieve.IsSheafFor.{v_1, v_1, u_1} (X := X) (Functor.obj yoneda W)
      (Sieve.arrows
        (Sieve.generate
          (Presieve.ofArrows
            (fun (c : (a : α) × β a) ↦ Y_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)))
            fun (c : (a : α) × β a) ↦
            π_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)) ≫
              π (c.fst (β := fun (a : α) ↦ β a)))))
⊢ Nonempty
    (Limits.IsColimit (J :=
      Presieve.category.{v_1, u_1} (C := C) (X := X)
        (Sieve.arrows
          (Sieve.generate
            (Presieve.ofArrows
              (fun (c : (a : α) × β a) ↦ Y_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)))
              fun (c : (a : α) × β a) ↦
              π_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)) ≫
                π (c.fst (β := fun (a : α) ↦ β a))))))
      (Presieve.cocone
        (Sieve.arrows
          (Sieve.generate
            (Presieve.ofArrows
              (fun (c : (a : α) × β a) ↦ Y_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)))
              fun (c : (a : α) × β a) ↦
              π_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)) ≫
                π (c.fst (β := fun (a : α) ↦ β a)))))))

Tactic:
rw [← Sieve.forallYonedaIsSheaf_iff_colimit]

Premises used: CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst_3 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (Presieve.ofArrows
        (fun (x : (x : α) × β x) ↦
          match (motive := (x : α) × β x → C) x with
          | ⟨a, b⟩ => Y_n a b)
        fun (x : (x : α) × β x) ↦
        match (motive :=
          (x : (x : α) × β x) →
            (fun (x : (x : α) × β x) ↦
                  (match (motive := (x : α) × β x → C) x with
                    | ⟨a, b⟩ => Y_n a b :
                    C))
                x ⟶
              X)
          x with
        | ⟨a, b⟩ => π_n a b ≫ π a) ∈
    (coherentTopology C : (a : C) → Set (Sieve a)) X
⊢ ∀ (W : C),
    Presieve.IsSheafFor.{v_1, v_1, u_1} (X := X) (Functor.obj yoneda W)
      (Sieve.arrows
        (Sieve.generate
          (Presieve.ofArrows
            (fun (c : (a : α) × β a) ↦ Y_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)))
            fun (c : (a : α) × β a) ↦
            π_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)) ≫
              π (c.fst (β := fun (a : α) ↦ β a)))))

Tactic:
fun W => coherentTopology.isSheaf_yoneda_obj W _ h₂

Premises used: Sigma.fst, CategoryTheory.coherentTopology.isSheaf_yoneda_obj, CategoryTheory.CategoryStruct.comp, CategoryTheory.Sieve.generate, Sigma.snd, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst_3 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (Presieve.ofArrows
        (fun (x : (x : α) × β x) ↦
          match (motive := (x : α) × β x → C) x with
          | ⟨a, b⟩ => Y_n a b)
        fun (x : (x : α) × β x) ↦
        match (motive :=
          (x : (x : α) × β x) →
            (fun (x : (x : α) × β x) ↦
                  (match (motive := (x : α) × β x → C) x with
                    | ⟨a, b⟩ => Y_n a b :
                    C))
                x ⟶
              X)
          x with
        | ⟨a, b⟩ => π_n a b ≫ π a) ∈
    (coherentTopology C : (a : C) → Set (Sieve a)) X
⊢ ∀ (W : C),
    Presieve.IsSheafFor.{v_1, v_1, u_1} (X := X) (Functor.obj yoneda W)
      (Sieve.arrows
        (Sieve.generate
          (Presieve.ofArrows
            (fun (c : (a : α) × β a) ↦ Y_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)))
            fun (c : (a : α) × β a) ↦
            π_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)) ≫
              π (c.fst (β := fun (a : α) ↦ β a)))))

Tactic:
exact fun W => coherentTopology.isSheaf_yoneda_obj W _ h₂

Premises used: Quiver.Hom, _private.0.CategoryTheory.EffectiveEpiFamily.transitive_of_finite.match_1, CategoryTheory.coherentTopology.isSheaf_yoneda_obj, CategoryTheory.CategoryStruct.comp, CategoryTheory.Sieve.generate, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst_3 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
suffices :
  Sieve.generate
      (Presieve.ofArrows
        (fun (x : (x : α) × β x) ↦
          match (motive := (x : α) × β x → C) x with
          | ⟨a, b⟩ => Y_n a b)
        fun (x : (x : α) × β x) ↦
        match (motive :=
          (x : (x : α) × β x) →
            (fun (x : (x : α) × β x) ↦
                  (match (motive := (x : α) × β x → C) x with
                    | ⟨a, b⟩ => Y_n a b :
                    C))
                x ⟶
              X)
          x with
        | ⟨a, b⟩ => π_n a b ≫ π a) ∈
    (coherentTopology C : (a : C) → Set (Sieve a)) X
⊢ Presieve.EffectiveEpimorphic.{v_1, u_1} (C := C) (X := X)
    (Presieve.ofArrows (fun (c : (a : α) × β a) ↦ Y_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)))
      fun (c : (a : α) × β a) ↦
      π_n (c.fst (β := fun (a : α) ↦ β a)) (c.snd (β := fun (a : α) ↦ β a)) ≫ π (c.fst (β := fun (a : α) ↦ β a)))

Tactic:
suffices h₂ : (Sieve.generate (Presieve.ofArrows (fun (⟨a, b⟩ : Σ _, β _) => Y_n a b)
        (fun ⟨a,b⟩ => π_n a b ≫ π a))) ∈ (coherentTopology C) X by
    change Nonempty _
    rw [← Sieve.forallYonedaIsSheaf_iff_colimit]
    exact fun W => coherentTopology.isSheaf_yoneda_obj W _ h₂
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst_3 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
a : Coverage.Saturate (coherentCoverage C) X (Sieve.generate (Presieve.ofArrows Y π))
a₁ :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
    (Sieve.generate (Presieve.ofArrows Y π)).arrows f →
      Coverage.Saturate (coherentCoverage C) Y_1
        (Sieve.pullback f
          (Sieve.generate
            (Presieve.ofArrows
              (fun (x : (x : α) × β x) ↦
                match (motive := (x : α) × β x → C) x with
                | ⟨a, b⟩ => Y_n a b)
              fun (x : (x : α) × β x) ↦
              match (motive :=
                (x : (x : α) × β x) →
                  (fun (x : (x : α) × β x) ↦
                        (match (motive := (x : α) × β x → C) x with
                          | ⟨a, b⟩ => Y_n a b :
                          C))
                      x ⟶
                    X)
                x with
              | ⟨a, b⟩ => π_n a b ≫ π a)))
⊢ Sieve.generate
      (Presieve.ofArrows
        (fun (x : (x : α) × β x) ↦
          match (motive := (x : α) × β x → C) x with
          | ⟨a, b⟩ => Y_n a b)
        fun (x : (x : α) × β x) ↦
        match (motive :=
          (x : (x : α) × β x) →
            (fun (x : (x : α) × β x) ↦
                  (match (motive := (x : α) × β x → C) x with
                    | ⟨a, b⟩ => Y_n a b :
                    C))
                x ⟶
              X)
          x with
        | ⟨a, b⟩ => π_n a b ≫ π a) ∈
    (coherentTopology C : (a : C) → Set (Sieve a)) X

Tactic:
apply Coverage.Saturate.transitive X (Sieve.generate (Presieve.ofArrows Y π))

Premises used: CategoryTheory.Coverage.Saturate.transitive, CategoryTheory.Sieve.generate, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst_3 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
a :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) (Presieve.ofArrows Y π)
⊢ Coverage.Saturate (coherentCoverage C) X (Sieve.generate (Presieve.ofArrows Y π))

Tactic:
apply Coverage.Saturate.of

Premises used: CategoryTheory.Coverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst_3 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
w : Type
w₁ : Finite α
w₂ : α → C
w₃ : (a : α) → Y a ⟶ X
h₁ : Presieve.ofArrows Y π = Presieve.ofArrows Y π ∧ EffectiveEpiFamily Y π
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) (Presieve.ofArrows Y π)

Tactic:
use α, inferInstance, Y, π
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst_3 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
V : C
f : V ⟶ X
a :
  ∀ (Y₁ : C) (h : V ⟶ Y₁) (g : Y₁ ⟶ X) (hY : Presieve.ofArrows Y π g) (hf : h ≫ g = f),
    Coverage.Saturate (coherentCoverage C) V
      (Sieve.pullback f
        (Sieve.generate
          (Presieve.ofArrows
            (fun (x : (x : α) × β x) ↦
              match (motive := (x : α) × β x → C) x with
              | ⟨a, b⟩ => Y_n a b)
            fun (x : (x : α) × β x) ↦
            match (motive :=
              (x : (x : α) × β x) →
                (fun (x : (x : α) × β x) ↦
                      (match (motive := (x : α) × β x → C) x with
                        | ⟨a, b⟩ => Y_n a b :
                        C))
                    x ⟶
                  X)
              x with
            | ⟨a, b⟩ => π_n a b ≫ π a)))
⊢ (Sieve.generate (Presieve.ofArrows Y π)).arrows f →
    Coverage.Saturate (coherentCoverage C) V
      (Sieve.pullback f
        (Sieve.generate
          (Presieve.ofArrows
            (fun (x : (x : α) × β x) ↦
              match (motive := (x : α) × β x → C) x with
              | ⟨a, b⟩ => Y_n a b)
            fun (x : (x : α) × β x) ↦
            match (motive :=
              (x : (x : α) × β x) →
                (fun (x : (x : α) × β x) ↦
                      (match (motive := (x : α) × β x → C) x with
                        | ⟨a, b⟩ => Y_n a b :
                        C))
                    x ⟶
                  X)
              x with
            | ⟨a, b⟩ => π_n a b ≫ π a)))

Tactic:
⟨Y₁, h, g, ⟨hY, hf⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h_1 : EffectiveEpiFamily Y π
β : α → Type
inst_3 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : Presieve.ofArrows Y π g
hf : h ≫ g = f
a :
  Coverage.Saturate (coherentCoverage C) V
    (Sieve.pullback h
      (Sieve.pullback g
        (Sieve.generate
          (Presieve.ofArrows
            (fun (x : (x : α) × β x) ↦
              match (motive := (x : α) × β x → C) x with
              | ⟨a, b⟩ => Y_n a b)
            fun (x : (x : α) × β x) ↦
            match (motive :=
              (x : (x : α) × β x) →
                (fun (x : (x : α) × β x) ↦
                      (match (motive := (x : α) × β x → C) x with
                        | ⟨a, b⟩ => Y_n a b :
                        C))
                    x ⟶
                  X)
              x with
            | ⟨a, b⟩ => π_n a b ≫ π a))))
⊢ Coverage.Saturate (coherentCoverage C) V
    (Sieve.pullback f
      (Sieve.generate
        (Presieve.ofArrows
          (fun (x : (x : α) × β x) ↦
            match (motive := (x : α) × β x → C) x with
            | ⟨a, b⟩ => Y_n a b)
          fun (x : (x : α) × β x) ↦
          match (motive :=
            (x : (x : α) × β x) →
              (fun (x : (x : α) × β x) ↦
                    (match (motive := (x : α) × β x → C) x with
                      | ⟨a, b⟩ => Y_n a b :
                      C))
                  x ⟶
                X)
            x with
          | ⟨a, b⟩ => π_n a b ≫ π a)))

Tactic:
rw [← hf, Sieve.pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_comp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
X : C
α : Type
inst_2 : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h_1 : EffectiveEpiFamily Y π
β : α → Type
inst_3 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : Presieve.ofArrows Y π g
hf : h ≫ g = f
a :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} Y₁)) (GrothendieckTopology.sieves (coherentTopology C) Y₁)
    (Sieve.pullback g
      (Sieve.generate
        (Presieve.ofArrows
          (fun (x : (x : α) × β x) ↦
            match (motive := (x : α) × β x → C) x with
            | ⟨a, b⟩ => Y_n a b)
          fun (x : (x : α) × β x) ↦
          match (motive :=
            (x : (x : α) × β x) →
              (fun (x : (x : α) × β x) ↦
                    (match (motive := (x : α) × β x → C) x with
                      | ⟨a, b⟩ => Y_n a b :
                      C))
                  x ⟶
                X)
            x with
          | ⟨a, b⟩ => π_n a b ≫ π a)))
⊢ Coverage.Saturate (coherentCoverage C) V
    (Sieve.pullback h
      (Sieve.pullback g
        (Sieve.generate
          (Presieve.ofArrows
            (fun (x : (x : α) × β x) ↦
              match (motive := (x : α) × β x → C) x with
              | ⟨a, b⟩ => Y_n a b)
            fun (x : (x : α) × β x) ↦
            match (motive :=
              (x : (x : α) × β x) →
                (fun (x : (x : α) × β x) ↦
                      (match (motive := (x : α) × β x → C) x with
                        | ⟨a, b⟩ => Y_n a b :
                        C))
                    x ⟶
                  X)
              x with
            | ⟨a, b⟩ => π_n a b ≫ π a))))

Tactic:
apply (coherentTopology C).pullback_stable'

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable', CategoryTheory.coherentTopology