-- 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:
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))))

Tactic:
apply (coherentTopology C).pullback_stable'

Result:
case 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
⊢ 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)) ∈
    (coherentTopology C).sieves Y₁

Proof state:
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)

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⟩⟩

Result:
no goals

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)
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
    (Sieve.generate (Presieve.ofArrows Y π)).arrows f →
      (coherentCoverage C).Saturate Y_1
        (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:
intro V f ⟨Y₁, h, g, ⟨hY, hf⟩⟩

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 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)))