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 : Functor.{v₁, v₂, u₁, u₂} C D
X Y_1 Z_1 : C
f_1 : Y_1 ⟶ X
S R_1 : Sieve.{v₁, u₁} X
R : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : R ⟶ Functor.obj yoneda X
Y Z : C
t : R.obj (Opposite.op Y)
g : Z ⟶ Y
refine :
  Eq (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)))
    ((hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
          (a : (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Z))) →
            (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (Opposite.op Z)))
        ((hom (FC := TypeCat.Fun) (R.map g.op) :
              (a : (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Y))) → (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Z)))
            t :
          (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Z))) :
      (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)))
    (g ≫
        (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
            (a : (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Y))) →
              (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (Opposite.op Y)))
          t :
      Z ⟶ X)
⊢ ∃ (t_1 : R.obj (Opposite.op Z)),
    Eq (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)))
      ((hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
            (a : (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Z))) →
              (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (Opposite.op Z)))
          t_1 :
        (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)))
      (g ≫
          (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
              (a : (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Y))) →
                (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (Opposite.op Y)))
            t :
        Z ⟶ X)

Tactic:
refine ⟨R.map g.op t, ?_⟩
-- 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_1 Z_1 : C
f_1 : Y_1 ⟶ X
S R_1 : Sieve.{v₁, u₁} X
R : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : R ⟶ Functor.obj yoneda X
Y Z : C
t : R.obj (Opposite.op Y)
g : Z ⟶ Y
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)))
    ((hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
          (a : (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Z))) →
            (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (Opposite.op Z)))
        ((hom (FC := TypeCat.Fun) (R.map g.op) :
              (a : (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Y))) → (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Z)))
            t :
          (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Z))) :
      (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)))
    (g ≫
        (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
            (a : (fun (X : Type v₁) ↦ X) (R.obj (Opposite.op Y))) →
              (fun (X : Type v₁) ↦ X) ((yoneda.obj X).obj (Opposite.op Y)))
          t :
      Z ⟶ X)

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

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
h :
  (∃ (t : S.functor.obj (Opposite.op Y)),
      (hom (FC := TypeCat.Fun) (↾fun (f : S.functor.obj (Opposite.op Y)) ↦ (↑f : Y ⟶ X)) :
            (a : S.functor.obj (Opposite.op Y)) → (yoneda.obj X).obj (Opposite.op Y))
          t =
        f) →
    S.arrows f
h₁ :
  S.arrows f →
    ∃ (t : S.functor.obj (Opposite.op Y)),
      (hom (FC := TypeCat.Fun) (↾fun (f : S.functor.obj (Opposite.op Y)) ↦ (↑f : Y ⟶ X)) :
            (a : S.functor.obj (Opposite.op Y)) → (yoneda.obj X).obj (Opposite.op Y))
          t =
        f
⊢ (∃ (t : S.functor.obj (Opposite.op Y)),
      (hom (FC := TypeCat.Fun) (↾fun (f : S.functor.obj (Opposite.op Y)) ↦ (↑f : Y ⟶ X)) :
            (a : S.functor.obj (Opposite.op Y)) → (yoneda.obj X).obj (Opposite.op Y))
          t =
        f) ↔
    S.arrows f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
Y : C
f : Opposite.unop (Opposite.op Y) ⟶ X
hf : S.arrows f
⊢ S.arrows (Y := Y)
    ((hom (FC := TypeCat.Fun) (↾fun (f : S.functor.obj (Opposite.op Y)) ↦ (↑f : Y ⟶ X)) :
        (a : S.functor.obj (Opposite.op Y)) → (yoneda.obj X).obj (Opposite.op Y))
      (Subtype.mk (p := fun (g : Opposite.unop (Opposite.op Y) ⟶ X) ↦ S.arrows g) f hf))

Tactic:
hf
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
Y : C
f : Opposite.unop (Opposite.op Y) ⟶ X
hf : S.arrows f
⊢ S.arrows (Y := Y)
    ((hom (FC := TypeCat.Fun) (↾fun (f : S.functor.obj (Opposite.op Y)) ↦ (↑f : Y ⟶ X)) :
        (a : S.functor.obj (Opposite.op Y)) → (yoneda.obj X).obj (Opposite.op Y))
      (Subtype.mk (p := fun (g : Opposite.unop (Opposite.op Y) ⟶ X) ↦ S.arrows g) f hf))

Tactic:
exact hf
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ∃ (t : S.functor.obj (Opposite.op Y)),
    (hom (FC := TypeCat.Fun) (↾fun (f : S.functor.obj (Opposite.op Y)) ↦ (↑f : Y ⟶ X)) :
          (a : S.functor.obj (Opposite.op Y)) → (yoneda.obj X).obj (Opposite.op Y))
        t =
      f

Tactic:
⟨⟨_, hf⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ∃ (t : S.functor.obj (Opposite.op Y)),
    (hom (FC := TypeCat.Fun) (↾fun (f : S.functor.obj (Opposite.op Y)) ↦ (↑f : Y ⟶ X)) :
          (a : S.functor.obj (Opposite.op Y)) → (yoneda.obj X).obj (Opposite.op Y))
        t =
      f

Tactic:
exact ⟨⟨_, hf⟩, 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 Y Z : C
f : Y ⟶ X
S R : Sieve.{v₁, u₁} X
⊢ IsIso (C := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (X := functor (X := X) ⊤) (functorInclusion ⊤)

Tactic:
⟨⟨{ app := fun _ => ↾fun a => ⟨a, ⟨⟩⟩ }, rfl, rfl⟩⟩

Premises used: TypeCat.ofHom, Subtype.mk, CategoryTheory.NatTrans.mk, And.intro, Exists.intro, CategoryTheory.IsIso.mk, rfl, True.intro
-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S T : Sieve.{v₁, u₁} X
h : S ≤ T
⊢ uliftNatTransOfLe h ≫ T.uliftFunctorInclusion = S.uliftFunctorInclusion

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.comp, TypeCat.Fun.comp, CategoryTheory.Sieve.uliftFunctorInclusion, CategoryTheory.Functor.whiskerRight, 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 Y Z : C
f : Y ⟶ X
S_1 R S : Sieve.{v₁, u₁} X
Z_1 : Cᵒᵖ ⥤ Type (max w v₁)
x x_1 : Z_1 ⟶ uliftFunctor.{w, v₁, u₁} S
h : x ≫ S.uliftFunctorInclusion = x_1 ≫ S.uliftFunctorInclusion
w :
  ∀ (Y : Cᵒᵖ) (y : Z_1.obj Y),
    (hom (FC := TypeCat.Fun) (x.app Y)).toFun y = (hom (FC := TypeCat.Fun) (x_1.app Y)).toFun y
⊢ x = x_1

Tactic:
ext Y y
-- 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_1 Z : C
f : Y_1 ⟶ X
S_1 R S : Sieve.{v₁, u₁} X
Z_1 : Cᵒᵖ ⥤ Type (max w v₁)
x x_1 : Z_1 ⟶ uliftFunctor.{w, v₁, u₁} S
h : x ≫ S.uliftFunctorInclusion = x_1 ≫ S.uliftFunctorInclusion
Y : Cᵒᵖ
y : Z_1.obj Y
⊢ (hom (FC := TypeCat.Fun) (x.app Y)).toFun y = (hom (FC := TypeCat.Fun) (x_1.app Y)).toFun y

Tactic:
ULift.ext _ _ (Subtype.ext_iff.2 ?_)

Premises used: Iff.mpr, ULift.ext, Subtype.ext_iff
-- 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_1 Z : C
f : Y_1 ⟶ X
S_1 R S : Sieve.{v₁, u₁} X
Z_1 : Cᵒᵖ ⥤ Type (max w v₁)
x x_1 : Z_1 ⟶ uliftFunctor.{w, v₁, u₁} S
h : x ≫ S.uliftFunctorInclusion = x_1 ≫ S.uliftFunctorInclusion
Y : Cᵒᵖ
y : Z_1.obj Y
w :
  (↑(ULift.down.{w, v₁} ((hom (FC := TypeCat.Fun) (x.app Y)).toFun y)) : Opposite.unop Y ⟶ X) =
    (↑(ULift.down.{w, v₁} ((hom (FC := TypeCat.Fun) (x_1.app Y)).toFun y)) : Opposite.unop Y ⟶ X)
⊢ (hom (FC := TypeCat.Fun) (x.app Y)).toFun y = (hom (FC := TypeCat.Fun) (x_1.app Y)).toFun y

Tactic:
refine ULift.ext _ _ (Subtype.ext_iff.2 ?_)

Premises used: Iff.mpr, ULift.ext, Subtype.ext_iff
-- 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_1 Z : C
f : Y_1 ⟶ X
S_1 R S : Sieve.{v₁, u₁} X
Z_1 : Cᵒᵖ ⥤ Type (max w v₁)
x x_1 : Z_1 ⟶ uliftFunctor.{w, v₁, u₁} S
h : x ≫ S.uliftFunctorInclusion = x_1 ≫ S.uliftFunctorInclusion
Y : Cᵒᵖ
y : Z_1.obj Y
⊢ (↑(ULift.down.{w, v₁} ((hom (FC := TypeCat.Fun) (x.app Y)).toFun y)) : Opposite.unop Y ⟶ X) =
    (↑(ULift.down.{w, v₁} ((hom (FC := TypeCat.Fun) (x_1.app Y)).toFun y)) : Opposite.unop Y ⟶ X)

Tactic:
simpa using congr_hom (NatTrans.congr_app h Y) y

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.ConcreteCategory.congr_hom
-- 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_1 Z_1 : C
f_1 : Y_1 ⟶ X
S R_1 : Sieve.{v₁, u₁} X
R : Cᵒᵖ ⥤ Type (max w v₁)
f : R ⟶ Functor.obj uliftYoneda.{w, v₁, u₁} X
Y Z : C
_ :
  ∀ {f_2 : Y ⟶ X},
    (∃ (t : R.obj (Opposite.op Y)),
        (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
              (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))) →
                (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Y)))
            t =
          { down := f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Y)) }) →
      ∀ (g : Z ⟶ Y),
        ∃ (t : R.obj (Opposite.op Z)),
          (hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
                (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Z))) →
                  (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Z)))
              t =
            { down := g ≫ f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)) }
⊢ ∀ {f_2 : Y ⟶ X},
    (∃ (t : R.obj (Opposite.op Y)),
        (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
              (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))) →
                (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Y)))
            t =
          { down := f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Y)) }) →
      ∀ (g : Z ⟶ Y),
        ∃ (t : R.obj (Opposite.op Z)),
          (hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
                (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Z))) →
                  (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Z)))
              t =
            { down := g ≫ f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)) }

Tactic:
_
-- 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_1 Z_1 : C
f_1 : Y_1 ⟶ X
S R_1 : Sieve.{v₁, u₁} X
R : Cᵒᵖ ⥤ Type (max w v₁)
f : R ⟶ Functor.obj uliftYoneda.{w, v₁, u₁} X
Y Z : C
f_2 : Y ⟶ X
this :
  ∀ (t : R.obj (Opposite.op Y))
    (ht :
      (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
            (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))) →
              (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Y)))
          t =
        { down := f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Y)) })
    (g : Z ⟶ Y),
    ∃ (t : R.obj (Opposite.op Z)),
      (hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
            (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Z))) →
              (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Z)))
          t =
        { down := g ≫ f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)) }
⊢ (∃ (t : R.obj (Opposite.op Y)),
      (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
            (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))) →
              (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Y)))
          t =
        { down := f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Y)) }) →
    ∀ (g : Z ⟶ Y),
      ∃ (t : R.obj (Opposite.op Z)),
        (hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
              (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Z))) →
                (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Z)))
            t =
          { down := g ≫ f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)) }

Tactic:
⟨t, ht⟩
-- 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_1 Z_1 : C
f_1 : Y_1 ⟶ X
S R_1 : Sieve.{v₁, u₁} X
R : Cᵒᵖ ⥤ Type (max w v₁)
f : R ⟶ Functor.obj uliftYoneda.{w, v₁, u₁} X
Y Z : C
f_2 : Y ⟶ X
t : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))
ht :
  (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
        (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))) →
          (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Y)))
      t =
    { down := f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Y)) }
g : Z ⟶ Y
⊢ ∃ (t : R.obj (Opposite.op Z)),
    (hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Z))) →
            (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Z)))
        t =
      { down := g ≫ f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)) }

Tactic:
⟨R.map g.op t, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, Exists.intro, DFunLike.coe
-- 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_1 Z_1 : C
f_1 : Y_1 ⟶ X
S R_1 : Sieve.{v₁, u₁} X
R : Cᵒᵖ ⥤ Type (max w v₁)
f : R ⟶ Functor.obj uliftYoneda.{w, v₁, u₁} X
Y Z : C
f_2 : Y ⟶ X
t : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))
ht :
  (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
        (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))) →
          (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Y)))
      t =
    { down := f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Y)) }
g : Z ⟶ Y
refine :
  (hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
        (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Z))) →
          (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Z)))
      ((hom (FC := TypeCat.Fun) (R.map g.op) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))) →
            (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Z)))
        t) =
    { down := g ≫ f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)) }
⊢ ∃ (t : R.obj (Opposite.op Z)),
    (hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Z))) →
            (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Z)))
        t =
      { down := g ≫ f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)) }

Tactic:
refine ⟨R.map g.op t, ?_⟩
-- 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_1 Z_1 : C
f_1 : Y_1 ⟶ X
S R_1 : Sieve.{v₁, u₁} X
R : Cᵒᵖ ⥤ Type (max w v₁)
f : R ⟶ Functor.obj uliftYoneda.{w, v₁, u₁} X
Y Z : C
f_2 : Y ⟶ X
t : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))
ht :
  (hom (FC := TypeCat.Fun) (f.app (Opposite.op Y)) :
        (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))) →
          (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Y)))
      t =
    { down := f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Y)) }
g : Z ⟶ Y
⊢ (hom (FC := TypeCat.Fun) (f.app (Opposite.op Z)) :
        (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Z))) →
          (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (Opposite.op Z)))
      ((hom (FC := TypeCat.Fun) (R.map g.op) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Y))) →
            (fun (X : Type (max v₁ w)) ↦ X) (R.obj (Opposite.op Z)))
        t) =
    { down := g ≫ f_2 : ULift.{w, v₁} (Functor.obj (Functor.obj yoneda X) (Opposite.op Z)) }

Tactic:
simp [ht]
-- 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 R : Sieve.{v₁, u₁} X
⊢ IsIso (C := Cᵒᵖ ⥤ Type (max w v₁)) (X := uliftFunctor.{w, v₁, u₁} (X := X) ⊤) (uliftFunctorInclusion ⊤)

Tactic:
⟨⟨{ app := fun _ ↦ ↾fun a ↦ ⟨a.down, ⟨⟩⟩ }, rfl, rfl⟩⟩

Premises used: TypeCat.ofHom, Subtype.mk, CategoryTheory.NatTrans.mk, And.intro, Exists.intro, ULift.up, CategoryTheory.IsIso.mk, ULift.down, rfl, True.intro
-- 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
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ ofArrows P p₁ = pullback g (ofArrows X f)

Tactic:
le_antisymm ?_ ?_

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
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
refine_1 : ofArrows P p₁ ≤ pullback g (ofArrows X f)
refine_2 : pullback g (ofArrows X f) ≤ ofArrows P p₁
⊢ ofArrows P p₁ = pullback g (ofArrows X f)

Tactic:
refine le_antisymm ?_ ?_

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
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
refine_1 : Presieve.ofArrows P p₁ ≤ (pullback g (ofArrows X f)).arrows
⊢ ofArrows P p₁ ≤ pullback g (ofArrows X f)

Tactic:
rw [Sieve.ofArrows, Sieve.generate_le_iff]

Premises used: CategoryTheory.Sieve.ofArrows, CategoryTheory.Sieve.generate_le_iff
-- 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
Y_1 : C
g : Y_1 ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y_1
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
Y : C
i : ι
right : p₂ i ≫ f i = p₁ i ≫ g
⊢ (pullback g (ofArrows X f)).arrows (p₁ i)

Tactic:
use X i, p₂ i, f i, ⟨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
Y_1 : C
g : Y_1 ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y_1
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
Y : C
i : ι
⊢ p₂ i ≫ f i = p₁ i ≫ g

Tactic:
(h i).w.symm

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, Eq.symm
-- 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
Y_1 : C
g : Y_1 ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y_1
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
Y : C
i : ι
⊢ p₂ i ≫ f i = p₁ i ≫ g

Tactic:
exact (h i).w.symm

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, Eq.symm
-- 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
Y_1 : C
g : Y_1 ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y_1
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
W : C
u : W ⟶ Y_1
Y : C
i : ι
v : W ⟶ X i
heq : v ≫ f i = u ≫ g
right : ⋯.lift u v ⋯ ≫ p₁ i = u
⊢ (ofArrows P p₁).arrows u

Tactic:
use P i, (h i).lift u v heq.symm, p₁ i, ⟨i⟩

Premises used: Eq.symm, CategoryTheory.IsPullback.lift
-- 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
Y_1 : C
g : Y_1 ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y_1
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
W : C
u : W ⟶ Y_1
Y : C
i : ι
v : W ⟶ X i
heq : v ≫ f i = u ≫ g
⊢ ⋯.lift u v ⋯ ≫ p₁ i = 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_1 Y_1 Z_1 : C
f_1 : Y_1 ⟶ X_1
S_1 R : Sieve.{v₁, u₁} X_1
inst_2 : LocallySmall.{w, v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
Y Z : Cᵒᵖ
g : Y ⟶ Z
f : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y
hf :
  Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
    {f : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y |
      S.arrows (Y := Opposite.unop Y)
        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → Opposite.unop Y ⟶ X) f)}
    f
⊢ Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
    (Set.preimage (β :=
      (fun (X : Type w) ↦ X) (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Z))
      (⇑(hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{w, v₁, u₁} X) g)) :
        (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v₁, u₁}.obj X).obj Y)) →
          (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v₁, u₁}.obj X).obj Z))
      {f : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Z |
        S.arrows (Y := Opposite.unop Z)
          ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Z) → Opposite.unop Z ⟶ X) f)})
    f

Tactic:
simpa [shrinkYonedaObjObjEquiv_obj_map] using S.downward_closed hf _

Premises used: CategoryTheory.Sieve.downward_closed, CategoryTheory.shrinkYonedaObjObjEquiv_obj_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_1 Y Z : C
f : Y ⟶ X_1
S R : Sieve.{v₁, u₁} X_1
inst_2 : LocallySmall.{w, v₁, u₁} C
inst_3 : LocallySmall.{max w' w, v₁, u₁} C
X : Cᵒᵖ
a : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X_1) X
⊢ Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X_1) X))
      (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) X) a ↔
    Membership.mem (α := Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X_1) X) (γ :=
      Set (Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X_1) X))
      (Subfunctor.obj (shrinkFunctor.{max w' w, v₁, u₁} S) X)
      ((Equiv.trans shrinkYonedaObjObjEquiv (Equiv.symm shrinkYonedaObjObjEquiv) :
            (a : (shrinkYoneda.{w, v₁, u₁}.obj X_1).obj X) → (shrinkYoneda.{max w' w, v₁, u₁}.obj X_1).obj X)
          a :
        Functor.obj (Functor.obj shrinkYoneda.{max w' w, v₁, u₁} X_1) X)

Tactic:
simp