awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
h₂ :
  Sieve.generate
      (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
        match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
        | PUnit.unit => π' ≫ π) ∈
    (regularTopology C : (a : C) → Set (Sieve a)) X
⊢ ∀ (W : C),
    Presieve.IsSheafFor.{v_1, v_1, u_1} (X := X) (Functor.obj yoneda W)
      (Sieve.arrows
        (Sieve.generate
          (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
            match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
            | PUnit.unit => π' ≫ π)))

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

Premises used: Quiver.Hom, CategoryTheory.regularTopology.isSheaf_yoneda_obj, CategoryTheory.effectiveEpiFamilyStructSingletonOfEffectiveEpi.match_1, CategoryTheory.CategoryStruct.comp, CategoryTheory.Sieve.generate, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
suffices :
  Sieve.generate
      (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
        match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
        | PUnit.unit => π' ≫ π) ∈
    (regularTopology C : (a : C) → Set (Sieve a)) X
⊢ Presieve.EffectiveEpimorphic.{v_1, u_1} (C := C) (X := X)
    (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
      | PUnit.unit => π' ≫ π)

Tactic:
suffices h₂ : (Sieve.generate (Presieve.ofArrows _ _)) ∈ (regularTopology C) X by
    change Nonempty _
    rw [← Sieve.forallYonedaIsSheaf_iff_colimit]
    exact fun W => regularTopology.isSheaf_yoneda_obj W _ h₂
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
a :
  Coverage.Saturate.{v_1, u_1} (regularCoverage C) X
    (Sieve.generate
      (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
        match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
        | PUnit.unit => π))
a₁ :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
    Sieve.arrows
        (Sieve.generate
          (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
            match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
            | PUnit.unit => π))
        f →
      Coverage.Saturate (regularCoverage C) Y_1
        (Sieve.pullback f
          (Sieve.generate
            (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
              match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
              | PUnit.unit => π' ≫ π)))
⊢ Sieve.generate
      (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
        match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
        | PUnit.unit => π' ≫ π) ∈
    (regularTopology C : (a : C) → Set (Sieve a)) X

Tactic:
apply Coverage.Saturate.transitive X (Sieve.generate (Presieve.ofArrows (fun () ↦ Y)
      (fun () ↦ π)))

Premises used: CategoryTheory.Coverage.Saturate.transitive, CategoryTheory.Sieve.generate, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
a :
  Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
    (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) X)
    (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => π)
⊢ Coverage.Saturate.{v_1, u_1} (regularCoverage C) X
    (Sieve.generate
      (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
        match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
        | PUnit.unit => π))

Tactic:
apply Coverage.Saturate.of

Premises used: CategoryTheory.Coverage.Saturate.of
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
w : C
w₁ : Y ⟶ X
h :
  Eq (α := Presieve.{v_1, u_1} X)
      (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
        match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
        | PUnit.unit => π)
      (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ π) ∧
    EffectiveEpi π
⊢ Membership.mem (γ := Set (Presieve.{v_1, u_1} X))
    (Precoverage.coverings (Coverage.toPrecoverage (regularCoverage C)) X)
    (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => π)

Tactic:
use Y, π
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
V : C
f : V ⟶ X
a :
  ∀ (Y₁ : C) (h : V ⟶ Y₁) (g : Y₁ ⟶ X)
    (hY :
      Presieve.ofArrows (fun (x : Unit) ↦ Y)
        (fun (x : Unit) ↦
          match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
          | PUnit.unit => π)
        g)
    (hf : h ≫ g = f),
    Coverage.Saturate (regularCoverage C) V
      (Sieve.pullback f
        (Sieve.generate
          (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
            match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
            | PUnit.unit => π' ≫ π)))
⊢ Sieve.arrows
      (Sieve.generate
        (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
          match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
          | PUnit.unit => π))
      f →
    Coverage.Saturate (regularCoverage C) V
      (Sieve.pullback f
        (Sieve.generate
          (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
            match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
            | PUnit.unit => π' ≫ π)))

Tactic:
⟨Y₁, h, g, ⟨hY, hf⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY :
  Presieve.ofArrows (fun (x : Unit) ↦ Y)
    (fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => π)
    g
hf : h ≫ g = f
a :
  Coverage.Saturate (regularCoverage C) V
    (Sieve.pullback h
      (Sieve.pullback g
        (Sieve.generate
          (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
            match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
            | PUnit.unit => π' ≫ π))))
⊢ Coverage.Saturate (regularCoverage C) V
    (Sieve.pullback f
      (Sieve.generate
        (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
          match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
          | PUnit.unit => π' ≫ π)))

Tactic:
rw [← hf, Sieve.pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_comp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY :
  Presieve.ofArrows (fun (x : Unit) ↦ Y)
    (fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => π)
    g
hf : h ≫ g = f
a :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} Y₁)) (GrothendieckTopology.sieves (regularTopology C) Y₁)
    (Sieve.pullback g
      (Sieve.generate
        (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
          match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
          | PUnit.unit => π' ≫ π)))
⊢ Coverage.Saturate (regularCoverage C) V
    (Sieve.pullback h
      (Sieve.pullback g
        (Sieve.generate
          (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
            match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
            | PUnit.unit => π' ≫ π))))

Tactic:
apply (regularTopology C).pullback_stable'

Premises used: CategoryTheory.GrothendieckTopology.pullback_stable', CategoryTheory.regularTopology
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY :
  Presieve.ofArrows (fun (x : Unit) ↦ Y)
    (fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => π)
    g
hf : h ≫ g = f
a :
  ∃ (Y_1 : C) (π_1 : Y_1 ⟶ Y₁),
    EffectiveEpi π_1 ∧
      (Sieve.pullback g
            (Sieve.generate
              (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
                match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
                | PUnit.unit => π' ≫ π))).arrows
        π_1
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} Y₁)) (GrothendieckTopology.sieves (regularTopology C) Y₁)
    (Sieve.pullback g
      (Sieve.generate
        (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
          match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
          | PUnit.unit => π' ≫ π)))

Tactic:
apply regularTopology.mem_sieves_of_hasEffectiveEpi

Premises used: CategoryTheory.regularTopology.mem_sieves_of_hasEffectiveEpi
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY :
  Presieve.ofArrows (fun (x : Unit) ↦ Y)
    (fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => π)
    g
hf : h ≫ g = f
a :
  ∀ (i : Unit) (h : V ⟶ Y)
    (hf :
      (h ≫
          match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) i with
          | PUnit.unit => π) =
        f),
    ∃ (Y_1 : C) (π_1 : Y_1 ⟶ Y),
      EffectiveEpi π_1 ∧
        Sieve.arrows
          (Sieve.pullback (X := X)
            (match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) i with
            | PUnit.unit => π)
            (Sieve.generate
              (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
                match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
                | PUnit.unit => π' ≫ π)))
          π_1
⊢ ∃ (Y_1 : C) (π_1 : Y_1 ⟶ Y₁),
    EffectiveEpi π_1 ∧
      (Sieve.pullback g
            (Sieve.generate
              (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
                match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
                | PUnit.unit => π' ≫ π))).arrows
        π_1

Tactic:
cases hY
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
V : C
f : V ⟶ X
i : Unit
h : V ⟶ Y
hf :
  (h ≫
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) i with
      | PUnit.unit => π) =
    f
⊢ 𝟙 Y' ≫ π' ≫ π =
    π' ≫
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) i with
      | PUnit.unit => π

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X Y Y' : C
π : Y ⟶ X
inst_2 : EffectiveEpi π
π' : Y' ⟶ Y
inst_3 : EffectiveEpi π'
V : C
f : V ⟶ X
i : Unit
h : V ⟶ Y
hf :
  (h ≫
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) i with
      | PUnit.unit => π) =
    f
⊢ ∃ (Y_1 : C) (π_1 : Y_1 ⟶ Y),
    EffectiveEpi π_1 ∧
      Sieve.arrows
        (Sieve.pullback (X := X)
          (match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) i with
          | PUnit.unit => π)
          (Sieve.generate
            (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦
              match (motive := (x : Unit) → (fun (x : Unit) ↦ Y') x ⟶ X) x with
              | PUnit.unit => π' ≫ π)))
        π_1

Tactic:
exact ⟨Y', π', inferInstance, Y', (𝟙 _), π' ≫ π, Presieve.ofArrows.mk (), (by simp)⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
mp : S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X → ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π
mpr : (∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π) → S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X
⊢ S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X ↔ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{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 (regularCoverage C)) Y) T
mp :
  ∀ (Y' : C) (π : Y' ⟶ Y) (h' : (T = Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦ π) ∧ EffectiveEpi π),
    ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ (Sieve.generate T).arrows π
⊢ ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ (Sieve.generate T).arrows π

Tactic:
rcases hS with ⟨Y', π, h'⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
Y : C
T : Presieve.{v_1, u_1} Y
Y' : C
π : Y' ⟶ Y
h' : (T = Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦ π) ∧ EffectiveEpi π
⊢ ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ (Sieve.generate T).arrows π

Tactic:
⟨Y', π, h'.2, ?_⟩

Premises used: And.right, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
Y : C
T : Presieve.{v_1, u_1} Y
Y' : C
π : Y' ⟶ Y
h' : (T = Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦ π) ∧ EffectiveEpi π
mp : (Sieve.generate T).arrows π
⊢ ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ (Sieve.generate T).arrows π

Tactic:
refine ⟨Y', π, h'.2, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
Y : C
T : Presieve.{v_1, u_1} Y
Y' : C
π : Y' ⟶ Y
h' : (T = Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦ π) ∧ EffectiveEpi π
mp : EffectiveEpi π → Sieve.arrows (Sieve.generate (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦ π)) π
⊢ (Sieve.generate T).arrows π

Tactic:
rcases h' with ⟨rfl, _⟩

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
Y Y' : C
π : Y' ⟶ Y
right : EffectiveEpi π
⊢ 𝟙 Y' ≫ π = π

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
Y Y' : C
π : Y' ⟶ Y
right : EffectiveEpi π
⊢ Sieve.arrows (Sieve.generate (Presieve.ofArrows (fun (x : Unit) ↦ Y') fun (x : Unit) ↦ π)) π

Tactic:
exact ⟨Y', 𝟙 Y', π, Presieve.ofArrows.mk (), (by simp)⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
Y : C
⊢ Sieve.arrows.{v_1, u_1} ⊤ (𝟙 Y)

Tactic:
simp only [Sieve.top_apply]

Premises used: CategoryTheory.Sieve.top_apply
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
Y : C
⊢ ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ Sieve.arrows ⊤ π

Tactic:
exact ⟨Y, (𝟙 Y), inferInstance, by simp only [Sieve.top_apply]⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{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 (regularCoverage C) Y R
h_1 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (regularCoverage C) Y_1 (Sieve.pullback f S)
a : ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ R.arrows π
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ (Y_2 : C) (π : Y_2 ⟶ Y_1), EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
mp :
  ∀ (Y₁ : C) (π : Y₁ ⟶ Y) (h₁ : EffectiveEpi π) (h₂ : R.arrows π),
    ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ S.arrows π
⊢ ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ S.arrows π

Tactic:
rcases a with ⟨Y₁, π, ⟨h₁, h₂⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{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 (regularCoverage C) Y R
h_1 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (regularCoverage C) Y_1 (Sieve.pullback f S)
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ (Y_2 : C) (π : Y_2 ⟶ Y_1), EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
Y₁ : C
π : Y₁ ⟶ Y
h₁ : EffectiveEpi π
h₂ : R.arrows π
mp :
  ∀ (Y' : C) (π' : Y' ⟶ Y₁),
    EffectiveEpi π' → ∀ (H : (Sieve.pullback π S).arrows π'), ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ S.arrows π
⊢ ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ S.arrows π

Tactic:
choose Y' π' _ H using b h₂
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{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 (regularCoverage C) Y R
h_1 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (regularCoverage C) Y_1 (Sieve.pullback f S)
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ (Y_2 : C) (π : Y_2 ⟶ Y_1), EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
Y₁ : C
π : Y₁ ⟶ Y
h₁ : EffectiveEpi π
h₂ : R.arrows π
Y' : C
π' : Y' ⟶ Y₁
h_2 : EffectiveEpi π'
H : (Sieve.pullback π S).arrows π'
⊢ S.arrows (π' ≫ π)

Tactic:
simpa using H
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{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 (regularCoverage C) Y R
h_1 : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (regularCoverage C) Y_1 (Sieve.pullback f S)
b : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → ∃ (Y_2 : C) (π : Y_2 ⟶ Y_1), EffectiveEpi π ∧ (Sieve.pullback f S).arrows π
Y₁ : C
π : Y₁ ⟶ Y
h₁ : EffectiveEpi π
h₂ : R.arrows π
Y' : C
π' : Y' ⟶ Y₁
h_2 : EffectiveEpi π'
H : (Sieve.pullback π S).arrows π'
⊢ ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ S.arrows π

Tactic:
exact ⟨Y', π' ≫ π, inferInstance, (by simpa using H)⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
h : S ∈ (regularTopology 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 (regularCoverage C)) Y) T),
    ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ (Sieve.generate T).arrows π
mp₁ : ∀ (Y : C), ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ Sieve.arrows ⊤ π
mp₂ :
  ∀ (Y : C) (R S : Sieve.{v_1, u_1} Y),
    Coverage.Saturate (regularCoverage C) Y R →
      (∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → Coverage.Saturate (regularCoverage C) Y_1 (Sieve.pullback f S)) →
        ∀ (a : ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ R.arrows π)
          (b :
            ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
              R.arrows f → ∃ (Y_2 : C) (π : Y_2 ⟶ Y_1), EffectiveEpi π ∧ (Sieve.pullback f S).arrows π),
          ∃ (Y_1 : C) (π : Y_1 ⟶ Y), EffectiveEpi π ∧ S.arrows π
⊢ ∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π

Tactic:
induction h with
    | of Y T hS =>
      rcases hS with ⟨Y', π, h'⟩
      refine ⟨Y', π, h'.2, ?_⟩
      rcases h' with ⟨rfl, _⟩
      exact ⟨Y', 𝟙 Y', π, Presieve.ofArrows.mk (), (by simp)⟩
    | top Y => exact ⟨Y, (𝟙 Y), inferInstance, by simp only [Sieve.top_apply]⟩
    | transitive Y R S _ _ a b =>
      rcases a with ⟨Y₁, π, ⟨h₁, h₂⟩⟩
      choose Y' π' _ H using b h₂
      exact ⟨Y', π' ≫ π, inferInstance, (by simpa using H)⟩

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
⊢ (∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π) → S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X

Tactic:
regularTopology.mem_sieves_of_hasEffectiveEpi S

Premises used: CategoryTheory.regularTopology.mem_sieves_of_hasEffectiveEpi
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
X : C
S : Sieve.{v_1, u_1} X
⊢ (∃ (Y : C) (π : Y ⟶ X), EffectiveEpi π ∧ S.arrows π) → S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X

Tactic:
exact regularTopology.mem_sieves_of_hasEffectiveEpi S

Premises used: CategoryTheory.regularTopology.mem_sieves_of_hasEffectiveEpi
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X)
⊢ Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)

Tactic:
have := hF n
-- Module: Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preregular.{v, u} C
inst_2 : FinitaryExtensive.{v, u} C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X)
this : Sheaf.IsLocallySurjective (FA := TypeCat.Fun) (F.map (homOfLE ⋯).op)
⊢ ∀ (X : C)
    (y : ToType (FC := TypeCat.Fun) ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X))),
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x :
      ToType (FC := TypeCat.Fun) ((F.obj (op n.succ)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))),
      Eq (α := (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.map (homOfLE ⋯).op).hom.app (op X')) :
              (a : (F.obj (op n.succ)).obj.obj (op X')) → (F.obj (op n)).obj.obj (op X'))
            x :
          (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).map (op φ)) :
              (a : (F.obj (op n)).obj.obj (op X)) → (F.obj (op n)).obj.obj (op X'))
            y :
          (F.obj (op n)).obj (P := Presheaf.IsSheaf (coherentTopology C)).obj (op X'))

Tactic:
rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff] at this

Premises used: CategoryTheory.regularTopology.isLocallySurjective_iff, CategoryTheory.coherentTopology.isLocallySurjective_iff