awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
hR : IsSeparatedFor P R
t₁ t₂ : P.obj (op X)
h :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R f →
      Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Y)))
            t₁ :
          (fun (X : Type w) ↦ X) (P.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Y)))
            t₂ :
          (fun (X : Type w) ↦ X) (P.obj (op Y)))
⊢ t₁ = t₂

Tactic:
hR (fun _ f _ => P.map f.op t₂) t₁ t₂ (fun _ _ hf => h hf) fun _ _ _ => rfl

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, DFunLike.coe, rfl
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
mp : IsSeparatedFor P R → IsSeparatedFor P (generate R).arrows
mpr : IsSeparatedFor P (generate R).arrows → IsSeparatedFor P R
⊢ IsSeparatedFor P R ↔ IsSeparatedFor P (generate R).arrows

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
h : IsSeparatedFor P R
x : FamilyOfElements P (generate R).arrows
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation (R := (generate R).arrows) t₁
ht₂ : x.IsAmalgamation (R := (generate R).arrows) t₂
apply : (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x).IsAmalgamation (R := R) t₁
apply₁ : (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x).IsAmalgamation (R := R) t₂
⊢ t₁ = t₂

Tactic:
apply h (x.restrict (le_generate R)) t₁ t₂ _ _

Premises used: CategoryTheory.Sieve.le_generate, CategoryTheory.Presieve.FamilyOfElements.restrict
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
h : IsSeparatedFor P R
x : FamilyOfElements P (generate R).arrows
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation (R := (generate R).arrows) t₁
ht₂ : x.IsAmalgamation (R := (generate R).arrows) t₂
⊢ (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x).IsAmalgamation (R := R) t₁

Tactic:
isAmalgamation_restrict _ x t₁ ht₁

Premises used: CategoryTheory.Presieve.isAmalgamation_restrict
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
h : IsSeparatedFor P R
x : FamilyOfElements P (generate R).arrows
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation (R := (generate R).arrows) t₁
ht₂ : x.IsAmalgamation (R := (generate R).arrows) t₂
⊢ (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x).IsAmalgamation (R := R) t₁

Tactic:
exact isAmalgamation_restrict _ x t₁ ht₁

Premises used: CategoryTheory.Presieve.isAmalgamation_restrict
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
h : IsSeparatedFor P R
x : FamilyOfElements P (generate R).arrows
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation (R := (generate R).arrows) t₁
ht₂ : x.IsAmalgamation (R := (generate R).arrows) t₂
⊢ (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x).IsAmalgamation (R := R) t₂

Tactic:
isAmalgamation_restrict _ x t₂ ht₂

Premises used: CategoryTheory.Presieve.isAmalgamation_restrict
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
h : IsSeparatedFor P R
x : FamilyOfElements P (generate R).arrows
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation (R := (generate R).arrows) t₁
ht₂ : x.IsAmalgamation (R := (generate R).arrows) t₂
⊢ (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x).IsAmalgamation (R := R) t₂

Tactic:
exact isAmalgamation_restrict _ x t₂ ht₂

Premises used: CategoryTheory.Presieve.isAmalgamation_restrict
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
h : IsSeparatedFor P (generate R).arrows
x : FamilyOfElements P R
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation (R := R) t₁
ht₂ : x.IsAmalgamation (R := R) t₂
mpr : x.sieveExtend (R := R).IsAmalgamation (R := (generate R).arrows) t₁
mpr₁ : x.sieveExtend (R := R).IsAmalgamation (R := (generate R).arrows) t₂
⊢ t₁ = t₂

Tactic:
apply h x.sieveExtend

Premises used: CategoryTheory.Presieve.FamilyOfElements.sieveExtend
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
h : IsSeparatedFor P (generate R).arrows
x : FamilyOfElements P R
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation (R := R) t₁
ht₂ : x.IsAmalgamation (R := R) t₂
⊢ x.sieveExtend (R := R).IsAmalgamation (R := (generate R).arrows) t₁

Tactic:
isAmalgamation_sieveExtend x t₁ ht₁

Premises used: CategoryTheory.Presieve.isAmalgamation_sieveExtend
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
h : IsSeparatedFor P (generate R).arrows
x : FamilyOfElements P R
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation (R := R) t₁
ht₂ : x.IsAmalgamation (R := R) t₂
⊢ x.sieveExtend (R := R).IsAmalgamation (R := (generate R).arrows) t₁

Tactic:
exact isAmalgamation_sieveExtend x t₁ ht₁

Premises used: CategoryTheory.Presieve.isAmalgamation_sieveExtend
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
h : IsSeparatedFor P (generate R).arrows
x : FamilyOfElements P R
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation (R := R) t₁
ht₂ : x.IsAmalgamation (R := R) t₂
⊢ x.sieveExtend (R := R).IsAmalgamation (R := (generate R).arrows) t₂

Tactic:
isAmalgamation_sieveExtend x t₂ ht₂

Premises used: CategoryTheory.Presieve.isAmalgamation_sieveExtend
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
h : IsSeparatedFor P (generate R).arrows
x : FamilyOfElements P R
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation (R := R) t₁
ht₂ : x.IsAmalgamation (R := R) t₂
⊢ x.sieveExtend (R := R).IsAmalgamation (R := (generate R).arrows) t₂

Tactic:
exact isAmalgamation_sieveExtend x t₂ ht₂

Premises used: CategoryTheory.Presieve.isAmalgamation_sieveExtend
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
x : FamilyOfElements (X := X) P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation (R := ⊤) t₁
h₂ : x.IsAmalgamation (R := ⊤) t₂
⊢ ⊤ (𝟙 X)

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
x : FamilyOfElements (X := X) P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation (R := ⊤) t₁
h₂ : x.IsAmalgamation (R := ⊤) t₂
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (𝟙 X))) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
      t₁ =
    x (𝟙 X) trivial

Tactic:
have q₁ := h₁ (𝟙 X) (by tauto)
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
x : FamilyOfElements (X := X) P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation (R := ⊤) t₁
h₂ : x.IsAmalgamation (R := ⊤) t₂
q₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (𝟙 X))) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
      t₁ =
    x (𝟙 X) trivial
⊢ ⊤ (𝟙 X)

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
x : FamilyOfElements (X := X) P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation (R := ⊤) t₁
h₂ : x.IsAmalgamation (R := ⊤) t₂
q₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (𝟙 X))) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
      t₁ =
    x (𝟙 X) trivial
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (𝟙 X))) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
      t₂ =
    x (𝟙 X) trivial

Tactic:
have q₂ := h₂ (𝟙 X) (by tauto)
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
x : FamilyOfElements (X := X) P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation (R := ⊤) t₁
h₂ : x.IsAmalgamation (R := ⊤) t₂
q₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (𝟙 X))) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
      t₁ =
    x (𝟙 X) trivial
q₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (𝟙 X))) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
      t₂ =
    x (𝟙 X) trivial
⊢ t₁ = x (𝟙 X) trivial

Tactic:
simp only [op_id, Functor.map_id, id_apply] at q₁ q₂

Premises used: CategoryTheory.id_apply, CategoryTheory.Functor.map_id, CategoryTheory.op_id
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
x : FamilyOfElements (X := X) P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation (R := ⊤) t₁
h₂ : x.IsAmalgamation (R := ⊤) t₂
q₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (𝟙 X))) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
      t₁ =
    x (𝟙 X) trivial
q₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (𝟙 X))) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op X)))
      t₂ =
    x (𝟙 X) trivial
q₃ : t₁ = x (𝟙 X) trivial
⊢ t₂ = x (𝟙 X) trivial

Tactic:
simp only [op_id, Functor.map_id, id_apply] at q₁ q₂

Premises used: CategoryTheory.id_apply, CategoryTheory.Functor.map_id, CategoryTheory.op_id
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
x : FamilyOfElements (X := X) P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation (R := ⊤) t₁
h₂ : x.IsAmalgamation (R := ⊤) t₂
q₁ : t₁ = x (𝟙 X) trivial
q₂ : t₂ = x (𝟙 X) trivial
rw : x (𝟙 X) trivial = t₂
rw₁ rw₂ : x (𝟙 X) trivial = x (𝟙 X) trivial
⊢ t₁ = t₂

Tactic:
rw [q₁, q₂]
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y_1 : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
t : Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⟶ F
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Membership.mem.{w, w} (α := Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)) (γ :=
    Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)))
    (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) (op Y))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op Y) ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) f :
      Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y))

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
t : Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⟶ F
rw :
  FamilyOfElements.SieveCompatible.{w, v₁, u₁} (C := C) (P := F) (X := X) (S := S)
    fun (Y : C) (f : Y ⟶ X) (hf : S.arrows f) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (t.app (op Y)) :
        (a : (fun (X : Type w) ↦ X) ((shrinkFunctor.{w, v₁, u₁} S).toFunctor.obj (op Y))) →
          (fun (X : Type w) ↦ 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)) ↦
          Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)))
            (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) (op Y)) x)
          ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op 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) //
          Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)))
            (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) (op Y)) x })
⊢ FamilyOfElements.Compatible.{w, v₁, u₁} (P := F) (R := S.arrows) fun (Y : C) (f : Y ⟶ X) (hf : S.arrows f) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (t.app (op Y)) :
        (a : (fun (X : Type w) ↦ X) ((shrinkFunctor.{w, v₁, u₁} S).toFunctor.obj (op Y))) →
          (fun (X : Type w) ↦ 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)) ↦
          Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)))
            (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) (op Y)) x)
          ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op 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) //
          Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)))
            (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) (op Y)) x })

Tactic:
rw [Presieve.compatible_iff_sieveCompatible]

Premises used: CategoryTheory.Presieve.compatible_iff_sieveCompatible
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y_1 : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
t : { x : FamilyOfElements F S.arrows // x.Compatible (R := S.arrows) }
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))
    (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) f
h :
  (↑t : FamilyOfElements F S.arrows)
      ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Z) → unop Z ⟶ X)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{w, v₁, u₁} X) g) :
            (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj Z)
          f))
      ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) : (a : F.obj Y) → F.obj Z)
      ((↑t : FamilyOfElements F S.arrows)
        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X) f) ⋯)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S)).map g ≫
          ↾fun
              (f :
                (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S)).obj
                  Z) ↦
            (↑t : FamilyOfElements F S.arrows)
              ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Z) → unop Z ⟶ X)
                (↑f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Z))
              ⋯))
      (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)
        f hf) =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun
              (f :
                (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S)).obj
                  Y) ↦
            (↑t : FamilyOfElements F S.arrows)
              ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X)
                (↑f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y))
              ⋯) ≫
          F.map g))
      (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)
        f hf)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y_1 : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
t : { x : FamilyOfElements F S.arrows // x.Compatible (R := S.arrows) }
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))
    (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) f
⊢ (↑t : FamilyOfElements F S.arrows)
      (unop g ≫ (shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X) f) ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (unop g).op) :
        (a : (fun (X : Type w) ↦ X) (F.obj (op (unop Y)))) → (fun (X : Type w) ↦ X) (F.obj (op (unop Z))))
      ((↑t : FamilyOfElements F S.arrows)
        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X) f) ⋯)

Tactic:
t.2.to_sieveCompatible _ _ _

Premises used: CategoryTheory.Presieve.FamilyOfElements.Compatible.to_sieveCompatible, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y_1 : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
t : { x : FamilyOfElements F S.arrows // x.Compatible (R := S.arrows) }
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))
    (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) f
h :
  F.obj Z = F.obj (op (unop Z)) →
    Eq.{v₁ + 1} (α := unop Z ⟶ X)
      ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Z) → unop Z ⟶ X)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{w, v₁, u₁} X) g) :
              (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj Z)
            f) :
        unop Z ⟶ X)
      (unop g ≫ (shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X) f : unop Z ⟶ X)
⊢ (↑t : FamilyOfElements F S.arrows)
      ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Z) → unop Z ⟶ X)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{w, v₁, u₁} X) g) :
            (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj Z)
          f))
      ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) : (a : F.obj Y) → F.obj Z)
      ((↑t : FamilyOfElements F S.arrows)
        ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X) f) ⋯)

Tactic:
convert! t.2.to_sieveCompatible _ _ _

Premises used: CategoryTheory.Presieve.FamilyOfElements.Compatible.to_sieveCompatible, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y_1 : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
t : { x : FamilyOfElements F S.arrows // x.Compatible (R := S.arrows) }
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))
    (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) f
e_1 : F.obj Z = F.obj (op (unop Z))
h :
  Eq (α := unop Z ⟶ X)
    (g.unop ≫ (shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X) f)
    (unop g ≫ (shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X) f)
⊢ Eq.{v₁ + 1} (α := unop Z ⟶ X)
    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Z) → unop Z ⟶ X)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{w, v₁, u₁} X) g) :
            (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj Z)
          f) :
      unop Z ⟶ X)
    (unop g ≫ (shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X) f : unop Z ⟶ X)

Tactic:
simp only [Opposite.op_unop, shrinkYonedaObjObjEquiv_obj_map]

Premises used: Opposite.op_unop, CategoryTheory.shrinkYonedaObjObjEquiv_obj_map
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y_1 : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
t : { x : FamilyOfElements F S.arrows // x.Compatible (R := S.arrows) }
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))
    (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) f
e_1 : F.obj Z = F.obj (op (unop Z))
⊢ Eq (α := unop Z ⟶ X)
    (g.unop ≫ (shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X) f)
    (unop g ≫ (shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X) f)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
x : { x : FamilyOfElements F S.arrows // x.Compatible (R := S.arrows) }
Y_1 : C
f : Y_1 ⟶ X
hf : S.arrows f
a : (↑x : FamilyOfElements F S.arrows) f ⋯ = (↑x : FamilyOfElements F S.arrows) f hf
⊢ (↑x : FamilyOfElements F S.arrows)
      ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y_1)) → Y_1 ⟶ X)
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : Y_1 ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y_1)) f))
      ⋯ =
    (↑x : FamilyOfElements F S.arrows) f hf

Tactic:
rw! [Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q U : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X Y : C
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
x : { x : FamilyOfElements F S.arrows // x.Compatible (R := S.arrows) }
Y_1 : C
f : Y_1 ⟶ X
hf : S.arrows f
⊢ (↑x : FamilyOfElements F S.arrows) f ⋯ = (↑x : FamilyOfElements F S.arrows) f hf

Tactic:
simp