awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W X w Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS :
  ∃ (f_1 : w ⟶ X),
    Eq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
        (ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f_1) ∧
      EffectiveEpi f_1
this : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
h_colim :
  IsColimit (J :=
    Presieve.category.{v_1, u_1} (C := C) (X := X)
      (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
    (cocone (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
x : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx : x.Compatible (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
x_ext : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W)
  (Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f))) :=
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx_ext :
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f).Compatible (R :=
    Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)))
S : Sieve.{v_1, u_1} X :=
  Sieve.generate
    (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => f)
t : obj (obj yoneda W) (op X)
t_amalg : x_ext.IsAmalgamation (R := S.arrows) t
t_uniq :
  ∀ (y : obj (obj yoneda W) (op X)),
    (fun (t : obj (obj yoneda W) (op X)) ↦ x_ext.IsAmalgamation (R := S.arrows) t) y → y = t
⊢ (FamilyOfElements.restrict (R₁ :=
        ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
          match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
          | PUnit.unit => f)
        (R₂ :=
        Sieve.arrows
          (Sieve.generate
            (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
              match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
              | PUnit.unit => f)))
        ⋯ x_ext).IsAmalgamation
    (R :=
    ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => f)
    t

Tactic:
Presieve.isAmalgamation_restrict
      (Sieve.le_generate (Presieve.ofArrows (fun () ↦ Y) (fun () ↦ f))) _ _ t_amalg

Premises used: CategoryTheory.Sieve.le_generate, CategoryTheory.Presieve.isAmalgamation_restrict, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W X w Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS :
  ∃ (f_1 : w ⟶ X),
    Eq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
        (ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f_1) ∧
      EffectiveEpi f_1
this : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
h_colim :
  IsColimit (J :=
    Presieve.category.{v_1, u_1} (C := C) (X := X)
      (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
    (cocone (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
x : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx : x.Compatible (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
x_ext : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W)
  (Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f))) :=
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx_ext :
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f).Compatible (R :=
    Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)))
S : Sieve.{v_1, u_1} X :=
  Sieve.generate
    (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => f)
t : obj (obj yoneda W) (op X)
t_amalg : x_ext.IsAmalgamation (R := S.arrows) t
t_uniq :
  ∀ (y : obj (obj yoneda W) (op X)),
    (fun (t : obj (obj yoneda W) (op X)) ↦ x_ext.IsAmalgamation (R := S.arrows) t) y → y = t
h :
  HEq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f) (β := Presieve.{v_1, u_1} X)
      (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
        match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
        | PUnit.unit => f) →
    x =
      FamilyOfElements.restrict (R₁ :=
        ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
          match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
          | PUnit.unit => f)
        (R₂ :=
        Sieve.arrows
          (Sieve.generate
            (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
              match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
              | PUnit.unit => f)))
        ⋯ x_ext
⊢ (fun (t : obj (obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f) t) t

Tactic:
convert!
    Presieve.isAmalgamation_restrict
      (Sieve.le_generate (Presieve.ofArrows (fun () ↦ Y) (fun () ↦ f))) _ _ t_amalg

Premises used: CategoryTheory.Sieve.le_generate, CategoryTheory.Presieve.isAmalgamation_restrict, CategoryTheory.Presieve.ofArrows
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W X w Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS :
  ∃ (f_1 : w ⟶ X),
    Eq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
        (ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f_1) ∧
      EffectiveEpi f_1
this : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
h_colim :
  IsColimit (J :=
    Presieve.category.{v_1, u_1} (C := C) (X := X)
      (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
    (cocone (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
x : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx : x.Compatible (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
x_ext : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W)
  (Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f))) :=
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx_ext :
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f).Compatible (R :=
    Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)))
S : Sieve.{v_1, u_1} X :=
  Sieve.generate
    (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => f)
t : obj (obj yoneda W) (op X)
t_amalg : x_ext.IsAmalgamation (R := S.arrows) t
t_uniq :
  ∀ (y : obj (obj yoneda W) (op X)),
    (fun (t : obj (obj yoneda W) (op X)) ↦ x_ext.IsAmalgamation (R := S.arrows) t) y → y = t
e_5 :
  HEq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f) (β := Presieve.{v_1, u_1} X)
    (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => f)
⊢ x =
    FamilyOfElements.restrict (R₁ :=
      ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
        match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
        | PUnit.unit => f)
      (R₂ :=
      Sieve.arrows
        (Sieve.generate
          (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
            match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
            | PUnit.unit => f)))
      ⋯ x_ext

Tactic:
(Presieve.restrict_extend hx).symm

Premises used: CategoryTheory.Presieve.restrict_extend, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W X w Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS :
  ∃ (f_1 : w ⟶ X),
    Eq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
        (ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f_1) ∧
      EffectiveEpi f_1
this : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
h_colim :
  IsColimit (J :=
    Presieve.category.{v_1, u_1} (C := C) (X := X)
      (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
    (cocone (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
x : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx : x.Compatible (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
x_ext : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W)
  (Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f))) :=
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx_ext :
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f).Compatible (R :=
    Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)))
S : Sieve.{v_1, u_1} X :=
  Sieve.generate
    (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => f)
t : obj (obj yoneda W) (op X)
t_amalg : x_ext.IsAmalgamation (R := S.arrows) t
t_uniq :
  ∀ (y : obj (obj yoneda W) (op X)),
    (fun (t : obj (obj yoneda W) (op X)) ↦ x_ext.IsAmalgamation (R := S.arrows) t) y → y = t
e_5 :
  HEq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f) (β := Presieve.{v_1, u_1} X)
    (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => f)
⊢ x =
    FamilyOfElements.restrict (R₁ :=
      ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
        match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
        | PUnit.unit => f)
      (R₂ :=
      Sieve.arrows
        (Sieve.generate
          (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
            match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
            | PUnit.unit => f)))
      ⋯ x_ext

Tactic:
exact (Presieve.restrict_extend hx).symm

Premises used: CategoryTheory.Presieve.restrict_extend, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W X w Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS :
  ∃ (f_1 : w ⟶ X),
    Eq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
        (ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f_1) ∧
      EffectiveEpi f_1
this : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
h_colim :
  IsColimit (J :=
    Presieve.category.{v_1, u_1} (C := C) (X := X)
      (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
    (cocone (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
x : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx : x.Compatible (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
x_ext : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W)
  (Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f))) :=
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx_ext :
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f).Compatible (R :=
    Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)))
S : Sieve.{v_1, u_1} X :=
  Sieve.generate
    (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => f)
t : obj (obj yoneda W) (op X)
t_amalg : x_ext.IsAmalgamation (R := S.arrows) t
t_uniq :
  ∀ (y : obj (obj yoneda W) (op X)),
    (fun (t : obj (obj yoneda W) (op X)) ↦ x_ext.IsAmalgamation (R := S.arrows) t) y → y = t
⊢ ∀ (y : obj (obj yoneda W) (op X)),
    (fun (t : obj (obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f) t)
        y →
      y = t

Tactic:
fun y hy ↦ t_uniq y <| Presieve.isAmalgamation_sieveExtend x y hy

Premises used: CategoryTheory.Presieve.isAmalgamation_sieveExtend
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
W X w Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS :
  ∃ (f_1 : w ⟶ X),
    Eq (α := Presieve.{v_1, u_1} X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
        (ofArrows (fun (x : Unit) ↦ w) fun (x : Unit) ↦ f_1) ∧
      EffectiveEpi f_1
this : regular.{v_1, u_1} (C := C) (X := X) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
h_colim :
  IsColimit (J :=
    Presieve.category.{v_1, u_1} (C := C) (X := X)
      (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
    (cocone (Sieve.arrows (Sieve.generate (ofArrows (fun (x : PUnit.{1}) ↦ Y) fun (x : PUnit.{1}) ↦ f))))
x : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W) (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx : x.Compatible (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
x_ext : FamilyOfElements.{v_1, v_1, u_1} (X := X) (obj yoneda W)
  (Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f))) :=
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)
hx_ext :
  x.sieveExtend (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f).Compatible (R :=
    Sieve.arrows (Sieve.generate (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f)))
S : Sieve.{v_1, u_1} X :=
  Sieve.generate
    (ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦
      match (motive := (x : Unit) → (fun (x : Unit) ↦ Y) x ⟶ X) x with
      | PUnit.unit => f)
t : obj (obj yoneda W) (op X)
t_amalg : x_ext.IsAmalgamation (R := S.arrows) t
t_uniq :
  ∀ (y : obj (obj yoneda W) (op X)),
    (fun (t : obj (obj yoneda W) (op X)) ↦ x_ext.IsAmalgamation (R := S.arrows) t) y → y = t
⊢ ∀ (y : obj (obj yoneda W) (op X)),
    (fun (t : obj (obj yoneda W) (op X)) ↦ x.IsAmalgamation (R := ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ f) t)
        y →
      y = t

Tactic:
exact fun y hy ↦ t_uniq y <| Presieve.isAmalgamation_sieveExtend x y hy

Premises used: CategoryTheory.Presieve.isAmalgamation_sieveExtend
-- Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : Preregular.{v_1, u_1} C
⊢ GrothendieckTopology.Subcanonical.{v_1, u_1} (regularTopology C)

Tactic:
GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ isSheaf_yoneda_obj

Premises used: CategoryTheory.regularTopology.isSheaf_yoneda_obj, CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
-- 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
h : EffectiveEpi π ∧ S.arrows π
rw : (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ π) ≤ S.arrows
⊢ Sieve.generate (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ π) ≤ S

Tactic:
rw [Sieve.generate_le_iff (Presieve.ofArrows _ _) S]

Premises used: CategoryTheory.Sieve.generate_le_iff, 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 : C
S : Sieve.{v_1, u_1} X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
apply : Presieve.FactorsThru (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ π) S.arrows
⊢ (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ π) ≤ S.arrows

Tactic:
apply Presieve.le_of_factorsThru_sieve (Presieve.ofArrows _ _) S _

Premises used: CategoryTheory.Presieve.le_of_factorsThru_sieve, 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 : C
S : Sieve.{v_1, u_1} X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
W : C
g : W ⟶ X
f : Presieve.ofArrows (fun (x : Unit) ↦ Y) (fun (x : Unit) ↦ π) g
⊢ ∃ (W_1 : C) (i : W ⟶ W_1) (e : W_1 ⟶ X), S.arrows e ∧ i ≫ e = g

Tactic:
⟨W, 𝟙 W, ?_⟩

Premises used: CategoryTheory.CategoryStruct.id, 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
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
W : C
g : W ⟶ X
f : Presieve.ofArrows (fun (x : Unit) ↦ Y) (fun (x : Unit) ↦ π) g
refine : ∃ (e : W ⟶ X), S.arrows e ∧ 𝟙 W ≫ e = g
⊢ ∃ (W_1 : C) (i : W ⟶ W_1) (e : W_1 ⟶ X), S.arrows e ∧ i ≫ e = g

Tactic:
refine ⟨W, 𝟙 W, ?_⟩
-- 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
h : EffectiveEpi π ∧ S.arrows π
W : C
g : W ⟶ X
f : Presieve.ofArrows (fun (x : Unit) ↦ Y) (fun (x : Unit) ↦ π) g
mk : ∀ (i : Unit), ∃ (e : Y ⟶ X), S.arrows e ∧ 𝟙 Y ≫ e = π
⊢ ∃ (e : W ⟶ X), S.arrows e ∧ 𝟙 W ≫ e = g

Tactic:
cases f
-- 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
h : EffectiveEpi π ∧ S.arrows π
i : Unit
⊢ ∃ (e : Y ⟶ X), S.arrows e ∧ 𝟙 Y ≫ e = π

Tactic:
⟨π, ⟨h.2, Category.id_comp π⟩⟩

Premises used: And.right, And.intro, Exists.intro, CategoryTheory.Category.id_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 : C
S : Sieve.{v_1, u_1} X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
i : Unit
⊢ ∃ (e : Y ⟶ X), S.arrows e ∧ 𝟙 Y ≫ e = π

Tactic:
exact ⟨π, ⟨h.2, Category.id_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 : C
S : Sieve.{v_1, u_1} X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
⊢ Sieve.generate (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ π) ≤ S

Tactic:
have h_le : Sieve.generate (Presieve.ofArrows (fun () ↦ Y) (fun _ ↦ π)) ≤ S := by
    rw [Sieve.generate_le_iff (Presieve.ofArrows _ _) S]
    apply Presieve.le_of_factorsThru_sieve (Presieve.ofArrows _ _) S _
    intro W g f
    refine ⟨W, 𝟙 W, ?_⟩
    cases f
    exact ⟨π, ⟨h.2, Category.id_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 : C
S : Sieve.{v_1, u_1} X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
h_le : Sieve.generate (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ π) ≤ S
apply :
  Coverage.Saturate.{v_1, u_1} (regularCoverage C) X
    (Sieve.generate (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ π))
⊢ S ∈ (regularTopology C : (a : C) → Set (Sieve a)) X

Tactic:
apply Coverage.saturate_of_superset (regularCoverage C) h_le

Premises used: CategoryTheory.regularCoverage, CategoryTheory.Coverage.saturate_of_superset
-- 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
h : EffectiveEpi π ∧ S.arrows π
h_le : Sieve.generate (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ π) ≤ S
⊢ Coverage.Saturate.{v_1, u_1} (regularCoverage C) X
    (Sieve.generate (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ π))

Tactic:
Coverage.Saturate.of X _ ⟨Y, π, rfl, h.1⟩

Premises used: CategoryTheory.Coverage.Saturate.of, And.left, And.intro, Exists.intro, 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
h : EffectiveEpi π ∧ S.arrows π
h_le : Sieve.generate (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ π) ≤ S
⊢ Coverage.Saturate.{v_1, u_1} (regularCoverage C) X
    (Sieve.generate (Presieve.ofArrows (fun (x : Unit) ↦ Y) fun (x : Unit) ↦ π))

Tactic:
exact Coverage.Saturate.of X _ ⟨Y, π, rfl, h.1⟩
-- 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 π'
rw :
  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 => π' ≫ π)
⊢ EffectiveEpi (π' ≫ π)

Tactic:
rw [effectiveEpi_iff_effectiveEpiFamily, ← Sieve.effectiveEpimorphic_family]

Premises used: CategoryTheory.Sieve.effectiveEpimorphic_family, CategoryTheory.effectiveEpi_iff_effectiveEpiFamily
-- 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
rw :
  ∀ (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 => π' ≫ π)))
⊢ Nonempty
    (IsColimit (J :=
      Presieve.category.{v_1, u_1} (C := C) (X := 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 => π' ≫ π))))
      (Presieve.cocone
        (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:
rw [← Sieve.forallYonedaIsSheaf_iff_colimit]

Premises used: CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit
-- 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:
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