awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
U : Sieve.{v₁, u₁} X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve.{v₁, u₁} Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible (R := (Sieve.bind U.arrows B).arrows)
y_1 : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows :=
  fun (Y : C) (f : Y ⟶ X) (hf : U.arrows f) (Z : C) (g : Z ⟶ Y) (hg : (B hf).arrows g) ↦ s (g ≫ f) ⋯
hy_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y_1 hf).Compatible (R := (B hf).arrows)
t : FamilyOfElements P U.arrows :=
  fun (Y : C) (f : Y ⟶ X) (hf : U.arrows f) ↦ ⋯.amalgamate (R := (B hf).arrows) (y_1 hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y_1 hf).IsAmalgamation (R := (B hf).arrows) (t f hf)
hT : t.Compatible (R := U.arrows)
y : P.obj (op X)
hy : s.IsAmalgamation (R := (Sieve.bind U.arrows B).arrows) y
refine_2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    U.arrows f →
      Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
              (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
            y :
          (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
              (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
            (hU.amalgamate (R := U.arrows) t hT) :
          (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
⊢ y = hU.amalgamate (R := U.arrows) t hT

Tactic:
apply hU.isSeparatedFor.ext

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
U : Sieve.{v₁, u₁} X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve.{v₁, u₁} Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible (R := (Sieve.bind U.arrows B).arrows)
y_1 : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows :=
  fun (Y : C) (f : Y ⟶ X) (hf : U.arrows f) (Z : C) (g : Z ⟶ Y) (hg : (B hf).arrows g) ↦ s (g ≫ f) ⋯
hy_1 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y_1 hf).Compatible (R := (B hf).arrows)
t : FamilyOfElements P U.arrows :=
  fun (Y : C) (f : Y ⟶ X) (hf : U.arrows f) ↦ ⋯.amalgamate (R := (B hf).arrows) (y_1 hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y_1 hf).IsAmalgamation (R := (B hf).arrows) (t f hf)
hT : t.Compatible (R := U.arrows)
y : P.obj (op X)
hy : s.IsAmalgamation (R := (Sieve.bind U.arrows B).arrows) y
Y : C
f : Y ⟶ X
hf : U.arrows f
refine_2 :
  ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (B hf).arrows f_1 →
      Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (op Y_1)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f_1.op) :
              (a : (fun (X : Type u_1) ↦ X) (P.obj (op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y_1)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
                  (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
                y :
              (fun (X : Type u_1) ↦ X) (P.obj (op Y))) :
          (fun (X : Type u_1) ↦ X) (P.obj (op Y_1)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f_1.op) :
              (a : (fun (X : Type u_1) ↦ X) (P.obj (op Y))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y_1)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
                  (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
                (hU.amalgamate (R := U.arrows) t hT) :
              (fun (X : Type u_1) ↦ X) (P.obj (op Y))) :
          (fun (X : Type u_1) ↦ X) (P.obj (op Y_1)))
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
        y :
      (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type u_1) ↦ X) (P.obj (op X))) → (fun (X : Type u_1) ↦ X) (P.obj (op Y)))
        (hU.amalgamate (R := U.arrows) t hT) :
      (fun (X : Type u_1) ↦ X) (P.obj (op Y)))

Tactic:
apply (hB hf).isSeparatedFor.ext

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
Z W : C
f : Z ⟶ W
g : W ⟶ X
hg : R.arrows g
hf : S.arrows (f ≫ g)
⊢ S.arrows (f ≫ g)

Tactic:
apply hf
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
⊢ (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows

Tactic:
have : (Sieve.bind R fun Y f _ => S.pullback f : Presieve X) ≤ S := by
    rintro Z f ⟨W, f, g, hg, hf : S _, rfl⟩
    apply hf
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
hS₁ : IsSheafFor P (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows
trans :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      IsSeparatedFor P
        (Sieve.pullback f (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S)).arrows
⊢ IsSheafFor P S.arrows

Tactic:
apply Presieve.isSheafFor_subsieve_aux P this

Premises used: CategoryTheory.Presieve.isSheafFor_subsieve_aux
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
hS₁ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : R.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y),
    IsSeparatedFor P (Sieve.pullback g (Sieve.pullback f S)).arrows
⊢ IsSheafFor P (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows

Tactic:
apply isSheafFor_bind _ _ _ hR hS

Premises used: CategoryTheory.Presieve.isSheafFor_bind
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : R.arrows f
Z : C
g : Z ⟶ Y
hS₁ : IsSeparatedFor P (Sieve.pullback (g ≫ f) S).arrows
⊢ IsSeparatedFor P (Sieve.pullback g (Sieve.pullback f S)).arrows

Tactic:
rw [← pullback_comp]

Premises used: CategoryTheory.Sieve.pullback_comp
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : R.arrows f
Z : C
g : Z ⟶ Y
⊢ IsSeparatedFor P (Sieve.pullback (g ≫ f) S).arrows

Tactic:
apply (hS (R.downward_closed hf _)).isSeparatedFor

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
h :
  ∀ ⦃Z : C⦄ (g : Z ⟶ Y),
    (Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S)).arrows g ↔
      (Sieve.pullback f R).arrows g
⊢ Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S) =
    Sieve.pullback f R

Tactic:
ext Z g
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
h :
  (Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S)).arrows g →
    (Sieve.pullback f R).arrows g
h₁ :
  (Sieve.pullback f R).arrows g →
    (Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S)).arrows g
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S)).arrows g ↔
    (Sieve.pullback f R).arrows g

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
W : C
k : Z ⟶ W
l : W ⟶ X
hl : R.arrows l
left : arrows ((fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S) W l hl) k
comm : k ≫ l = g ≫ f
h : R.arrows (k ≫ l)
⊢ (Sieve.pullback f R).arrows g

Tactic:
rw [pullback_apply, ← comm]

Premises used: CategoryTheory.Sieve.pullback_apply
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
W : C
k : Z ⟶ W
l : W ⟶ X
hl : R.arrows l
left : arrows ((fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S) W l hl) k
comm : k ≫ l = g ≫ f
⊢ R.arrows (k ≫ l)

Tactic:
simp [hl]
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
a : (Sieve.pullback f R).arrows g
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S)).arrows g

Tactic:
⟨Z, 𝟙 Z, _, a, ?_⟩

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Presieve.bind, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
a : (Sieve.pullback f R).arrows g
h :
  (fun (x : C) (x_1 : x ⟶ X) (h : R.arrows x_1) ↦
        (arrows ((fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S) x x_1 h) : Presieve.{v₁, u₁} x))
      Z (g ≫ f) a (𝟙 Z) ∧
    𝟙 Z ≫ g ≫ f = g ≫ f
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S)).arrows g

Tactic:
refine ⟨Z, 𝟙 Z, _, a, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
a : (Sieve.pullback f R).arrows g
⊢ (fun (x : C) (x_1 : x ⟶ X) (h : R.arrows x_1) ↦
        (arrows ((fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S) x x_1 h) : Presieve.{v₁, u₁} x))
      Z (g ≫ f) a (𝟙 Z) ∧
    𝟙 Z ≫ g ≫ f = g ≫ f

Tactic:
simp [hf]
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S) =
    Sieve.pullback f R

Tactic:
have : Sieve.pullback f (Sieve.bind R fun T (k : T ⟶ X) (_ : R k) => pullback k S) =
        R.pullback f := by
      ext Z g
      constructor
      · rintro ⟨W, k, l, hl, _, comm⟩
        rw [pullback_apply, ← comm]
        simp [hl]
      · intro a
        refine ⟨Z, 𝟙 Z, _, a, ?_⟩
        simp [hf]
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this_1 : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
this :
  Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S) =
    Sieve.pullback f R
trans : IsSeparatedFor P (Sieve.pullback f R).arrows
⊢ IsSeparatedFor P
    (Sieve.pullback f (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S)).arrows

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, u_1, u₁, u_1 + 1} Cᵒᵖ (Type u_1)
R S : Sieve.{v₁, u₁} X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this_1 : (Sieve.bind R.arrows fun (Y : C) (f : Y ⟶ X) (x : R.arrows f) ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
this :
  Sieve.pullback f (Sieve.bind R.arrows fun (T : C) (k : T ⟶ X) (x : R.arrows k) ↦ Sieve.pullback k S) =
    Sieve.pullback f R
⊢ IsSeparatedFor P (Sieve.pullback f R).arrows

Tactic:
apply hR' hf
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X : Type u
R : Presieve X
⊢ R ∈ jointlySurjectivePrecoverage.coverings X ↔
    ∀ (x : X),
      ∃ (Y : Type u) (g : Y ⟶ X),
        R g ∧
          Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
            (Set.range (ι := (fun (X : Type u) ↦ X) Y)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
                (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) X))
            x

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X Y : Type u
f : X ⟶ Y
hf :
  Function.Surjective (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
x : Y
⊢ Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
    (Set.range (ι := (fun (X : Type u) ↦ X) X)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
    x

Tactic:
simp [hf.range_eq]

Premises used: Function.Surjective.range_eq
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X Y : Type u
f : X ⟶ Y
refine :
  ∀
    (hf :
      ∀ (x : Y),
        ∃ (Y_1 : Type u) (g : Y_1 ⟶ Y),
          Presieve.singleton f g ∧
            Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
              (Set.range (ι := (fun (X : Type u) ↦ X) Y_1)
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
                  (a : (fun (X : Type u) ↦ X) Y_1) → (fun (X : Type u) ↦ X) Y))
              x)
    (x : (fun (X : Type u) ↦ X) Y),
    ∃ (a : (fun (X : Type u) ↦ X) X),
      (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) a = x
⊢ (∀ (x : Y),
      ∃ (Y_1 : Type u) (g : Y_1 ⟶ Y),
        Presieve.singleton f g ∧
          Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
            (Set.range (ι := (fun (X : Type u) ↦ X) Y_1)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
                (a : (fun (X : Type u) ↦ X) Y_1) → (fun (X : Type u) ↦ X) Y))
            x) ↔
    Function.Surjective (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)

Tactic:
refine ⟨fun hf x ↦ ?_, fun hf x ↦ ⟨X, f, ⟨⟩, by simp [hf.range_eq]⟩⟩
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X Y : Type u
f : X ⟶ Y
hf :
  ∀ (x : Y),
    ∃ (Y_1 : Type u) (g : Y_1 ⟶ Y),
      Presieve.singleton f g ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
          (Set.range (ι := (fun (X : Type u) ↦ X) Y_1)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
              (a : (fun (X : Type u) ↦ X) Y_1) → (fun (X : Type u) ↦ X) Y))
          x
x : (fun (X : Type u) ↦ X) Y
obtain :
  ∀ ⦃Y_1 : Type u⦄
    (hx :
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
        (Set.range (ι := (fun (X : Type u) ↦ X) X)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
        x),
    ∃ (a : (fun (X : Type u) ↦ X) X),
      (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) a = x
⊢ ∃ (a : (fun (X : Type u) ↦ X) X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y) a = x

Tactic:
obtain ⟨_, _, ⟨⟩, hx⟩ := hf x
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X Y_1 : Type u
f : X ⟶ Y_1
hf :
  ∀ (x : Y_1),
    ∃ (Y : Type u) (g : Y ⟶ Y_1),
      Presieve.singleton f g ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y_1))
          (Set.range (ι := (fun (X : Type u) ↦ X) Y)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
              (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Y_1))
          x
x : (fun (X : Type u) ↦ X) Y_1
Y : Type u
hx :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y_1))
    (Set.range (ι := (fun (X : Type u) ↦ X) X)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y_1))
    x
⊢ ∃ (a : (fun (X : Type u) ↦ X) X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y_1) a = x

Tactic:
hx

Premises used: Set.Mem, setOf, Set.range
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X Y_1 : Type u
f : X ⟶ Y_1
hf :
  ∀ (x : Y_1),
    ∃ (Y : Type u) (g : Y ⟶ Y_1),
      Presieve.singleton f g ∧
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y_1))
          (Set.range (ι := (fun (X : Type u) ↦ X) Y)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
              (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Y_1))
          x
x : (fun (X : Type u) ↦ X) Y_1
Y : Type u
hx :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y_1))
    (Set.range (ι := (fun (X : Type u) ↦ X) X)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y_1))
    x
⊢ ∃ (a : (fun (X : Type u) ↦ X) X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y_1) a = x

Tactic:
exact hx
-- Module: Mathlib.CategoryTheory.Sites.JointlySurjective
Goal:
X : Type u
ι : Type u_1
Y : ι → Type u
f : (i : ι) → Y i ⟶ X
⊢ Presieve.ofArrows Y f ∈ jointlySurjectivePrecoverage.coverings X ↔
    ∀ (x : (fun (X : Type u) ↦ X) X),
      ∃ (i : ι),
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
          (Set.range (ι := (fun (X : Type u) ↦ X) (Y i))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f i)) :
              (a : (fun (X : Type u) ↦ X) (Y i)) → (fun (X : Type u) ↦ X) X))
          x

Tactic:
⟨fun h x ↦ ?_, fun h x ↦ ?_⟩

Premises used: Iff.intro