-- Mathlib/CategoryTheory/Sites/Coherent/CoherentTopology.lean
theorem EffectiveEpiFamily.transitive_of_finite {α : Type} [Finite α] {Y : α → C}
    (π : (a : α) → (Y a ⟶ X)) (h : EffectiveEpiFamily Y π) {β : α → Type} [∀ (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)) :
    EffectiveEpiFamily
      (fun (c : Σ a, β a) => Y_n c.fst c.snd) (fun c => π_n c.fst c.snd ≫ π c.fst)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (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 =>
          match x with
          | ⟨a, b⟩ => Y_n a b)
        fun x =>
        match x with
        | ⟨a, b⟩ => π_n a b ≫ π a) ∈
    (coherentTopology C) X
⊢ (Presieve.ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst).EffectiveEpimorphic

Tactic:
change Nonempty _

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (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 =>
          match x with
          | ⟨a, b⟩ => Y_n a b)
        fun x =>
        match x with
        | ⟨a, b⟩ => π_n a b ≫ π a) ∈
    (coherentTopology C) X
⊢ Nonempty
    (Limits.IsColimit
      (Sieve.generate (Presieve.ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows.cocone)

Proof state:
case a
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (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
⊢ (coherentCoverage C).Saturate V
    (Sieve.pullback f
      (Sieve.generate
        (Presieve.ofArrows
          (fun x =>
            match x with
            | ⟨a, b⟩ => Y_n a b)
          fun x =>
          match x with
          | ⟨a, b⟩ => π_n a b ≫ π a)))

Tactic:
rw [← hf, Sieve.pullback_comp]

Result:
case a
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (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
⊢ (coherentCoverage C).Saturate V
    (Sieve.pullback h
      (Sieve.pullback g
        (Sieve.generate
          (Presieve.ofArrows
            (fun x =>
              match x with
              | ⟨a, b⟩ => Y_n a b)
            fun x =>
            match x with
            | ⟨a, b⟩ => π_n a b ≫ π a))))

Proof state:
case a.hS
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (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)
⊢ Presieve.ofArrows Y π ∈ (coherentCoverage C).covering X

Tactic:
use α, inferInstance, Y, π

Result:
no goals

Proof state:
case a.a.a
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (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
⊢ ∃ α_1,
    ∃ (_ : Finite α_1),
      ∃ Y_1 π_1,
        EffectiveEpiFamily Y_1 π_1 ∧
          ∀ (a : α_1),
            (Sieve.pullback g
                  (Sieve.generate
                    (Presieve.ofArrows
                      (fun x =>
                        match x with
                        | ⟨a, b⟩ => Y_n a b)
                      fun x =>
                      match x with
                      | ⟨a, b⟩ => π_n a b ≫ π a))).arrows
              (π_1 a)

Tactic:
obtain ⟨i⟩ := hY

Result:
case a.a.a.mk
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y✝ : α → C
π : (a : α) → Y✝ a ⟶ X
h✝ : EffectiveEpiFamily Y✝ π
β : α → Type
inst✝ : ∀ (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
i : α
h : V ⟶ Y✝ i
hf : h ≫ π i = f
⊢ ∃ α_1,
    ∃ (_ : Finite α_1),
      ∃ Y π_1,
        EffectiveEpiFamily Y π_1 ∧
          ∀ (a : α_1),
            (Sieve.pullback (π i)
                  (Sieve.generate
                    (Presieve.ofArrows
                      (fun x =>
                        match x with
                        | ⟨a, b⟩ => Y_n a b)
                      fun x =>
                      match x with
                      | ⟨a, b⟩ => π_n a b ≫ π a))).arrows
              (π_1 a)

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (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 =>
          match x with
          | ⟨a, b⟩ => Y_n a b)
        fun x =>
        match x with
        | ⟨a, b⟩ => π_n a b ≫ π a) ∈
    (coherentTopology C) X
⊢ ∀ (W : C),
    Presieve.IsSheafFor (yoneda.obj W)
      (Sieve.generate (Presieve.ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst)).arrows

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

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (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)
⊢ EffectiveEpiFamily (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst

Tactic:
rw [← Sieve.effectiveEpimorphic_family]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (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)
⊢ (Presieve.ofArrows (fun c => Y_n c.fst c.snd) fun c => π_n c.fst c.snd ≫ π c.fst).EffectiveEpimorphic