awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves (goal)
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
have refine_1 : (fun (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)) ↦ x.IsAmalgamation (R := Presieve.ofArrows Y π) t) t
Tactic: refine ⟨t, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves (goal)
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
⊢ ∃! t : Functor.obj (Functor.obj yoneda W) (Opposite.op X), x.IsAmalgamation (R := Presieve.ofArrows Y π) t
have 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
Tactic: refine ⟨t, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves (goal)
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
⊢ (fun (t : Functor.obj (Functor.obj yoneda W) (Opposite.op X)) ↦ x.IsAmalgamation (R := Presieve.ofArrows Y π) t) t
have h : x =
  Presieve.FamilyOfElements.restrict (R₁ := Presieve.ofArrows Y π) (R₂ :=
    (Sieve.generate (Presieve.ofArrows Y π)).arrows) sorry x_ext
Tactic: convert!
    Presieve.isAmalgamation_restrict (Sieve.le_generate (Presieve.ofArrows Y π)) _ _ t_amalg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
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)
⊢ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X
have h : Presieve.ofArrows Y π ≤ S.arrows
Tactic: apply (coherentCoverage C).mem_toGrothendieck_sieves_of_superset (R := Presieve.ofArrows Y π)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
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
⊢ S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) X
have hR : Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
  (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) (Presieve.ofArrows Y π)
Tactic: apply (coherentCoverage C).mem_toGrothendieck_sieves_of_superset (R := Presieve.ofArrows Y π)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
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
⊢ S.arrows x_1
have mk : ∀ (i : α), S.arrows (π i)
Tactic: cases h
Cleared hypotheses: x, x_1, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
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)
⊢ 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))
have 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)))
Tactic: rw [← Sieve.effectiveEpimorphic_family]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
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
⊢ 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)))))))
have 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)))))
Tactic: rw [← Sieve.forallYonedaIsSheaf_iff_colimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
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)
⊢ 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)))
have 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
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₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
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)
⊢ 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
have a : Coverage.Saturate (coherentCoverage C) X (Sieve.generate (Presieve.ofArrows Y π))
Tactic: apply Coverage.Saturate.transitive X (Sieve.generate (Presieve.ofArrows Y π))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
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 π))
⊢ 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
have 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)))
Tactic: apply Coverage.Saturate.transitive X (Sieve.generate (Presieve.ofArrows Y π))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
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)
⊢ Coverage.Saturate (coherentCoverage C) X (Sieve.generate (Presieve.ofArrows Y π))
have a : Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
  (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) (Presieve.ofArrows Y π)
Tactic: apply Coverage.Saturate.of
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
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
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
    (Precoverage.coverings (Coverage.toPrecoverage (coherentCoverage C)) X) (Presieve.ofArrows Y π)
have h₁ : Presieve.ofArrows Y π = Presieve.ofArrows Y π ∧ EffectiveEpiFamily Y π
Tactic: use α, inferInstance, Y, π
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
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
⊢ (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)))
have 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)))
Tactic: ⟨Y₁, h, g, ⟨hY, hf⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
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
⊢ 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)))
have 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: rw [← hf, Sieve.pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
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
⊢ 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))))
have 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 C).pullback_stable'
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology (goal)
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
⊢ 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)))
have 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: apply coherentTopology.mem_sieves_of_hasEffectiveEpiFamily