awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∃ (α_1 : Type) (_ : Finite α_1) (Y_1 : α_1 → C) (π_1 : (a : α_1) → Y_1 a ⟶ Y₁),
    EffectiveEpiFamily Y_1 π_1 ∧
      ∀ (a : α_1),
        (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))).arrows
          (π_1 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)))

Tactic:
apply coherentTopology.mem_sieves_of_hasEffectiveEpiFamily

Premises used: CategoryTheory.coherentTopology.mem_sieves_of_hasEffectiveEpiFamily
-- 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 :
  ∀ ⦃Y_1 : C⦄ (i : α) (h : V ⟶ Y i) (hf : h ≫ π i = f),
    ∃ (α_1 : Type) (_ : Finite α_1) (Y_2 : α_1 → C) (π_1 : (a : α_1) → Y_2 a ⟶ Y i),
      EffectiveEpiFamily Y_2 π_1 ∧
        ∀ (a : α_1),
          (Sieve.pullback (π i)
                (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))).arrows
            (π_1 a)
⊢ ∃ (α_1 : Type) (_ : Finite α_1) (Y_1 : α_1 → C) (π_1 : (a : α_1) → Y_1 a ⟶ Y₁),
    EffectiveEpiFamily Y_1 π_1 ∧
      ∀ (a : α_1),
        (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))).arrows
          (π_1 a)

Tactic:
obtain ⟨i⟩ := hY
-- 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_1 : α → C
π : (a : α) → Y_1 a ⟶ X
h_1 : EffectiveEpiFamily Y_1 π
β : α → Type
inst_3 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y_1 a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y_1 i
hf : h ≫ π i = f
b : β i
⊢ 𝟙 (Y_n i b) ≫ π_n i b ≫ π i = π_n i b ≫ π i

Tactic:
simp
-- 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_1 : α → C
π : (a : α) → Y_1 a ⟶ X
h_1 : EffectiveEpiFamily Y_1 π
β : α → Type
inst_3 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y_1 a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
V : C
f : V ⟶ X
Y : C
i : α
h : V ⟶ Y_1 i
hf : h ≫ π i = f
⊢ ∃ (α_1 : Type) (_ : Finite α_1) (Y : α_1 → C) (π_1 : (a : α_1) → Y a ⟶ Y_1 i),
    EffectiveEpiFamily Y π_1 ∧
      ∀ (a : α_1),
        (Sieve.pullback (π i)
              (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))).arrows
          (π_1 a)

Tactic:
exact ⟨β i, inferInstance, Y_n i, π_n i, H i, fun b ↦
      ⟨Y_n i b, (𝟙 _), π_n i b ≫ π i, ⟨(⟨i, b⟩ : Σ (i : α), β i)⟩, by simp⟩⟩
-- 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 Z : α → C
π : (a : α) → Y a ⟶ X
inst_3 : EffectiveEpiFamily Y π
f : (a : α) → Z a ⟶ Y a
h : ∀ (a : α), EffectiveEpi (f a)
⊢ ∀ (a : α), EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := Y a) (fun (x : Unit) ↦ Z a) fun (x : Unit) ↦ f a

Tactic:
simp_rw [effectiveEpi_iff_effectiveEpiFamily] at h

Premises used: CategoryTheory.effectiveEpi_iff_effectiveEpiFamily
-- 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 Z : α → C
π : (a : α) → Y a ⟶ X
inst_3 : EffectiveEpiFamily Y π
f : (a : α) → Z a ⟶ Y a
h : ∀ (a : α), EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := Y a) (fun (x : Unit) ↦ Z a) fun (x : Unit) ↦ f a
⊢ EffectiveEpiFamily.{v_1, u_1, 0} (B := X) Z fun (a : α) ↦ f a ≫ π a

Tactic:
EffectiveEpiFamily.reindex (e := Equiv.sigmaPUnit α) _ _
    (EffectiveEpiFamily.transitive_of_finite (β := fun _ ↦ Unit) _ inferInstance _ h)

Premises used: Equiv.sigmaPUnit, inferInstance, CategoryTheory.EffectiveEpiFamily.reindex, CategoryTheory.EffectiveEpiFamily.transitive_of_finite
-- 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 Z : α → C
π : (a : α) → Y a ⟶ X
inst_3 : EffectiveEpiFamily Y π
f : (a : α) → Z a ⟶ Y a
h : ∀ (a : α), EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := Y a) (fun (x : Unit) ↦ Z a) fun (x : Unit) ↦ f a
⊢ EffectiveEpiFamily.{v_1, u_1, 0} (B := X) Z fun (a : α) ↦ f a ≫ π a

Tactic:
exact EffectiveEpiFamily.reindex (e := Equiv.sigmaPUnit α) _ _
    (EffectiveEpiFamily.transitive_of_finite (β := fun _ ↦ Unit) _ inferInstance _ h)

Premises used: Equiv.sigmaPUnit, CategoryTheory.EffectiveEpiFamily.reindex
-- 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
mp :
  S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X →
    ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
mpr :
  (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
      EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X
⊢ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X ↔
    ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
constructor
-- 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
Y : C
T : Presieve.{v_1, u_1} Y
hS :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) Y) T
mp :
  ∀ (a : Type) (h : Finite a) (Y' : a → C) (π : (a : a) → Y' a ⟶ Y) (h' : T = Presieve.ofArrows Y' π),
    EffectiveEpiFamily Y' π →
      ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
        EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)

Tactic:
obtain ⟨a, h, Y', π, h', _⟩ := hS
-- 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
Y : C
T : Presieve.{v_1, u_1} Y
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = Presieve.ofArrows Y' π
right : EffectiveEpiFamily Y' π
⊢ ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)

Tactic:
⟨a, h, Y', π, inferInstance, fun a' ↦ ?_⟩

Premises used: inferInstance, And.intro, Exists.intro
-- 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
Y : C
T : Presieve.{v_1, u_1} Y
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = Presieve.ofArrows Y' π
right : EffectiveEpiFamily Y' π
mp : ∀ (a' : a), (Sieve.generate T).arrows (π a')
⊢ ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)

Tactic:
refine ⟨a, h, Y', π, inferInstance, fun a' ↦ ?_⟩
-- 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
Y : C
T : Presieve.{v_1, u_1} Y
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
h' : T = Presieve.ofArrows Y' π
right : EffectiveEpiFamily Y' π
a' : a
mp : (Sieve.generate (Presieve.ofArrows Y' π)).arrows (π a')
⊢ (Sieve.generate T).arrows (π a')

Tactic:
obtain ⟨rfl, _⟩ := h'

Premises used: 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
Y : C
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
right : EffectiveEpiFamily Y' π
a' : a
⊢ 𝟙 Y' a' ≫ π a' = π a'

Tactic:
simp
-- 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
Y : C
a : Type
h : Finite a
Y' : a → C
π : (a : a) → Y' a ⟶ Y
right : EffectiveEpiFamily Y' π
a' : a
⊢ (Sieve.generate (Presieve.ofArrows Y' π)).arrows (π a')

Tactic:
exact ⟨Y' a', 𝟙 Y' a', π a', Presieve.ofArrows.mk a', by simp⟩
-- 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
Y : C
⊢ ∀ (a : Unit),
    Sieve.arrows.{v_1, u_1} (C := C) (X := Y) ⊤ (Y := (fun (x : Unit) ↦ Y) a) ((fun (x : Unit) ↦ (𝟙 Y : Y ⟶ Y)) a)

Tactic:
simp
-- 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
Y : C
⊢ ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), Sieve.arrows ⊤ (π a)

Tactic:
exact ⟨Unit, inferInstance, fun _ => Y, fun _ => (𝟙 Y), inferInstance, by simp⟩
-- 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_1 : Sieve.{v_1, u_1} X
Y : C
R S : Sieve.{v_1, u_1} Y
h : Coverage.Saturate (coherentCoverage C) Y R
h_1 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
a :
  ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), R.arrows (π a)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f →
      ∃ (α : Type) (_ : Finite α) (Y_2 : α → C) (π : (a : α) → Y_2 a ⟶ Y_1),
        EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
mp :
  ∀ (α : Type) (w : Finite α) (Y₁ : α → C) (π : (a : α) → Y₁ a ⟶ Y) (h₁ : EffectiveEpiFamily Y₁ π)
    (h₂ : ∀ (a : α), R.arrows (π a)),
    ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
      EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
obtain ⟨α, w, Y₁, π, ⟨h₁, h₂⟩⟩ := a
-- 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_1 : Sieve.{v_1, u_1} X
Y : C
R S : Sieve.{v_1, u_1} Y
h : Coverage.Saturate (coherentCoverage C) Y R
h_1 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f →
      ∃ (α : Type) (_ : Finite α) (Y_2 : α → C) (π : (a : α) → Y_2 a ⟶ Y_1),
        EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Finite α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
mp :
  ∀ (β : (a : α) → Type),
    (∀ (a : α), Finite (β a)) →
      ∀ (Y_n : (a : α) → β a → C) (π_n : (a : α) → (a_1 : β a) → Y_n a a_1 ⟶ Y₁ a)
        (H :
          ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) ∧ ∀ (a_1 : β a), (Sieve.pullback (π a) S).arrows (π_n a a_1)),
        ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
          EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
choose β _ Y_n π_n H using fun a => b (h₂ a)
-- 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_1 : Sieve.{v_1, u_1} X
Y : C
R S : Sieve.{v_1, u_1} Y
h : Coverage.Saturate (coherentCoverage C) Y R
h_1 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f →
      ∃ (α : Type) (_ : Finite α) (Y_2 : α → C) (π : (a : α) → Y_2 a ⟶ Y_1),
        EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Finite α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : (a : α) → Type
h_2 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (a_1 : β a) → Y_n a a_1 ⟶ Y₁ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) ∧ ∀ (a_1 : β a), (Sieve.pullback (π a) S).arrows (π_n a a_1)
⊢ ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
        EffectiveEpiFamily.transitive_of_finite _ h₁ _ (fun a => (H a).1),
        fun c => (H c.fst).2 c.snd⟩

Premises used: Quiver.Hom, inferInstance, Sigma.fst, _private.0.CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily.match_1, And.right, And.left, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, Sigma.snd, CategoryTheory.EffectiveEpiFamily.transitive_of_finite, Sigma
-- 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_1 : Sieve.{v_1, u_1} X
Y : C
R S : Sieve.{v_1, u_1} Y
h : Coverage.Saturate (coherentCoverage C) Y R
h_1 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f →
      ∃ (α : Type) (_ : Finite α) (Y_2 : α → C) (π : (a : α) → Y_2 a ⟶ Y_1),
        EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Finite α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
β : (a : α) → Type
h_2 : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (a_1 : β a) → Y_n a a_1 ⟶ Y₁ a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a) ∧ ∀ (a_1 : β a), (Sieve.pullback (π a) S).arrows (π_n a a_1)
⊢ ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
    EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
        EffectiveEpiFamily.transitive_of_finite _ h₁ _ (fun a => (H a).1),
        fun c => (H c.fst).2 c.snd⟩
-- 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
h : S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X
mp :
  ∀ (Y : C) (T : Presieve.{v_1, u_1} Y)
    (hS :
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) Y) T),
    ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
      EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), (Sieve.generate T).arrows (π a)
mp₁ :
  ∀ (Y : C),
    ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
      EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), Sieve.arrows ⊤ (π a)
mp₂ :
  ∀ (Y : C) (R S : Sieve.{v_1, u_1} Y),
    Coverage.Saturate (coherentCoverage C) Y R →
      (∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (coherentCoverage C) Y_1 (Sieve.pullback f S)) →
        ∀
          (a :
            ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
              EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), R.arrows (π a))
          (b :
            ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
              R.arrows f →
                ∃ (α : Type) (_ : Finite α) (Y_2 : α → C) (π : (a : α) → Y_2 a ⟶ Y_1),
                  EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)),
          ∃ (α : Type) (_ : Finite α) (Y_1 : α → C) (π : (a : α) → Y_1 a ⟶ Y),
            EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
⊢ ∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X), EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
induction h with
    | of Y T hS =>
      obtain ⟨a, h, Y', π, h', _⟩ := hS
      refine ⟨a, h, Y', π, inferInstance, fun a' ↦ ?_⟩
      obtain ⟨rfl, _⟩ := h'
      exact ⟨Y' a', 𝟙 Y' a', π a', Presieve.ofArrows.mk a', by simp⟩
    | top Y =>
      exact ⟨Unit, inferInstance, fun _ => Y, fun _ => (𝟙 Y), inferInstance, by simp⟩
    | transitive Y R S _ _ a b =>
      obtain ⟨α, w, Y₁, π, ⟨h₁, h₂⟩⟩ := a
      choose β _ Y_n π_n H using fun a => b (h₂ a)
      exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
        EffectiveEpiFamily.transitive_of_finite _ h₁ _ (fun a => (H a).1),
        fun c => (H c.fst).2 c.snd⟩

Premises used: 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) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
      EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X

Tactic:
coherentTopology.mem_sieves_of_hasEffectiveEpiFamily S

Premises used: CategoryTheory.coherentTopology.mem_sieves_of_hasEffectiveEpiFamily
-- 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) (_ : Finite α) (Y : α → C) (π : (a : α) → Y a ⟶ X),
      EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X

Tactic:
exact coherentTopology.mem_sieves_of_hasEffectiveEpiFamily S

Premises used: CategoryTheory.coherentTopology.mem_sieves_of_hasEffectiveEpiFamily
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h : EffectiveEpi g
⊢ (EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := Y) (fun (x : PUnit.{1}) ↦ Z) fun (x : PUnit.{1}) ↦
      match (motive := (x : PUnit.{1}) → (fun (x : PUnit.{1}) ↦ Z) x ⟶ Y) x with
      | PUnit.unit => g) →
    ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
      EffectiveEpiFamily X₂ π₂ ∧
        ∃ (i : β → PUnit.{1}) (ι : (b : β) → X₂ b ⟶ Z),
          ∀ (b : β),
            (ι b ≫
                match (motive := (x : PUnit.{1}) → (fun (x : PUnit.{1}) ↦ Z) x ⟶ Y) i b with
                | PUnit.unit => g) =
              π₂ b ≫ f

Tactic:
have hp := Precoherent.pullback f PUnit (fun () ↦ Z) (fun () ↦ g)
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h : EffectiveEpi g
hp :
  (EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := Y) (fun (x : PUnit.{1}) ↦ Z) fun (x : PUnit.{1}) ↦
      match (motive := (x : PUnit.{1}) → (fun (x : PUnit.{1}) ↦ Z) x ⟶ Y) x with
      | PUnit.unit => g) →
    ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
      EffectiveEpiFamily X₂ π₂ ∧
        ∃ (i : β → PUnit.{1}) (ι : (b : β) → X₂ b ⟶ Z),
          ∀ (b : β),
            (ι b ≫
                match (motive := (x : PUnit.{1}) → (fun (x : PUnit.{1}) ↦ Z) x ⟶ Y) i b with
                | PUnit.unit => g) =
              π₂ b ≫ f
⊢ (EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := Y) (fun (x : PUnit.{1}) ↦ Z) fun (x : PUnit.{1}) ↦ g) →
    ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
      EffectiveEpiFamily X₂ π₂ ∧ ∃ (ι : (b : β) → X₂ b ⟶ Z), ∀ (b : β), ι b ≫ g = π₂ b ≫ f

Tactic:
simp only [exists_const] at hp

Premises used: exists_const