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
x : FamilyOfElements P R
hx : x.Compatible (R := R)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : (generate R).arrows f₁
h₂ : (generate R).arrows f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (g₁ ≫
        ⋯.choose (p :=
          fun (h : Y₁ ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₁ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₁) h₁) ↦
          ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₁ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₁) h₁ ⟶ X),
            R g ∧ h ≫ g = f₁)) ≫
      ⋯.choose (p := fun (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₁ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₁) h₁ ⟶ X) ↦
        R g ∧
          ⋯.choose (p :=
                fun (h : Y₁ ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₁ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₁) h₁) ↦
                ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₁ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₁) h₁ ⟶ X),
                  R g ∧ h ≫ g = f₁) ≫
              g =
            f₁) =
    (g₂ ≫
        ⋯.choose (p :=
          fun (h : Y₂ ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₂ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₂) h₂) ↦
          ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₂ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₂) h₂ ⟶ X),
            R g ∧ h ≫ g = f₂)) ≫
      ⋯.choose (p := fun (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₂ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₂) h₂ ⟶ X) ↦
        R g ∧
          ⋯.choose (p :=
                fun (h : Y₂ ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₂ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₂) h₂) ↦
                ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : Y₂ ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f₂) h₂ ⟶ X),
                  R g ∧ h ≫ g = f₂) ≫
              g =
            f₂)

Tactic:
simp [comm, h₁.choose_spec.choose_spec.choose_spec.2, h₂.choose_spec.choose_spec.choose_spec.2]

Premises used: Exists.choose_spec, And.right
-- 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 Y : C
R : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
t : x.Compatible (R := R)
f : Y ⟶ X
hf : R f
⊢ ∃ (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) (g :
    Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X), R g ∧ h ≫ g = f

Tactic:
have h := (le_generate R Y _ hf).choose_spec
-- 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 Y : C
R : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
t : x.Compatible (R := R)
f : Y ⟶ X
hf : R f
h :
  ∃ (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) (g :
    Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X), R g ∧ h ≫ g = f
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (𝟙 Y))) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op Y))) → (fun (X : Type w) ↦ X) (P.obj (op Y)))
      (x f hf) =
    x f hf
rw₁ :
  h.choose (p := fun (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) ↦
        ∃ (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X),
          R g ∧ h ≫ g = f) ≫
      ⋯.choose (p :=
        fun (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X) ↦
        R g ∧
          ⋯.choose (p :=
                fun (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) ↦
                ∃ (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X),
                  R g ∧ h ≫ g = f) ≫
              g =
            f) =
    𝟙 Y ≫ f
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (P.map
            ⋯.choose (p :=
                fun (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) ↦
                ∃ (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X),
                  R g ∧ h ≫ g = f).op) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op (Exists.choose ⋯)))) → (fun (X : Type w) ↦ X) (P.obj (op Y)))
      (x
        (⋯.choose (p :=
          fun (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X) ↦
          R g ∧
            ⋯.choose (p :=
                  fun (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) ↦
                  ∃ (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X),
                    R g ∧ h ≫ g = f) ≫
                g =
              f))
        ⋯) =
    x f hf

Tactic:
rw [t h.choose (𝟙 _) _ hf _]

Premises used: CategoryTheory.CategoryStruct.id, Exists.choose
-- 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 Y : C
R : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
t : x.Compatible (R := R)
f : Y ⟶ X
hf : R f
h :
  ∃ (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) (g :
    Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X), R g ∧ h ≫ g = f
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (𝟙 Y))) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op Y))) → (fun (X : Type w) ↦ X) (P.obj (op Y)))
      (x f hf) =
    x f hf

Tactic:
simp
-- 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 Y : C
R : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
t : x.Compatible (R := R)
f : Y ⟶ X
hf : R f
h :
  ∃ (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) (g :
    Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X), R g ∧ h ≫ g = f
rw :
  h.choose (p := fun (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) ↦
        ∃ (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X),
          R g ∧ h ≫ g = f) ≫
      ⋯.choose (p :=
        fun (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X) ↦
        R g ∧
          ⋯.choose (p :=
                fun (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) ↦
                ∃ (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X),
                  R g ∧ h ≫ g = f) ≫
              g =
            f) =
    f
⊢ h.choose (p := fun (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) ↦
        ∃ (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X),
          R g ∧ h ≫ g = f) ≫
      ⋯.choose (p :=
        fun (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X) ↦
        R g ∧
          ⋯.choose (p :=
                fun (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) ↦
                ∃ (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X),
                  R g ∧ h ≫ g = f) ≫
              g =
            f) =
    𝟙 Y ≫ f

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- 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 Y : C
R : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
t : x.Compatible (R := R)
f : Y ⟶ X
hf : R f
h :
  ∃ (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) (g :
    Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X), R g ∧ h ≫ g = f
⊢ h.choose (p := fun (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) ↦
        ∃ (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X),
          R g ∧ h ≫ g = f) ≫
      ⋯.choose (p :=
        fun (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X) ↦
        R g ∧
          ⋯.choose (p :=
                fun (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) ↦
                ∃ (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X),
                  R g ∧ h ≫ g = f) ≫
              g =
            f) =
    f

Tactic:
h.choose_spec.choose_spec.2

Premises used: Exists.choose_spec, And.right
-- 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 Y : C
R : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
t : x.Compatible (R := R)
f : Y ⟶ X
hf : R f
h :
  ∃ (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) (g :
    Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X), R g ∧ h ≫ g = f
⊢ h.choose (p := fun (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) ↦
        ∃ (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X),
          R g ∧ h ≫ g = f) ≫
      ⋯.choose (p :=
        fun (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X) ↦
        R g ∧
          ⋯.choose (p :=
                fun (h : Y ⟶ Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯) ↦
                ∃ (g : Exists.choose (p := fun (Y_1 : C) ↦ ∃ (h : Y ⟶ Y_1) (g : Y_1 ⟶ X), R g ∧ h ≫ g = f) ⋯ ⟶ X),
                  R g ∧ h ≫ g = f) ≫
              g =
            f) =
    f

Tactic:
exact h.choose_spec.choose_spec.2

Premises used: Exists.choose_spec, And.right
-- 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
x : FamilyOfElements P R
t : x.Compatible (R := R)
h :
  ∀ (Y : C) (f : Y ⟶ X) (hf : R f),
    FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ (x.sieveExtend (R := R)) f hf = x f hf
⊢ FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ (x.sieveExtend (R := R)) = x

Tactic:
funext Y f hf
-- 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
x : FamilyOfElements P R
t : x.Compatible (R := R)
Y : C
f : Y ⟶ X
hf : R f
⊢ FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ (x.sieveExtend (R := R)) f hf = x f hf

Tactic:
extend_agrees t hf

Premises used: CategoryTheory.Presieve.extend_agrees, 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
x : FamilyOfElements P R
t : x.Compatible (R := R)
Y : C
f : Y ⟶ X
hf : R f
⊢ FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ (x.sieveExtend (R := R)) f hf = x f hf

Tactic:
exact extend_agrees t hf

Premises used: CategoryTheory.Presieve.extend_agrees
-- 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
S : Sieve.{v₁, u₁} X
x : FamilyOfElements P S.arrows
mp : x.Compatible (R := S.arrows) → x.SieveCompatible
mpr : x.SieveCompatible → x.Compatible (R := S.arrows)
⊢ x.Compatible (R := S.arrows) ↔ x.SieveCompatible

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
S : Sieve.{v₁, u₁} X
x : FamilyOfElements P S.arrows
h : x.Compatible (R := S.arrows)
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ x (g ≫ f) ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op Y))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
      (x f hf)

Tactic:
simpa using h (𝟙 _) g (S.downward_closed hf g) hf (id_comp _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Sieve.downward_closed, CategoryTheory.Category.id_comp
-- 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
S : Sieve.{v₁, u₁} X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S.arrows f₁
h₂ : S.arrows f₂
k : g₁ ≫ f₁ = g₂ ≫ f₂
mpr : x (g₁ ≫ f₁) ⋯ = x (g₂ ≫ f₂) ⋯
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f₁ h₁) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f₂ h₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
simp_rw [← h f₁ g₁ h₁, ← h f₂ g₂ h₂]
-- 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
S : Sieve.{v₁, u₁} X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S.arrows f₁
h₂ : S.arrows f₂
k : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ x (g₁ ≫ f₁) ⋯ = x (g₂ ≫ f₂) ⋯

Tactic:
congr
-- 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
S : Sieve.{v₁, u₁} X
x : FamilyOfElements P S.arrows
t : x.Compatible (R := S.arrows)
⊢ x.SieveCompatible

Tactic:
(compatible_iff_sieveCompatible x).1 t

Premises used: Iff.mp, CategoryTheory.Presieve.compatible_iff_sieveCompatible
-- 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
x : FamilyOfElements P (generate R).arrows
t : x.Compatible (R := (generate R).arrows)
⊢ x.SieveCompatible

Tactic:
rw [compatible_iff_sieveCompatible] at t

Premises used: CategoryTheory.Presieve.compatible_iff_sieveCompatible
-- 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
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
h :
  ∀ (x_1 : C) (x_2 : x_1 ⟶ X) (h : (generate R).arrows x_2),
    (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x).sieveExtend (R := R) x_2 h = x x_2 h
⊢ (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x).sieveExtend (R := R) = x

Tactic:
funext _ _ h
-- 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
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
x_1 : C
x_2 : x_1 ⟶ X
h : (generate R).arrows x_2
h₁ :
  x
      (⋯.choose (p :=
          fun (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
          ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
            R g ∧ h_1 ≫ g = x_2) ≫
        ⋯.choose (p :=
          fun (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X) ↦
          R g ∧
            ⋯.choose (p :=
                  fun
                    (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
                  ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
                    R g ∧ h_1 ≫ g = x_2) ≫
                g =
              x_2))
      ⋯ =
    x x_2 h
⊢ (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x).sieveExtend (R := R) x_2 h = x x_2 h

Tactic:
apply (t _ _ _).symm.trans

Premises used: Eq.symm, Eq.trans
-- 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
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
x_1 : C
x_2 : x_1 ⟶ X
h : (generate R).arrows x_2
h₁ :
  ⋯.choose (p := fun (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
        ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
          R g ∧ h_1 ≫ g = x_2) ≫
      ⋯.choose (p := fun (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X) ↦
        R g ∧
          ⋯.choose (p :=
                fun (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
                ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
                  R g ∧ h_1 ≫ g = x_2) ≫
              g =
            x_2) =
    x_2
⊢ x
      (⋯.choose (p :=
          fun (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
          ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
            R g ∧ h_1 ≫ g = x_2) ≫
        ⋯.choose (p :=
          fun (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X) ↦
          R g ∧
            ⋯.choose (p :=
                  fun
                    (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
                  ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
                    R g ∧ h_1 ≫ g = x_2) ≫
                g =
              x_2))
      ⋯ =
    x x_2 h

Tactic:
congr
-- 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
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
x_1 : C
x_2 : x_1 ⟶ X
h : (generate R).arrows x_2
⊢ ⋯.choose (p := fun (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
        ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
          R g ∧ h_1 ≫ g = x_2) ≫
      ⋯.choose (p := fun (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X) ↦
        R g ∧
          ⋯.choose (p :=
                fun (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
                ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
                  R g ∧ h_1 ≫ g = x_2) ≫
              g =
            x_2) =
    x_2

Tactic:
h.choose_spec.choose_spec.choose_spec.2

Premises used: Exists.choose_spec, And.right
-- 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
x : FamilyOfElements P (generate R).arrows
t : x.SieveCompatible
x_1 : C
x_2 : x_1 ⟶ X
h : (generate R).arrows x_2
⊢ ⋯.choose (p := fun (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
        ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
          R g ∧ h_1 ≫ g = x_2) ≫
      ⋯.choose (p := fun (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X) ↦
        R g ∧
          ⋯.choose (p :=
                fun (h_1 : x_1 ⟶ Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h) ↦
                ∃ (g : Exists.choose (p := fun (Y : C) ↦ ∃ (h : x_1 ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = x_2) h ⟶ X),
                  R g ∧ h_1 ≫ g = x_2) ≫
              g =
            x_2) =
    x_2

Tactic:
exact h.choose_spec.choose_spec.choose_spec.2

Premises used: Exists.choose_spec, And.right
-- 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
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : x₁.Compatible (R := (generate R).arrows)
t₂ : x₂.Compatible (R := (generate R).arrows)
h :
  FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x₁ =
    FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x₂
rw :
  (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x₁).sieveExtend (R := R) =
    (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x₂).sieveExtend (R := R)
⊢ x₁ = x₂

Tactic:
rw [← extend_restrict t₁, ← extend_restrict t₂]

Premises used: CategoryTheory.Presieve.extend_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
x₁ x₂ : FamilyOfElements P (generate R).arrows
t₁ : x₁.Compatible (R := (generate R).arrows)
t₂ : x₂.Compatible (R := (generate R).arrows)
h :
  FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x₁ =
    FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x₂
⊢ (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x₁).sieveExtend (R := R) =
    (FamilyOfElements.restrict (R₁ := R) (R₂ := (generate R).arrows) ⋯ x₂).sieveExtend (R := R)

Tactic:
congr
-- 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 Y : C
S : Sieve.{v₁, u₁} X
x : FamilyOfElements P S.arrows
t : x.Compatible (R := S.arrows)
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ x (g ≫ f) ⋯ =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op Y))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
      (x f hf)

Tactic:
simpa using t (𝟙 _) g (S.downward_closed hf g) hf (id_comp _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Sieve.downward_closed, CategoryTheory.Category.id_comp
-- 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 Y : C
f : X ⟶ Y
x : FamilyOfElements P (singleton f)
⊢ x.Compatible (R := singleton f) ↔
    ∀ {Z : C} (p₁ p₂ : Z ⟶ X),
      p₁ ≫ f = p₂ ≫ f →
        Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₁.op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
              (x f ⋯) :
            (fun (X : Type w) ↦ X) (P.obj (op Z)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map p₂.op) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
              (x f ⋯) :
            (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
⟨fun H Z p₁ p₂ h ↦ H _ _ _ _ h, fun H Y₁ Y₂ Z g₁ g₂ f₁ f₂ ↦ ?_⟩

Premises used: CategoryTheory.Presieve.singleton.mk, Iff.intro