awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
X Y_1 Z_1 : C
f_1 : Y_1 ⟶ X
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
F : Functor.{v₁, v₂, u₁, u₂} C D
S : Presieve.{v₁, u₁} X
Y : D
f : Y ⟶ F.obj X
Z : C
f' : Z ⟶ X
g : Y ⟶ F.obj Z
h₁ : S f'
h : f = g ≫ F.map f'
⊢ FunctorPushforwardStructure F S f

Tactic:
exact ⟨Z, f', g, h₁, h⟩
-- 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 : C
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Presieve.{v₁, u₁} X
h :
  ∀ (x : E),
    Eq (α := (x ⟶ (F ⋙ G).obj X) → Prop) (functorPushforward (F ⋙ G) R) (functorPushforward G (functorPushforward F R))
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)

Tactic:
funext x
-- 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 : C
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Presieve.{v₁, u₁} X
x : E
h : ∀ (f : x ⟶ (F ⋙ G).obj X), functorPushforward (F ⋙ G) R f ↔ functorPushforward G (functorPushforward F R) f
⊢ Eq (α := (x ⟶ (F ⋙ G).obj X) → Prop) (functorPushforward (F ⋙ G) R) (functorPushforward G (functorPushforward F R))

Tactic:
ext f
-- 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 : C
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Presieve.{v₁, u₁} X
x : E
f : x ⟶ (F ⋙ G).obj X
h : functorPushforward (F ⋙ G) R f → functorPushforward G (functorPushforward F R) f
h₁ : functorPushforward G (functorPushforward F R) f → functorPushforward (F ⋙ G) R f
⊢ functorPushforward (F ⋙ G) R f ↔ functorPushforward G (functorPushforward F R) f

Tactic:
constructor
-- 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_1 : C
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Presieve.{v₁, u₁} X_1
x : E
X : C
f₁ : X ⟶ X_1
g₁ : x ⟶ (F ⋙ G).obj X
h₁ : R f₁
⊢ F.map f₁ = 𝟙 (F.obj X) ≫ F.map f₁

Tactic:
simp
-- 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_1 : C
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Presieve.{v₁, u₁} X_1
x : E
X : C
f₁ : X ⟶ X_1
g₁ : x ⟶ (F ⋙ G).obj X
h₁ : R f₁
⊢ functorPushforward G (functorPushforward F R) (g₁ ≫ (F ⋙ G).map f₁)

Tactic:
exact ⟨F.obj X, F.map f₁, g₁, ⟨X, f₁, 𝟙 _, h₁, by simp⟩, rfl⟩
-- 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_1 : C
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Presieve.{v₁, u₁} X_1
x : E
X : D
g₁ : x ⟶ G.obj X
X' : C
f₂ : X' ⟶ X_1
g₂ : X ⟶ F.obj X'
h₁ : R f₂
⊢ g₁ ≫ G.map (g₂ ≫ F.map f₂) = (g₁ ≫ G.map g₂) ≫ (F ⋙ G).map f₂

Tactic:
simp
-- 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_1 : C
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Presieve.{v₁, u₁} X_1
x : E
X : D
g₁ : x ⟶ G.obj X
X' : C
f₂ : X' ⟶ X_1
g₂ : X ⟶ F.obj X'
h₁ : R f₂
⊢ functorPushforward (F ⋙ G) R (g₁ ≫ G.map (g₂ ≫ F.map f₂))

Tactic:
exact ⟨X', f₂, g₁ ≫ G.map g₂, h₁, by simp⟩
-- 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 : C
R : Presieve.{v₁, u₁} X
f : Y ⟶ X
h : R f
⊢ F.map f = 𝟙 (F.obj Y) ≫ F.map f

Tactic:
simp
-- 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 : C
f : Y ⟶ X
R : Presieve.{v₁, u₁} X
hf : R f
⊢ map F R (F.map f)

Tactic:
⟨hf⟩

Premises used: CategoryTheory.Presieve.map.of
-- 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 : C
R : Presieve.{v₁, u₁} X
Y : D
f : Y ⟶ F.obj X
h : map F R f
Y_1 : C
u : Y_1 ⟶ X
hu : R u
⊢ F.map u = eqToHom ⋯ ≫ F.map u

Tactic:
simp
-- 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 : C
R : Presieve.{v₁, u₁} X
Y : D
f : Y ⟶ F.obj X
refine :
  (∃ (Z : C) (h : F.obj Z = Y) (g : Z ⟶ X), R g ∧ F.map g = eqToHom h ≫ f) →
    ∀ (Z : C) (h : F.obj Z = Y) (g : Z ⟶ X) (hg : R g) (heq : F.map g = eqToHom h ≫ f), map F R f
⊢ map F R f ↔ ∃ (Z : C) (h : F.obj Z = Y) (g : Z ⟶ X), R g ∧ F.map g = eqToHom h ≫ f

Tactic:
refine ⟨fun (.of (u := u) hu) ↦ ⟨_, rfl, u, hu, by simp⟩, fun ⟨Z, h, g, hg, heq⟩ ↦ ?_⟩
-- 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 : C
R : Presieve.{v₁, u₁} X
Y : D
f : Y ⟶ F.obj X
h_1 : ∃ (Z : C) (h : F.obj Z = Y) (g : Z ⟶ X), R g ∧ F.map g = eqToHom h ≫ f
Z : C
h : F.obj Z = Y
g : Z ⟶ X
hg : R g
heq : F.map g = eqToHom h ≫ f
subst :
  ∀ {f : F.obj Z ⟶ F.obj X},
    (∃ (Z_1 : C) (h : F.obj Z_1 = F.obj Z) (g : Z_1 ⟶ X), R g ∧ F.map g = eqToHom h ≫ f) →
      ∀ (heq : F.map g = eqToHom ⋯ ≫ f), map F R f
⊢ map F R f

Tactic:
subst h
-- 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 : C
R : Presieve.{v₁, u₁} X
Z : C
g : Z ⟶ X
hg : R g
f : F.obj Z ⟶ F.obj X
h : ∃ (Z_1 : C) (h : F.obj Z_1 = F.obj Z) (g : Z_1 ⟶ X), R g ∧ F.map g = eqToHom h ≫ f
heq : F.map g = eqToHom ⋯ ≫ f
⊢ F.map g = f

Tactic:
rw [eqToHom_refl, Category.id_comp] at heq

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.id_comp
-- 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 : C
R : Presieve.{v₁, u₁} X
Z : C
g : Z ⟶ X
hg : R g
f : F.obj Z ⟶ F.obj X
h : ∃ (Z_1 : C) (h : F.obj Z_1 = F.obj Z) (g : Z_1 ⟶ X), R g ∧ F.map g = eqToHom h ≫ f
heq : F.map g = f
⊢ map F R f

Tactic:
simp [← heq, map_map hg]

Premises used: CategoryTheory.Presieve.map_map
-- 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 : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ map F (ofArrows Y f) = ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i)

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

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.Presieve.map_map, CategoryTheory.Presieve.map, le_antisymm, CategoryTheory.Presieve.ofArrows, _private.0.CategoryTheory.Presieve.map_ofArrows.match_1
-- 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 : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
refine :
  ∀ (Z : D) (g : Z ⟶ F.obj X) (hg : map F (ofArrows Y f) g),
    ofArrows (fun (i : ι) ↦ F.obj (Y i)) (fun (i : ι) ↦ F.map (f i)) g
⊢ map F (ofArrows Y f) = ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i)

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

Premises used: le_antisymm
-- 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 : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : D
g : Z ⟶ F.obj X
hg : map F (ofArrows Y f) g
obtain :
  ∀ ⦃Y_1 : D⦄ {Y_2 : C} {u : Y_2 ⟶ X} (hu : ofArrows Y f u),
    ofArrows (fun (i : ι) ↦ F.obj (Y i)) (fun (i : ι) ↦ F.map (f i)) (F.map u)
⊢ ofArrows (fun (i : ι) ↦ F.obj (Y i)) (fun (i : ι) ↦ F.map (f i)) g

Tactic:
obtain ⟨hu⟩ := hg
-- 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 : C
ι : Type u_1
Y_1 : ι → C
f : (i : ι) → Y_1 i ⟶ X
Y : D
Y_2 : C
u : Y_2 ⟶ X
hu : ofArrows Y_1 f u
obtain :
  ∀ (i : ι) (hu : ofArrows Y_1 f (eqToHom ⋯ ≫ f i)),
    ofArrows (fun (i : ι) ↦ F.obj (Y_1 i)) (fun (i : ι) ↦ F.map (f i)) (F.map (eqToHom ⋯ ≫ f i))
⊢ ofArrows (fun (i : ι) ↦ F.obj (Y_1 i)) (fun (i : ι) ↦ F.map (f i)) (F.map u)

Tactic:
obtain ⟨i, rfl, rfl⟩ := Presieve.ofArrows_surj _ _ hu

Premises used: CategoryTheory.Presieve.ofArrows_surj, rfl
-- 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 : C
ι : Type u_1
Y_1 : ι → C
f : (i : ι) → Y_1 i ⟶ X
Y : D
i : ι
hu : ofArrows Y_1 f (eqToHom ⋯ ≫ f i)
⊢ ofArrows (fun (i : ι) ↦ F.obj (Y_1 i)) (fun (i : ι) ↦ F.map (f i)) (F.map (eqToHom ⋯ ≫ f i))

Tactic:
simpa using ofArrows.mk i

Premises used: CategoryTheory.Presieve.ofArrows.mk
-- 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 : C
f : X ⟶ Y
rw : map F (ofArrows (fun (x : PUnit.{1}) ↦ X) fun (x : PUnit.{1}) ↦ f) = singleton (F.map f)
rw₁ : (ofArrows (fun (i : PUnit.{1}) ↦ F.obj X) fun (i : PUnit.{1}) ↦ F.map f) = singleton (F.map f)
rw₂ rw₃ : singleton (F.map f) = singleton (F.map f)
⊢ map F (singleton f) = singleton (F.map f)

Tactic:
rw [← ofArrows_pUnit.{_, _, 0}, map_ofArrows, ofArrows_pUnit]

Premises used: CategoryTheory.Presieve.map_ofArrows, CategoryTheory.Presieve.ofArrows_pUnit
-- 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 : C
R : Presieve.{v₁, u₁} X
S : Presieve.{v₂, u₂} (F.obj X)
⊢ map F R ≤ S ↔ R ≤ functorPullback F S

Tactic:
⟨fun h _ _ hf ↦ h _ _ (.of hf), fun h _ f ⟨hu⟩ ↦ h _ _ hu⟩

Premises used: _private.0.CategoryTheory.Presieve.map_iff.match_1, CategoryTheory.Functor.map, Iff.intro, CategoryTheory.Presieve.map.of, CategoryTheory.Functor.obj
-- 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 : C
⊢ GaloisConnection (α := Presieve.{v₁, u₁} X) (map F) (functorPullback F)

Tactic:
fun _ _ ↦ Presieve.map_le_iff_le_functorPullback

Premises used: CategoryTheory.Presieve.map_le_iff_le_functorPullback, GaloisConnection
-- 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 : C
R : Presieve.{v₂, u₂} (F.obj X)
⊢ map F (functorPullback F R) ≤ R

Tactic:
(galoisConnection_map_functorPullback _ _).l_u_le _

Premises used: GaloisConnection.l_u_le, CategoryTheory.Presieve.galoisConnection_map_functorPullback
-- 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 : C
R : Presieve.{v₁, u₁} X
⊢ R ≤ functorPullback F (map F R)

Tactic:
(galoisConnection_map_functorPullback _ _).le_u_l _

Premises used: GaloisConnection.le_u_l, CategoryTheory.Presieve.galoisConnection_map_functorPullback
-- 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 : C
R : Presieve.{v₁, u₁} X
⊢ map F (functorPullback F (map F R)) = map F R

Tactic:
(galoisConnection_map_functorPullback _ _).l_u_l_eq_l _

Premises used: GaloisConnection.l_u_l_eq_l, CategoryTheory.Presieve.galoisConnection_map_functorPullback
-- 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 : C
R : Presieve.{v₂, u₂} (F.obj X)
⊢ functorPullback F (map F (functorPullback F R)) = functorPullback F R

Tactic:
(galoisConnection_map_functorPullback _ _).u_l_u_eq_u _

Premises used: CategoryTheory.Presieve.galoisConnection_map_functorPullback, GaloisConnection.u_l_u_eq_u
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R : Presieve.{v₁, u₁} X
⊢ map (𝟭 C) R = R

Tactic:
le_antisymm (fun _ _ ⟨hg⟩ ↦ hg) fun _ _ hg ↦ ⟨hg⟩

Premises used: le_antisymm, CategoryTheory.Presieve.map.of
-- 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 : C
⊢ Monotone (α := Presieve.{v₁, u₁} X) (map F)

Tactic:
(galoisConnection_map_functorPullback _ _).monotone_l

Premises used: GaloisConnection.monotone_l, CategoryTheory.Presieve.galoisConnection_map_functorPullback
-- 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 : C
⊢ Monotone (α := Presieve.{v₂, u₂} (F.obj X)) (functorPullback F)

Tactic:
(Presieve.galoisConnection_map_functorPullback F X).monotone_u

Premises used: GaloisConnection.monotone_u, CategoryTheory.Presieve.galoisConnection_map_functorPullback
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
h :
  ∀ (Z : C) (v : Z ⟶ X),
    Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry ↔
      Membership.mem (γ := Set ((Y : C) × (Y ⟶ X))) {Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u}
        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
⊢ (singleton u).uncurry = {Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u}

Tactic:
ext ⟨Z, v⟩
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
h :
  Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry →
    Membership.mem (γ := Set ((Y : C) × (Y ⟶ X))) {Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u}
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
h₁ :
  Membership.mem (γ := Set ((Y : C) × (Y ⟶ X))) {Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u}
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) →
    Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry ↔
    Membership.mem (γ := Set ((Y : C) × (Y ⟶ X))) {Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u}
      (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 Z : C
v : Z ⟶ X
Y : C
⊢ Membership.mem (γ := Set ((Y : C) × (Y ⟶ X)))
    {Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
        (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v))
        (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v))}
    (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
h :
  Membership.mem (γ := Set ((Y : C) × (Y ⟶ X))) {Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u}
    (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
⊢ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) =
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) ∧
    HEq.{v₁ + 1} (α := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) :
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
      (β := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) ⟶ X)
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) :
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) ⟶ X)

Tactic:
rw [Set.mem_singleton_iff, Sigma.ext_iff] at h

Premises used: Sigma.ext_iff, Set.mem_singleton_iff
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
h :
  Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) =
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) ∧
    HEq.{v₁ + 1} (α := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) :
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
      (β := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) ⟶ X)
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) :
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u) ⟶ X)
h₁ :
  ∀ (u : Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
    (h :
      HEq.{v₁ + 1} (α := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
        (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) :
          Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
        (β :=
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X)
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
              (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)) u) ⟶
          X)
        (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X)
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
              (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)) u) :
          Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X)
              (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
                (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)) u) ⟶
            X)),
    Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry

Tactic:
obtain ⟨rfl, h⟩ := h

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Z : C
v : Z ⟶ X
u : Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X
h :
  HEq.{v₁ + 1} (α := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
    (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) :
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
    (β :=
    Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X)
        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
          (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)) u) ⟶
      X)
    (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X)
        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
          (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)) u) :
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X)
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
            (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)) u) ⟶
        X)
h₁ :
  Membership.mem (γ := Set ((Y : C) × (Y ⟶ X)))
    (uncurry
        (singleton (Y := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v))
          (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v))) :
      Set ((Y : C) × (Y ⟶ X)))
    (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (singleton u).uncurry

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Z : C
v : Z ⟶ X
⊢ Membership.mem (γ := Set ((Y : C) × (Y ⟶ X)))
    (uncurry
        (singleton (Y := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v))
          (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v))) :
      Set ((Y : C) × (Y ⟶ 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
inst_1 : HasPullbacks.{v₁, u₁} C
B : C
b : B ⟶ X
h :
  ∀ (Z : C) (v : Z ⟶ B),
    Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v ∈ (pullbackArrows b s).uncurry ↔
      Membership.mem (γ := Set ((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)) ''
          s.uncurry)
        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v)
⊢ (pullbackArrows b s).uncurry =
    (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)) ''
      s.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
inst_1 : HasPullbacks.{v₁, u₁} C
B : C
b : B ⟶ X
Z : C
v : Z ⟶ B
h :
  Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v ∈ (pullbackArrows b s).uncurry →
    Membership.mem (γ := Set ((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)) ''
        s.uncurry)
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v)
h₁ :
  Membership.mem (γ := Set ((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)) ''
        s.uncurry)
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v) →
    Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v ∈ (pullbackArrows b s).uncurry
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v ∈ (pullbackArrows b s).uncurry ↔
    Membership.mem (γ := Set ((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)) ''
        s.uncurry)
      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) 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
inst_1 : HasPullbacks.{v₁, u₁} C
B : C
b : B ⟶ X
Y_1 Y : C
u : Y ⟶ X
hu : s u
⊢ Membership.mem (γ := Set ((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)) ''
      s.uncurry)
    (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (limit.cone (cospan u b)).1
      ((limit.cone (cospan u b)).π.1 WalkingCospan.right))

Tactic:
⟨⟨Y, u⟩, hu, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, Sigma.mk, rfl
-- 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_1 Y : C
u : Y ⟶ X
hu : s u
⊢ Membership.mem (γ := Set ((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)) ''
      s.uncurry)
    (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (limit.cone (cospan u b)).1
      ((limit.cone (cospan u b)).π.1 WalkingCospan.right))

Tactic:
exact ⟨⟨Y, u⟩, hu, rfl⟩