awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
f : Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⟶ F
g : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F
dsimp :
  Subfunctor.ι (shrinkFunctor.{w, v₁, u₁} S) ≫ g = f ↔
    ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
      Eq (α := F.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1.op) : (a : F.obj (op X)) → F.obj (op Y))
            ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) g : F.obj (op X)) :
          F.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
              (a :
                  { x : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y) //
                    S.arrows
                      ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) →
                F.obj (op Y))
            (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)) ↦
                S.arrows (Y := Y)
                  ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x))
                ((Equiv.symm shrinkYonedaObjObjEquiv : (a : Y ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) f_1)
                ⋯ :
              { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y) //
                S.arrows (Y := Y)
                  ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) :
          F.obj (op Y))
⊢ Subfunctor.ι (shrinkFunctor.{w, v₁, u₁} S) ≫ g = f ↔
    FamilyOfElements.IsAmalgamation.{w, v₁, u₁} (P := F) (R := S.arrows)
      (↑((shrinkFunctorHomEquiv :
              (a : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F) → { x : FamilyOfElements F S.arrows // x.Compatible })
            f) :
        FamilyOfElements F S.arrows)
      ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) g)

Tactic:
dsimp [Presieve.FamilyOfElements.IsAmalgamation]

Premises used: CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
f : Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⟶ F
g : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F
⊢ Subfunctor.ι (shrinkFunctor.{w, v₁, u₁} S) ≫ g = f ↔
    ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
      Eq (α := F.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1.op) : (a : F.obj (op X)) → F.obj (op Y))
            ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) g : F.obj (op X)) :
          F.obj (op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
              (a :
                  { x : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y) //
                    S.arrows
                      ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) →
                F.obj (op Y))
            (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)) ↦
                S.arrows (Y := Y)
                  ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x))
                ((Equiv.symm shrinkYonedaObjObjEquiv : (a : Y ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) f_1)
                ⋯ :
              { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y) //
                S.arrows (Y := Y)
                  ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) :
          F.obj (op Y))

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

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
g : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Eq (α := F.obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) : (a : F.obj (op X)) → F.obj (op Y))
        ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) g : F.obj (op X)) :
      F.obj (op Y))
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app (Subfunctor.ι (shrinkFunctor.{w, v₁, u₁} S) ≫ g) (op Y)) :
            TypeCat.Fun
              { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y) //
                S.arrows (Y := Y)
                  ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }
              (F.obj (op Y))) :
          (a :
              { x : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y) //
                S.arrows ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) →
            F.obj (op Y))
        (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)) ↦
            S.arrows (Y := Y) ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x))
            ((Equiv.symm shrinkYonedaObjObjEquiv : (a : Y ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) f) ⋯ :
          { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y) //
            S.arrows (Y := Y)
              ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) :
      F.obj (op Y))

Tactic:
simp [shrinkYonedaEquiv_naturality, shrinkYonedaEquiv_comp, shrinkYonedaEquiv_shrinkYoneda_map]

Premises used: CategoryTheory.shrinkYonedaEquiv_comp, CategoryTheory.shrinkYonedaEquiv_naturality, CategoryTheory.shrinkYonedaEquiv_shrinkYoneda_map
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
f : Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⟶ F
g : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F
h :
  ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
    Eq (α := F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1.op) : (a : F.obj (op X)) → F.obj (op Y))
          ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) g : F.obj (op X)) :
        F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
            (a :
                { x : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y) //
                  S.arrows
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) →
              F.obj (op Y))
          (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)) ↦
              S.arrows (Y := Y)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x))
              ((Equiv.symm shrinkYonedaObjObjEquiv : (a : Y ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) f_1) ⋯ :
            { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y) //
              S.arrows (Y := Y)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) :
        F.obj (op Y))
refine_2 :
  ∀ (Y : Cᵒᵖ) (u : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y)
    (hu :
      Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
        (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) u),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Subfunctor.ι (shrinkFunctor.{w, v₁, u₁} S) ≫ g) Y))
        (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y) ↦
          Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
            (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) x)
          u hu) =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y)).toFun
        (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y) ↦
          Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
            (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) x)
          u hu)
⊢ Subfunctor.ι (shrinkFunctor.{w, v₁, u₁} S) ≫ g = f

Tactic:
ext Y ⟨u, hu⟩
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
f : Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⟶ F
g : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F
h :
  ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
    Eq (α := F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1.op) : (a : F.obj (op X)) → F.obj (op Y))
          ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) g : F.obj (op X)) :
        F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
            (a :
                { x : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y) //
                  S.arrows
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) →
              F.obj (op Y))
          (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)) ↦
              S.arrows (Y := Y)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x))
              ((Equiv.symm shrinkYonedaObjObjEquiv : (a : Y ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) f_1) ⋯ :
            { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y) //
              S.arrows (Y := Y)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) :
        F.obj (op Y))
Y : Cᵒᵖ
u : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y
hu :
  Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
    (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) u
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Subfunctor.ι (shrinkFunctor.{w, v₁, u₁} S) ≫ g) Y))
      (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y) ↦
        Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
          (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) x)
        u hu) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app (op (unop Y))) :
        (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v₁, u₁}.obj X).obj (op (unop Y)))) →
          (fun (X : Type w) ↦ X) (F.obj (op (unop Y))))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
            (a : unop (op (unop Y)) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op (unop Y)))
          ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X) u) :
        Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op (unop Y)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
f : Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⟶ F
g : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F
h :
  ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
    Eq (α := F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1.op) : (a : F.obj (op X)) → F.obj (op Y))
          ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) g : F.obj (op X)) :
        F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
            (a :
                { x : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y) //
                  S.arrows
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) →
              F.obj (op Y))
          (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)) ↦
              S.arrows (Y := Y)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x))
              ((Equiv.symm shrinkYonedaObjObjEquiv : (a : Y ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) f_1) ⋯ :
            { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y) //
              S.arrows (Y := Y)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) :
        F.obj (op Y))
Y : Cᵒᵖ
u : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y
hu :
  Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
    (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) u
h₁ : u = u
⊢ u =
    (Equiv.symm shrinkYonedaObjObjEquiv : (a : unop Y ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op (unop Y)))
      ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X) u)

Tactic:
rw! [Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
f : Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⟶ F
g : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F
h :
  ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
    Eq (α := F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1.op) : (a : F.obj (op X)) → F.obj (op Y))
          ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) g : F.obj (op X)) :
        F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
            (a :
                { x : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y) //
                  S.arrows
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) →
              F.obj (op Y))
          (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)) ↦
              S.arrows (Y := Y)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x))
              ((Equiv.symm shrinkYonedaObjObjEquiv : (a : Y ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) f_1) ⋯ :
            { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y) //
              S.arrows (Y := Y)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) :
        F.obj (op Y))
Y : Cᵒᵖ
u : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y
hu :
  Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
    (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) u
⊢ u = u

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
simp :
  (∀ (x : FamilyOfElements F S.arrows),
      x.Compatible (R := S.arrows) → ∃! t : F.obj (op X), x.IsAmalgamation (R := S.arrows) t) ↔
    ∀ (a : FamilyOfElements F S.arrows) (b : a.Compatible (R := S.arrows)),
      ∃! a_1 : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F,
        FamilyOfElements.IsAmalgamation.{w, v₁, u₁} (P := F) (R := S.arrows)
          (↑((shrinkFunctorHomEquiv :
                  (a : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F) →
                    { x : FamilyOfElements F S.arrows // x.Compatible })
                ((Equiv.symm shrinkFunctorHomEquiv :
                    (a : { x : FamilyOfElements F S.arrows // x.Compatible }) →
                      (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F)
                  (Subtype.mk (p := fun (a : FamilyOfElements F S.arrows) ↦ a.Compatible (R := S.arrows)) a b))) :
            FamilyOfElements F S.arrows)
          ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) a_1)
⊢ IsSheafFor F S.arrows ↔
    Function.Bijective (β :=
      Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⟶ F)
      fun (g : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F) ↦ Subfunctor.ι (shrinkFunctor.{w, v₁, u₁} S) ≫ g

Tactic:
simp only [IsSheafFor, Function.bijective_iff_existsUnique,
    shrinkFunctor_ι_comp_eq_iff_isAmalgamation, shrinkFunctorHomEquiv.forall_congr_left,
    Subtype.forall]

Premises used: CategoryTheory.Presieve.IsSheafFor, Equiv.forall_congr_left, Subtype.forall, CategoryTheory.Presieve.shrinkFunctorHomEquiv, CategoryTheory.Presieve.shrinkFunctor_ι_comp_eq_iff_isAmalgamation, Function.bijective_iff_existsUnique
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
x : FamilyOfElements F S.arrows
hx : x.Compatible (R := S.arrows)
⊢ (∃! t : F.obj (op X), x.IsAmalgamation (R := S.arrows) t) ↔
    ∃! a : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F,
      FamilyOfElements.IsAmalgamation.{w, v₁, u₁} (P := F) (R := S.arrows)
        (↑((shrinkFunctorHomEquiv :
                (a : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F) → { x : FamilyOfElements F S.arrows // x.Compatible })
              ((Equiv.symm shrinkFunctorHomEquiv :
                  (a : { x : FamilyOfElements F S.arrows // x.Compatible }) →
                    (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F)
                (Subtype.mk (p := fun (a : FamilyOfElements F S.arrows) ↦ a.Compatible (R := S.arrows)) x hx))) :
          FamilyOfElements F S.arrows)
        ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) a)

Tactic:
simp [Equiv.existsUnique_congr_right]

Premises used: Equiv.existsUnique_congr_right
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
⊢ (∀ (x : FamilyOfElements F S.arrows),
      x.Compatible (R := S.arrows) → ∃! t : F.obj (op X), x.IsAmalgamation (R := S.arrows) t) ↔
    ∀ (a : FamilyOfElements F S.arrows) (b : a.Compatible (R := S.arrows)),
      ∃! a_1 : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F,
        FamilyOfElements.IsAmalgamation.{w, v₁, u₁} (P := F) (R := S.arrows)
          (↑((shrinkFunctorHomEquiv :
                  (a : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F) →
                    { x : FamilyOfElements F S.arrows // x.Compatible })
                ((Equiv.symm shrinkFunctorHomEquiv :
                    (a : { x : FamilyOfElements F S.arrows // x.Compatible }) →
                      (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F)
                  (Subtype.mk (p := fun (a : FamilyOfElements F S.arrows) ↦ a.Compatible (R := S.arrows)) a b))) :
            FamilyOfElements F S.arrows)
          ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) a_1)

Tactic:
exact forall₂_congr fun x hx ↦ by simp [Equiv.existsUnique_congr_right]

Premises used: forall₂_congr
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
P : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
rw :
  (∀ (b : S.functor ⟶ P),
      ∃! a : Functor.obj shrinkYoneda.{v₁, v₁, u₁} X ⟶ P,
        Eq (α := Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) (shrinkFunctor.{v₁, v₁, u₁} S) ⟶ P)
          (Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫ a)
          ((Equiv.symm S.shrinkFunctorIsoFunctor.homFromEquiv :
              (a : S.functor ⟶ P) → (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor ⟶ P)
            b)) ↔
    ∀ (f : S.functor ⟶ P), ∃! g : Functor.obj yoneda X ⟶ P, S.functorInclusion ≫ g = f
⊢ IsSheafFor P S.arrows ↔ YonedaSheafCondition P S

Tactic:
rw [isSheafFor_iff_bijective_shrinkFunctor_ι_comp, YonedaSheafCondition,
    Function.bijective_iff_existsUnique,
    Equiv.forall_congr_left S.shrinkFunctorIsoFunctor.homFromEquiv]

Premises used: CategoryTheory.Presieve.YonedaSheafCondition, Equiv.forall_congr_left, CategoryTheory.Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp, CategoryTheory.Iso.homFromEquiv, Function.bijective_iff_existsUnique, CategoryTheory.Sieve.shrinkFunctorIsoFunctor
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
P : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
⊢ (∀ (b : S.functor ⟶ P),
      ∃! a : Functor.obj shrinkYoneda.{v₁, v₁, u₁} X ⟶ P,
        Eq (α := Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) (shrinkFunctor.{v₁, v₁, u₁} S) ⟶ P)
          (Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫ a)
          ((Equiv.symm S.shrinkFunctorIsoFunctor.homFromEquiv :
              (a : S.functor ⟶ P) → (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor ⟶ P)
            b)) ↔
    ∀ (f : S.functor ⟶ P), ∃! g : Functor.obj yoneda X ⟶ P, S.functorInclusion ≫ g = f

Tactic:
forall_congr' fun a ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
P : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
refine :
  ∀ (a : S.functor ⟶ P),
    (∃! a_1 : Functor.obj shrinkYoneda.{v₁, v₁, u₁} X ⟶ P,
        Eq (α := Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) (shrinkFunctor.{v₁, v₁, u₁} S) ⟶ P)
          (Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫ a_1)
          ((Equiv.symm S.shrinkFunctorIsoFunctor.homFromEquiv :
              (a : S.functor ⟶ P) → (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor ⟶ P)
            a)) ↔
      ∃! g : Functor.obj yoneda X ⟶ P, S.functorInclusion ≫ g = a
⊢ (∀ (b : S.functor ⟶ P),
      ∃! a : Functor.obj shrinkYoneda.{v₁, v₁, u₁} X ⟶ P,
        Eq (α := Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) (shrinkFunctor.{v₁, v₁, u₁} S) ⟶ P)
          (Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫ a)
          ((Equiv.symm S.shrinkFunctorIsoFunctor.homFromEquiv :
              (a : S.functor ⟶ P) → (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor ⟶ P)
            b)) ↔
    ∀ (f : S.functor ⟶ P), ∃! g : Functor.obj yoneda X ⟶ P, S.functorInclusion ≫ g = f

Tactic:
refine forall_congr' fun a ↦ ?_

Premises used: forall_congr'