awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
s : Presieve.{v₁, u₁} X
inst_1 : HasPullbacks.{v₁, u₁} C
B : C
b : B ⟶ X
Z : C
v : Z ⟶ B
Y : C
u : Y ⟶ X
hu : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u ∈ s.uncurry
h :
  Eq (α := (Y : C) × (Y ⟶ B))
    ((fun (f : (Y : C) × (Y ⟶ X)) ↦
        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
            (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
          (Y : C) × (Y ⟶ B)))
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u))
    (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v)
⊢ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B)
        ((fun (f : (Y : C) × (Y ⟶ X)) ↦
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
              (Y : C) × (Y ⟶ B)))
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) =
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v) ∧
    HEq.{v₁ + 1} (α :=
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B)
          ((fun (f : (Y : C) × (Y ⟶ X)) ↦
              (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                  (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
                (Y : C) × (Y ⟶ B)))
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) ⟶
        B)
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ B)
          ((fun (f : (Y : C) × (Y ⟶ X)) ↦
              (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                  (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
                (Y : C) × (Y ⟶ B)))
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) :
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B)
            ((fun (f : (Y : C) × (Y ⟶ X)) ↦
                (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                    (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
                  (Y : C) × (Y ⟶ B)))
              (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) ⟶
          B)
      (β := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v) ⟶ B)
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ B) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v) :
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v) ⟶ B)

Tactic:
rw [Sigma.ext_iff] at h

Premises used: Sigma.ext_iff
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
s : Presieve.{v₁, u₁} X
inst_1 : HasPullbacks.{v₁, u₁} C
B : C
b : B ⟶ X
Y : C
u : Y ⟶ X
hu : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u ∈ s.uncurry
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B)
      (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B)
        ((fun (f : (Y : C) × (Y ⟶ X)) ↦
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
              (Y : C) × (Y ⟶ B)))
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)))
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ B)
        ((fun (f : (Y : C) × (Y ⟶ X)) ↦
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
              (Y : C) × (Y ⟶ B)))
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u))) ∈
    (pullbackArrows b s).uncurry

Tactic:
⟨Y, u, hu⟩

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Presieve.uncurry, Set.Mem, setOf, CategoryTheory.Limits.limit, CategoryTheory.Presieve.pullbackArrows.mk
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
s : Presieve.{v₁, u₁} X
inst_1 : HasPullbacks.{v₁, u₁} C
B : C
b : B ⟶ X
Y : C
u : Y ⟶ X
hu : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u ∈ s.uncurry
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B)
      (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B)
        ((fun (f : (Y : C) × (Y ⟶ X)) ↦
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
              (Y : C) × (Y ⟶ B)))
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)))
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ B)
        ((fun (f : (Y : C) × (Y ⟶ X)) ↦
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
              (Y : C) × (Y ⟶ B)))
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u))) ∈
    (pullbackArrows b s).uncurry

Tactic:
exact ⟨Y, u, hu⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
s : Presieve.{v₁, u₁} X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve.{v₁, u₁} Y
h :
  ∀ (Z : C) (v : Z ⟶ X),
    Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry ↔
      Membership.mem (γ := Set ((Y : C) × (Y ⟶ X)))
        (⋃ (i : (Y : C) × (Y ⟶ X)),
          ⋃ (h : i ∈ s.uncurry),
            (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
                fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) ''
              (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) h).uncurry)
        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
⊢ (s.bind t).uncurry =
    ⋃ (i : (Y : C) × (Y ⟶ X)),
      ⋃ (h : i ∈ s.uncurry),
        (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
            fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) ''
          (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) h).uncurry

Tactic:
ext ⟨Z, v⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
s : Presieve.{v₁, u₁} X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve.{v₁, u₁} Y
Z : C
v : Z ⟶ X
h :
  Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry ↔
    ∃ (i : (Y : C) × (Y ⟶ X)) (h : i ∈ s.uncurry),
      ∃ x ∈ (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) ⋯).uncurry,
        Eq (α := (Y : C) × (Y ⟶ X))
          (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
            (fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) x)
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry ↔
    Membership.mem (γ := Set ((Y : C) × (Y ⟶ X)))
      (⋃ (i : (Y : C) × (Y ⟶ X)),
        ⋃ (h : i ∈ s.uncurry),
          (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
              fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) ''
            (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) h).uncurry)
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)

Tactic:
simp only [Set.mem_iUnion, Set.mem_image]

Premises used: Set.mem_iUnion, Set.mem_image
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
s : Presieve.{v₁, u₁} X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve.{v₁, u₁} Y
Z : C
v : Z ⟶ X
h :
  Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry →
    ∃ (i : (Y : C) × (Y ⟶ X)) (h : i ∈ s.uncurry),
      ∃ x ∈ (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) ⋯).uncurry,
        Eq (α := (Y : C) × (Y ⟶ X))
          (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
            (fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) x)
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
h₁ :
  (∃ (i : (Y : C) × (Y ⟶ X)) (h : i ∈ s.uncurry),
      ∃ x ∈ (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) ⋯).uncurry,
        Eq (α := (Y : C) × (Y ⟶ X))
          (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
            (fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) x)
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)) →
    Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry ↔
    ∃ (i : (Y : C) × (Y ⟶ X)) (h : i ∈ s.uncurry),
      ∃ x ∈ (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) ⋯).uncurry,
        Eq (α := (Y : C) × (Y ⟶ X))
          (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
            (fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) x)
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
s : Presieve.{v₁, u₁} X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve.{v₁, u₁} Y
Z : C
v : Z ⟶ X
Y : C
g : Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ Y
f : Y ⟶ X
hf : s f
ht : t f hf g
hv : g ≫ f = Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
⊢ ∃ (i : (Y : C) × (Y ⟶ X)) (h : i ∈ s.uncurry),
    ∃ x ∈ (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) ⋯).uncurry,
      Eq (α := (Y : C) × (Y ⟶ X))
        (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
          (fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) x)
        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)

Tactic:
⟨⟨_, f⟩, hf, ⟨_, g⟩, ht, Sigma.ext rfl (heq_of_eq hv)⟩

Premises used: heq_of_eq, And.intro, Exists.intro, Sigma.mk, Sigma.ext, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
s : Presieve.{v₁, u₁} X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve.{v₁, u₁} Y
Z : C
v : Z ⟶ X
Y : C
g : Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ Y
f : Y ⟶ X
hf : s f
ht : t f hf g
hv : g ≫ f = Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
⊢ ∃ (i : (Y : C) × (Y ⟶ X)) (h : i ∈ s.uncurry),
    ∃ x ∈ (t (i.snd (β := fun (Y : C) ↦ Y ⟶ X)) ⋯).uncurry,
      Eq (α := (Y : C) × (Y ⟶ X))
        (Sigma.map (β₁ := fun (Z : C) ↦ Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) (β₂ := fun (Y : C) ↦ Y ⟶ X) id
          (fun (Z : C) (g : Z ⟶ i.fst (β := fun (Y : C) ↦ Y ⟶ X)) ↦ g ≫ i.snd (β := fun (Y : C) ↦ Y ⟶ X)) x)
        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)

Tactic:
exact ⟨⟨_, f⟩, hf, ⟨_, g⟩, ht, Sigma.ext rfl (heq_of_eq hv)⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
s : Presieve.{v₁, u₁} X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve.{v₁, u₁} Y
fst : C
f : fst ⟶ X
hf : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f ∈ s.uncurry
Y : C
g : Y ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)
hg :
  Sigma.mk (β := fun (Z : C) ↦ Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) Y
      g ∈
    (t (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) ⋯).uncurry
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
      (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X)
        (Sigma.map (β₁ := fun (Z : C) ↦
          Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) (β₂ := fun (Y : C) ↦
          Y ⟶ X) id
          (fun (Z : C) (g : Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) ↦
            g ≫ Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f))
          (Sigma.mk (β := fun (Z : C) ↦
            Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) Y g)))
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X)
        (Sigma.map (β₁ := fun (Z : C) ↦
          Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) (β₂ := fun (Y : C) ↦
          Y ⟶ X) id
          (fun (Z : C) (g : Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) ↦
            g ≫ Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f))
          (Sigma.mk (β := fun (Z : C) ↦
            Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) Y g))) ∈
    (s.bind t).uncurry

Tactic:
⟨_, _, _, _, hg, rfl⟩

Premises used: CategoryTheory.Presieve.uncurry, Set.Mem, setOf, CategoryTheory.Presieve.bind, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
s : Presieve.{v₁, u₁} X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve.{v₁, u₁} Y
fst : C
f : fst ⟶ X
hf : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f ∈ s.uncurry
Y : C
g : Y ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)
hg :
  Sigma.mk (β := fun (Z : C) ↦ Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) Y
      g ∈
    (t (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) ⋯).uncurry
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
      (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X)
        (Sigma.map (β₁ := fun (Z : C) ↦
          Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) (β₂ := fun (Y : C) ↦
          Y ⟶ X) id
          (fun (Z : C) (g : Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) ↦
            g ≫ Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f))
          (Sigma.mk (β := fun (Z : C) ↦
            Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) Y g)))
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X)
        (Sigma.map (β₁ := fun (Z : C) ↦
          Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) (β₂ := fun (Y : C) ↦
          Y ⟶ X) id
          (fun (Z : C) (g : Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) ↦
            g ≫ Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f))
          (Sigma.mk (β := fun (Z : C) ↦
            Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) Y g))) ∈
    (s.bind t).uncurry

Tactic:
exact ⟨_, _, _, _, hg, rfl⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
h :
  ∀ (Z : C) (v : Z ⟶ X),
    Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (ofArrows Y f).uncurry ↔
      Membership.mem (γ := Set ((Y : C) × (Y ⟶ X)))
        (Set.range fun (i : ι) ↦ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) (Y i) (f i))
        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
⊢ (ofArrows Y f).uncurry = Set.range fun (i : ι) ↦ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) (Y i) (f i)

Tactic:
ext ⟨Z, v⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
v : Z ⟶ X
h : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (ofArrows Y f).uncurry ↔ ∃ (y : ι), Y y = Z ∧ f y ≍ v
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (ofArrows Y f).uncurry ↔
    Membership.mem (γ := Set ((Y : C) × (Y ⟶ X)))
      (Set.range fun (i : ι) ↦ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) (Y i) (f i))
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)

Tactic:
simp only [Set.mem_range, Sigma.mk.injEq]

Premises used: Set.mem_range, Sigma.mk.injEq
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
v : Z ⟶ X
h : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (ofArrows Y f).uncurry → ∃ (y : ι), Y y = Z ∧ f y ≍ v
h₁ : (∃ (y : ι), Y y = Z ∧ f y ≍ v) → Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (ofArrows Y f).uncurry
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (ofArrows Y f).uncurry ↔ ∃ (y : ι), Y y = Z ∧ f y ≍ v

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y_1 : ι → C
f : (i : ι) → Y_1 i ⟶ X
Y : C
i : ι
⊢ ∃ (y : ι), Y_1 y = Y_1 i ∧ f y ≍ f i

Tactic:
⟨_, rfl, HEq.refl _⟩

Premises used: HEq.refl, And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y_1 : ι → C
f : (i : ι) → Y_1 i ⟶ X
Y : C
i : ι
⊢ ∃ (y : ι), Y_1 y = Y_1 i ∧ f y ≍ f i

Tactic:
exact ⟨_, rfl, HEq.refl _⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
v : Y i ⟶ X
h : f i ≍ v
h₁ : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) (Y i) (f i) ∈ (ofArrows Y f).uncurry
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) (Y i) v ∈ (ofArrows Y f).uncurry

Tactic:
rw [← eq_of_heq h]

Premises used: eq_of_heq
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
v : Y i ⟶ X
h : f i ≍ v
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) (Y i) (f i) ∈ (ofArrows Y f).uncurry

Tactic:
⟨i⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Presieve.uncurry, Set.Mem, setOf
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
v : Y i ⟶ X
h : f i ≍ v
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) (Y i) (f i) ∈ (ofArrows Y f).uncurry

Tactic:
exact ⟨i⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
⊢ ofArrows X f =
    ofArrows (fun (i : (↑(ofArrows X f).uncurry : Type (max u₁ v₁))) ↦ X (ofArrows.idx ⋯))
      fun (i : (↑(ofArrows X f).uncurry : Type (max u₁ v₁))) ↦ f (ofArrows.idx ⋯)

Tactic:
le_antisymm (fun Z g hg ↦ ?_) fun Z g ⟨i⟩ ↦ .mk _

Premises used: CategoryTheory.Presieve.ofArrows.mk, _private.0.CategoryTheory.Presieve.ofArrows_eq_ofArrows_uncurry.match_1, le_antisymm, CategoryTheory.Presieve.ofArrows.idx, CategoryTheory.Presieve.ofArrows, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
refine :
  ∀ (Z : C) (g : Z ⟶ S) (hg : ofArrows X f g),
    ofArrows (fun (i : (↑(ofArrows X f).uncurry : Type (max u₁ v₁))) ↦ X (ofArrows.idx ⋯))
      (fun (i : (↑(ofArrows X f).uncurry : Type (max u₁ v₁))) ↦ f (ofArrows.idx ⋯)) g
⊢ ofArrows X f =
    ofArrows (fun (i : (↑(ofArrows X f).uncurry : Type (max u₁ v₁))) ↦ X (ofArrows.idx ⋯))
      fun (i : (↑(ofArrows X f).uncurry : Type (max u₁ v₁))) ↦ f (ofArrows.idx ⋯)

Tactic:
refine le_antisymm (fun Z g hg ↦ ?_) fun Z g ⟨i⟩ ↦ .mk _

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Z : C
g : Z ⟶ S
hg : ofArrows X f g
⊢ Z =
    X
      (ofArrows.idx.{v₁, u₁, u_1} (C := C) (S := S) (X := X) (f := f) (Y :=
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ S)
          (↑(Subtype.mk (p := fun (x : (Y : C) × (Y ⟶ S)) ↦ x ∈ (ofArrows X f).uncurry)
                (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ S) Z g) hg) :
            (Y : C) × (Y ⟶ S)))
        (g :=
        Sigma.snd (β := fun (Y : C) ↦ Y ⟶ S)
          (↑(Subtype.mk (p := fun (x : (Y : C) × (Y ⟶ S)) ↦ x ∈ (ofArrows X f).uncurry)
                (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ S) Z g) hg) :
            (Y : C) × (Y ⟶ S)))
        ⋯)

Tactic:
simp [ofArrows.obj_idx]

Premises used: CategoryTheory.Presieve.ofArrows.obj_idx
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Z : C
g : Z ⟶ S
hg : ofArrows X f g
⊢ g =
    CategoryStruct.comp (Y :=
      X
        (ofArrows.idx.{v₁, u₁, u_1} (C := C) (S := S) (X := X) (f := f) (Y :=
          Sigma.fst (β := fun (Y : C) ↦ Y ⟶ S)
            (↑(Subtype.mk (p := fun (x : (Y : C) × (Y ⟶ S)) ↦ x ∈ (ofArrows X f).uncurry)
                  (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ S) Z g) hg) :
              (Y : C) × (Y ⟶ S)))
          (g :=
          Sigma.snd (β := fun (Y : C) ↦ Y ⟶ S)
            (↑(Subtype.mk (p := fun (x : (Y : C) × (Y ⟶ S)) ↦ x ∈ (ofArrows X f).uncurry)
                  (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ S) Z g) hg) :
              (Y : C) × (Y ⟶ S)))
          ⋯))
      (eqToHom ⋯)
      (f
        (ofArrows.idx.{v₁, u₁, u_1} (C := C) (S := S) (X := X) (f := f) (Y :=
          Sigma.fst (β := fun (Y : C) ↦ Y ⟶ S)
            (↑(Subtype.mk (p := fun (x : (Y : C) × (Y ⟶ S)) ↦ x ∈ (ofArrows X f).uncurry)
                  (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ S) Z g) hg) :
              (Y : C) × (Y ⟶ S)))
          (g :=
          Sigma.snd (β := fun (Y : C) ↦ Y ⟶ S)
            (↑(Subtype.mk (p := fun (x : (Y : C) × (Y ⟶ S)) ↦ x ∈ (ofArrows X f).uncurry)
                  (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ S) Z g) hg) :
              (Y : C) × (Y ⟶ S)))
          ⋯))

Tactic:
simp [ofArrows.hom_idx]

Premises used: CategoryTheory.Presieve.ofArrows.hom_idx
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Z : C
g : Z ⟶ S
hg : ofArrows X f g
⊢ ofArrows (fun (i : (↑(ofArrows X f).uncurry : Type (max u₁ v₁))) ↦ X (ofArrows.idx ⋯))
    (fun (i : (↑(ofArrows X f).uncurry : Type (max u₁ v₁))) ↦ f (ofArrows.idx ⋯)) g

Tactic:
exact .mk' ⟨⟨_, _⟩, hg⟩ (by simp [ofArrows.obj_idx]) (by simp [ofArrows.hom_idx])
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
arrows : Presieve.{v₁, u₁} X
downward_closed : ∀ {Y Z : C} {f : Y ⟶ X}, arrows f → ∀ (g : Z ⟶ Y), arrows (g ≫ f)
downward_closed_1 :
  ∀ {Y Z : C} {f : Y ⟶ X},
    { arrows := arrows, downward_closed := @downward_closed : Sieve.{v₁, u₁} X }.arrows f →
      ∀ (g : Z ⟶ Y), { arrows := arrows, downward_closed := @downward_closed : Sieve.{v₁, u₁} X }.arrows (g ≫ f)
⊢ { arrows := arrows, downward_closed := @downward_closed : Sieve.{v₁, u₁} X } =
    { arrows := { arrows := arrows, downward_closed := @downward_closed }.arrows,
      downward_closed := @downward_closed_1 }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R S : Sieve.{v₁, u₁} X
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), R.arrows f ↔ S.arrows f
⊢ R = S

Tactic:
arrows_ext <| funext fun _ => funext fun f => propext <| h f

Premises used: CategoryTheory.Sieve.arrows_ext, funext, propext
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f_1 : Y ⟶ X
S R : Sieve.{v₁, u₁} X
𝒮 : Set (Sieve.{v₁, u₁} X)
x x_1 : C
f : x ⟶ X
hf : ∃ S ∈ 𝒮, S.arrows f
x_2 : x_1 ⟶ x
obtain : ∀ (S : Sieve.{v₁, u₁} X) (hS : S ∈ 𝒮) (hf : S.arrows f), ∃ S ∈ 𝒮, S.arrows (x_2 ≫ f)
⊢ ∃ S ∈ 𝒮, S.arrows (x_2 ≫ f)

Tactic:
obtain ⟨S, hS, hf⟩ := hf
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f_1 : Y ⟶ X
S_1 R : Sieve.{v₁, u₁} X
𝒮 : Set (Sieve.{v₁, u₁} X)
x x_1 : C
f : x ⟶ X
x_2 : x_1 ⟶ x
S : Sieve.{v₁, u₁} X
hS : S ∈ 𝒮
hf : S.arrows f
⊢ ∃ S ∈ 𝒮, S.arrows (x_2 ≫ f)

Tactic:
⟨S, hS, S.downward_closed hf _⟩

Premises used: CategoryTheory.Sieve.downward_closed, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f_1 : Y ⟶ X
S_1 R : Sieve.{v₁, u₁} X
𝒮 : Set (Sieve.{v₁, u₁} X)
x x_1 : C
f : x ⟶ X
x_2 : x_1 ⟶ x
S : Sieve.{v₁, u₁} X
hS : S ∈ 𝒮
hf : S.arrows f
⊢ ∃ S ∈ 𝒮, S.arrows (x_2 ≫ f)

Tactic:
exact ⟨S, hS, S.downward_closed hf _⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f : Y ⟶ X
S_1 R_1 S R : Sieve.{v₁, u₁} X
Y_1 Z_1 : C
f_1 : Y_1 ⟶ X
h : S.arrows f_1
g : Z_1 ⟶ Y_1
⊢ S.arrows (g ≫ f_1) ∨ R.arrows (g ≫ f_1)

Tactic:
simp [h]