awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ J₂ : GrothendieckTopology.{v, u} C
c : (X : C) → ClosureOperator (Sieve.{v, u} X)
hc :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve.{v, u} X),
    (c Y : (a : Sieve Y) → Sieve Y) (Sieve.pullback f S) = Sieve.pullback f ((c X : (a : Sieve X) → Sieve X) S)
X : C
S : Sieve.{v, u} X
hS : Eq (α := Sieve.{v, u} X) ((c X : (a : Sieve X) → Sieve X) S : Sieve.{v, u} X) (⊤ : Sieve.{v, u} X)
R : Sieve.{v, u} X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v, u} Y))
        {S : Sieve.{v, u} Y |
          Eq (α := Sieve.{v, u} Y) ((c Y : (a : Sieve Y) → Sieve Y) S : Sieve.{v, u} Y) (⊤ : Sieve.{v, u} Y)}
        (Sieve.pullback f R)
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Eq (α := Sieve.{v, u} Y) ((c Y : (a : Sieve Y) → Sieve Y) (Sieve.pullback f R) : Sieve.{v, u} Y) (⊤ : Sieve.{v, u} Y)

Tactic:
apply hR hf
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
h :
  ∀ (X : C) (S : Sieve.{v, u} X),
    S ∈ (topologyOfClosureOperator J₁.closureOperator ⋯ : (a : C) → Set (Sieve a)) X ↔
      S ∈ (J₁ : (a : C) → Set (Sieve a)) X
⊢ topologyOfClosureOperator J₁.closureOperator ⋯ = J₁

Tactic:
ext X S
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
J₁ : GrothendieckTopology.{v, u} C
X : C
S : Sieve.{v, u} X
⊢ S ∈ (topologyOfClosureOperator J₁.closureOperator ⋯ : (a : C) → Set (Sieve a)) X ↔
    S ∈ (J₁ : (a : C) → Set (Sieve a)) X

Tactic:
apply GrothendieckTopology.close_eq_top_iff_mem

Premises used: CategoryTheory.GrothendieckTopology.close_eq_top_iff_mem
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
c : (X : C) → ClosureOperator (Sieve.{v, u} X)
pb :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve.{v, u} X),
    (c Y : (a : Sieve Y) → Sieve Y) (Sieve.pullback f S) = Sieve.pullback f ((c X : (a : Sieve X) → Sieve X) S)
X : C
S : Sieve.{v, u} X
h :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    ((topologyOfClosureOperator c pb).close S).arrows f ↔ Sieve.arrows ((c X : (a : Sieve X) → Sieve X) S) f
⊢ (topologyOfClosureOperator c pb).close S = (c X : (a : Sieve X) → Sieve X) S

Tactic:
ext Y f
-- Module: Mathlib.CategoryTheory.Sites.Closed
Goal:
C : Type u
inst : Category.{v, u} C
c : (X : C) → ClosureOperator (Sieve.{v, u} X)
pb :
  ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve.{v, u} X),
    (c Y : (a : Sieve Y) → Sieve Y) (Sieve.pullback f S) = Sieve.pullback f ((c X : (a : Sieve X) → Sieve X) S)
X : C
S : Sieve.{v, u} X
Y : C
f : Y ⟶ X
h : Sieve.pullback f ((c X : (a : Sieve X) → Sieve X) S) = ⊤ ↔ Sieve.arrows ((c X : (a : Sieve X) → Sieve X) S) f
h₁ h₂ :
  Sieve.pullback f ((c X : (a : Sieve X) → Sieve X) S) = ⊤ ↔ Sieve.pullback f ((c X : (a : Sieve X) → Sieve X) S) = ⊤
⊢ Eq (α := Sieve.{v, u} Y) ((c Y : (a : Sieve Y) → Sieve Y) (Sieve.pullback f S) : Sieve.{v, u} Y)
      (⊤ : Sieve.{v, u} Y) ↔
    Sieve.arrows ((c X : (a : Sieve X) → Sieve X) S) f

Tactic:
rw [pb, Sieve.mem_iff_pullback_eq_top]

Premises used: CategoryTheory.Sieve.mem_iff_pullback_eq_top
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
obtain :
  ∀ (β : Type),
    Finite β →
      ∀ (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ B₂) (h : EffectiveEpiFamily X₂ π₂) (i : β → α)
        (ι : (b : β) → X₂ b ⟶ X₁ (i b)) (hh : ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f),
        ∃ (T : Presieve.{v_1, u_1} B₂),
          Membership.mem (γ := Set (Presieve.{v_1, u_1} B₂))
              {S : Presieve.{v_1, u_1} B₂ |
                ∃ (α : Type) (_ : Finite α) (X : α → C) (π : (a : α) → X a ⟶ B₂),
                  S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π}
              T ∧
            T.FactorsThruAlong (Presieve.ofArrows X₁ π₁) f
⊢ ∃ (T : Presieve.{v_1, u_1} B₂),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} B₂))
        {S : Presieve.{v_1, u_1} B₂ |
          ∃ (α : Type) (_ : Finite α) (X : α → C) (π : (a : α) → X a ⟶ B₂),
            S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π}
        T ∧
      T.FactorsThruAlong (Presieve.ofArrows X₁ π₁) f

Tactic:
obtain ⟨β, _, X₂, π₂, h, i, ι, hh⟩ := Precoherent.pullback f α X₁ π₁ hS

Premises used: CategoryTheory.Precoherent.pullback
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
β : Type
w_1 : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ B₂
h : EffectiveEpiFamily X₂ π₂
i : β → α
ι : (b : β) → X₂ b ⟶ X₁ (i b)
hh : ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
⊢ ∃ (T : Presieve.{v_1, u_1} B₂),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} B₂))
        {S : Presieve.{v_1, u_1} B₂ |
          ∃ (α : Type) (_ : Finite α) (X : α → C) (π : (a : α) → X a ⟶ B₂),
            S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π}
        T ∧
      T.FactorsThruAlong (Presieve.ofArrows X₁ π₁) f

Tactic:
⟨Presieve.ofArrows X₂ π₂, ⟨β, inferInstance, X₂, π₂, rfl, h⟩, ?_⟩

Premises used: inferInstance, And.intro, Exists.intro, CategoryTheory.Presieve.ofArrows, rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
β : Type
w_1 : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ B₂
h : EffectiveEpiFamily X₂ π₂
i : β → α
ι : (b : β) → X₂ b ⟶ X₁ (i b)
hh : ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
refine : (Presieve.ofArrows X₂ π₂).FactorsThruAlong (Presieve.ofArrows X₁ π₁) f
⊢ ∃ (T : Presieve.{v_1, u_1} B₂),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} B₂))
        {S : Presieve.{v_1, u_1} B₂ |
          ∃ (α : Type) (_ : Finite α) (X : α → C) (π : (a : α) → X a ⟶ B₂),
            S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π}
        T ∧
      T.FactorsThruAlong (Presieve.ofArrows X₁ π₁) f

Tactic:
refine ⟨Presieve.ofArrows X₂ π₂, ⟨β, inferInstance, X₂, π₂, rfl, h⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
β : Type
w_1 : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ B₂
h : EffectiveEpiFamily X₂ π₂
i : β → α
ι : (b : β) → X₂ b ⟶ X₁ (i b)
hh : ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
Y : C
b : β
⊢ ∃ (W : C) (i : X₂ b ⟶ W) (e : W ⟶ B₁), Presieve.ofArrows X₁ π₁ e ∧ i ≫ e = π₂ b ≫ f

Tactic:
⟨(X₁ (i b)), ι _, π₁ _, ⟨_⟩, hh _⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
β : Type
w_1 : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ B₂
h : EffectiveEpiFamily X₂ π₂
i : β → α
ι : (b : β) → X₂ b ⟶ X₁ (i b)
hh : ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
Y : C
b : β
⊢ ∃ (W : C) (i : X₂ b ⟶ W) (e : W ⟶ B₁), Presieve.ofArrows X₁ π₁ e ∧ i ≫ e = π₂ b ≫ f

Tactic:
exact ⟨(X₁ (i b)), ι _, π₁ _, ⟨_⟩, hh _⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
this :
  ∀ (Z : C) (π : Z ⟶ X) (hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π) (h_epi : EffectiveEpi π),
    ∃ (T : Presieve.{v_1, u_1} Y),
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
          {S : Presieve.{v_1, u_1} Y |
            ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
          T ∧
        T.FactorsThruAlong S f
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
      {S : Presieve.{v_1, u_1} X |
        ∃ (X_1 : C) (f : X_1 ⟶ X), (S = Presieve.ofArrows (fun (x : Unit) ↦ X_1) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
      S →
    ∃ (T : Presieve.{v_1, u_1} Y),
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
          {S : Presieve.{v_1, u_1} Y |
            ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
          T ∧
        T.FactorsThruAlong S f

Tactic:
⟨Z, π, hπ, h_epi⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
⊢ ∃ (W : C) (h : W ⟶ Y) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ π = h ≫ f

Tactic:
have := Preregular.exists_fac f π
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
this : ∃ (W : C) (h : W ⟶ Y) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ π = h ≫ f
obtain :
  ∀ (W : C) (h : W ⟶ Y),
    EffectiveEpi h →
      ∀ (i : W ⟶ Z) (this : i ≫ π = h ≫ f),
        ∃ (T : Presieve.{v_1, u_1} Y),
          Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
              {S : Presieve.{v_1, u_1} Y |
                ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
              T ∧
            T.FactorsThruAlong S f
⊢ ∃ (T : Presieve.{v_1, u_1} Y),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        {S : Presieve.{v_1, u_1} Y |
          ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
        T ∧
      T.FactorsThruAlong S f

Tactic:
obtain ⟨W, h, _, i, this⟩ := this
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ ∃ (T : Presieve.{v_1, u_1} Y),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        {S : Presieve.{v_1, u_1} Y |
          ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
        T ∧
      T.FactorsThruAlong S f

Tactic:
⟨Presieve.singleton h, ⟨?_, ?_⟩⟩

Premises used: And.intro, Exists.intro, CategoryTheory.Presieve.singleton
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
refine_1 :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    {S : Presieve.{v_1, u_1} Y |
      ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
    (Presieve.singleton h)
refine_2 : (Presieve.singleton h).FactorsThruAlong S f
⊢ ∃ (T : Presieve.{v_1, u_1} Y),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        {S : Presieve.{v_1, u_1} Y |
          ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
        T ∧
      T.FactorsThruAlong S f

Tactic:
refine ⟨Presieve.singleton h, ⟨?_, ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
rw rw₁ : Presieve.singleton h = Presieve.singleton h
⊢ Presieve.singleton h = Presieve.ofArrows (fun (x : Unit) ↦ W) fun (x : Unit) ↦ h

Tactic:
rw [Presieve.ofArrows_pUnit h]

Premises used: CategoryTheory.Presieve.ofArrows_pUnit
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
this₁ this₂ : Presieve.singleton h = Presieve.singleton h
⊢ Presieve.singleton h = Presieve.ofArrows (fun (x : Unit) ↦ W) fun (x : Unit) ↦ h

Tactic:
{rw [Presieve.ofArrows_pUnit h]}

Premises used: CategoryTheory.Presieve.ofArrows_pUnit
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    {S : Presieve.{v_1, u_1} Y |
      ∃ (X : C) (f : X ⟶ Y), (S = Presieve.ofArrows (fun (x : Unit) ↦ X) fun (x : Unit) ↦ f) ∧ EffectiveEpi f}
    (Presieve.singleton h)

Tactic:
exact ⟨W, h, by {rw [Presieve.ofArrows_pUnit h]}, inferInstance⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W_1 : C
h : W_1 ⟶ Y
w : EffectiveEpi h
i : W_1 ⟶ Z
this : i ≫ π = h ≫ f
W : C
g : W ⟶ Y
hg : Presieve.singleton h g
refine_2 : ∃ (W : C) (i : W_1 ⟶ W) (e : W ⟶ X), S e ∧ i ≫ e = h ≫ f
⊢ ∃ (W_2 : C) (i : W ⟶ W_2) (e : W_2 ⟶ X), S e ∧ i ≫ e = g ≫ f

Tactic:
cases hg
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ ∃ (W_1 : C) (i : W ⟶ W_1) (e : W_1 ⟶ X), S e ∧ i ≫ e = h ≫ f

Tactic:
⟨Z, i, π, ⟨?_, this⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
refine_2 : S π
⊢ ∃ (W_1 : C) (i : W ⟶ W_1) (e : W_1 ⟶ X), S e ∧ i ≫ e = h ≫ f

Tactic:
refine ⟨Z, i, π, ⟨?_, this⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun (x : Unit) ↦ Z) fun (x : Unit) ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
refine_2 : Presieve.ofArrows (fun (x : Unit) ↦ Z) (fun (x : Unit) ↦ π) π
⊢ S π

Tactic:
cases hπ
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
Z : C
π : Z ⟶ X
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
refine_2 : Presieve.singleton π π
⊢ Presieve.ofArrows (fun (x : Unit) ↦ Z) (fun (x : Unit) ↦ π) π

Tactic:
rw [Presieve.ofArrows_pUnit]

Premises used: CategoryTheory.Presieve.ofArrows_pUnit
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
Z : C
π : Z ⟶ X
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ Presieve.singleton π π

Tactic:
Presieve.singleton.mk

Premises used: CategoryTheory.Presieve.singleton.mk
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y : C
f : Y ⟶ X
Z : C
π : Z ⟶ X
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ Presieve.singleton π π

Tactic:
exact Presieve.singleton.mk

Premises used: CategoryTheory.Presieve.singleton.mk
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
this :
  ∀ (α : Type) (hα : Finite α) (Z : α → C) (π : (a : α) → Z a ⟶ X) (hS : S = Presieve.ofArrows Z π)
    (h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)),
    ∃ (T : Presieve.{v_1, u_1} Y),
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
          {S : Presieve.{v_1, u_1} Y |
            ∃ (α : Type) (x : Finite α) (X : α → C) (π : (a : α) → X a ⟶ Y),
              S = Presieve.ofArrows X π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)}
          T ∧
        T.FactorsThruAlong S f
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
      {S : Presieve.{v_1, u_1} X |
        ∃ (α : Type) (x : Finite α) (X_1 : α → C) (π : (a : α) → X_1 a ⟶ X),
          S = Presieve.ofArrows X_1 π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X_1) (Sigma.desc π)}
      S →
    ∃ (T : Presieve.{v_1, u_1} Y),
      Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
          {S : Presieve.{v_1, u_1} Y |
            ∃ (α : Type) (x : Finite α) (X : α → C) (π : (a : α) → X a ⟶ Y),
              S = Presieve.ofArrows X π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)}
          T ∧
        T.FactorsThruAlong S f

Tactic:
⟨α, hα, Z, π, hS, h_iso⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y := fun (a : α) ↦ pullback.fst f (π a)
⊢ ∃ (T : Presieve.{v_1, u_1} Y),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        {S : Presieve.{v_1, u_1} Y |
          ∃ (α : Type) (x : Finite α) (X : α → C) (π : (a : α) → X a ⟶ Y),
            S = Presieve.ofArrows X π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)}
        T ∧
      T.FactorsThruAlong S f

Tactic:
⟨@Presieve.ofArrows C _ _ α Z' π', ⟨?_, ?_⟩⟩

Premises used: And.intro, Exists.intro, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y := fun (a : α) ↦ pullback.fst f (π a)
refine_1 :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    {S : Presieve.{v_1, u_1} Y |
      ∃ (α : Type) (x : Finite α) (X : α → C) (π : (a : α) → X a ⟶ Y),
        S = Presieve.ofArrows X π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)}
    (Presieve.ofArrows Z' π')
refine_2 : (Presieve.ofArrows Z' π').FactorsThruAlong S f
⊢ ∃ (T : Presieve.{v_1, u_1} Y),
    Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
        {S : Presieve.{v_1, u_1} Y |
          ∃ (α : Type) (x : Finite α) (X : α → C) (π : (a : α) → X a ⟶ Y),
            S = Presieve.ofArrows X π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)}
        T ∧
      T.FactorsThruAlong S f

Tactic:
refine ⟨@Presieve.ofArrows C _ _ α Z' π', ⟨?_, ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y := fun (a : α) ↦ pullback.fst f (π a)
refine_1 :
  ∃ (x : Finite α) (X : α → C) (π : (a : α) → X a ⟶ Y),
    Presieve.ofArrows Z' π' = Presieve.ofArrows X π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)
refine_1₁ : Type
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} Y))
    {S : Presieve.{v_1, u_1} Y |
      ∃ (α : Type) (x : Finite α) (X : α → C) (π : (a : α) → X a ⟶ Y),
        S = Presieve.ofArrows X π ∧ IsIso (X := sigmaObj.{0, v_1, u_1} X) (Sigma.desc π)}
    (Presieve.ofArrows Z' π')

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y := fun (a : α) ↦ pullback.fst f (π a)
⊢ Presieve.ofArrows Z' π' = Presieve.ofArrows Z' π'

Tactic:
simp only
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y := fun (a : α) ↦ pullback.fst f (π a)
W : C
g : W ⟶ Y
hg : Presieve.ofArrows Z' π' g
refine_2 : ∀ ⦃Y_1 : C⦄ (a : α), ∃ (W : C) (i : Z' a ⟶ W) (e : W ⟶ X), S e ∧ i ≫ e = π' a ≫ f
⊢ ∃ (W_1 : C) (i : W ⟶ W_1) (e : W_1 ⟶ X), S e ∧ i ≫ e = g ≫ f

Tactic:
rcases hg with ⟨a⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y_1 : C
f : Y_1 ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y_1 := fun (a : α) ↦ pullback.fst f (π a)
Y : C
a : α
rw rw₁ : Eq (α := Z' a ⟶ X) (pullback.snd f (π a) ≫ π a) (pullback.snd f (π a) ≫ π a)
⊢ pullback.snd f (π a) ≫ π a = π' a ≫ f

Tactic:
rw [CategoryTheory.Limits.pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y_1 : C
f : Y_1 ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y_1 := fun (a : α) ↦ pullback.fst f (π a)
Y : C
a : α
refine_2 : S (π a)
⊢ ∃ (W : C) (i : Z' a ⟶ W) (e : W ⟶ X), S e ∧ i ≫ e = π' a ≫ f

Tactic:
refine ⟨Z a, pullback.snd _ _, π a, ?_, by rw [CategoryTheory.Limits.pullback.condition]⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
X Y_1 : C
f : Y_1 ⟶ X
S : Presieve.{v_1, u_1} X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (X := sigmaObj.{0, v_1, u_1} Z) (Sigma.desc π)
Z' : α → C := fun (a : α) ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y_1 := fun (a : α) ↦ pullback.fst f (π a)
Y : C
a : α
refine_2 : Presieve.ofArrows Z π (π a)
⊢ S (π a)

Tactic:
rw [hS]