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)
P₂ : Functor.{v₁, w', u₁, w' + 1} Cᵒᵖ (Type w')
e : ⦃X : C⦄ → Equiv.{w + 1, w' + 1} (P₁.obj (op X)) (P₂.obj (op X))
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    Eq.{w' + 1} (α := P₂.obj (op X))
      ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
            x) :
        P₂.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) x : P₂.obj (op Y)) :
        (fun (X : Type w') ↦ X) (P₂.obj (op X)))
X_1 : C
R : Presieve.{v₁, u₁} X_1
h : IsSheafFor P₂ R
X Y : C
f : X ⟶ Y
x : P₂.obj (op Y)
obtain :
  ∀ (y : P₁.obj (op Y)),
    Eq.{w + 1} (α := P₁.obj (op X))
      ((((fun (x : C) ↦ (Equiv.symm e : Equiv.{w' + 1, w + 1} (P₂.obj (op x)) (P₁.obj (op x)))) X :
              Equiv.{w' + 1, w + 1} (P₂.obj (op X)) (P₁.obj (op X))) :
            (a : P₂.obj (op X)) → P₁.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
              (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
            ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) y : P₂.obj (op Y))) :
        P₁.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
            (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
          ((((fun (x : C) ↦ (Equiv.symm e : Equiv.{w' + 1, w + 1} (P₂.obj (op x)) (P₁.obj (op x)))) Y :
                  Equiv.{w' + 1, w + 1} (P₂.obj (op Y)) (P₁.obj (op Y))) :
                (a : P₂.obj (op Y)) → P₁.obj (op Y))
              ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) y) :
            P₁.obj (op Y)) :
        (fun (X : Type w) ↦ X) (P₁.obj (op X)))
⊢ Eq.{w + 1} (α := P₁.obj (op X))
    ((((fun (x : C) ↦ (Equiv.symm e : Equiv.{w' + 1, w + 1} (P₂.obj (op x)) (P₁.obj (op x)))) X :
            Equiv.{w' + 1, w + 1} (P₂.obj (op X)) (P₁.obj (op X))) :
          (a : P₂.obj (op X)) → P₁.obj (op X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          x) :
      P₁.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
          (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
        ((((fun (x : C) ↦ (Equiv.symm e : Equiv.{w' + 1, w + 1} (P₂.obj (op x)) (P₁.obj (op x)))) Y :
                Equiv.{w' + 1, w + 1} (P₂.obj (op Y)) (P₁.obj (op Y))) :
              (a : P₂.obj (op Y)) → P₁.obj (op Y))
            x :
          P₁.obj (op Y)) :
      (fun (X : Type w) ↦ X) (P₁.obj (op X)))

Tactic:
obtain ⟨y, rfl⟩ := e.surjective x

Premises used: Equiv.surjective, 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)
P₂ : Functor.{v₁, w', u₁, w' + 1} Cᵒᵖ (Type w')
e : ⦃X : C⦄ → Equiv.{w + 1, w' + 1} (P₁.obj (op X)) (P₂.obj (op X))
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    Eq.{w' + 1} (α := P₂.obj (op X))
      ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
            x) :
        P₂.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) x : P₂.obj (op Y)) :
        (fun (X : Type w') ↦ X) (P₂.obj (op X)))
X_1 : C
R : Presieve.{v₁, u₁} X_1
h : IsSheafFor P₂ R
X Y : C
f : X ⟶ Y
y : P₁.obj (op Y)
⊢ Eq.{w + 1} (α := P₁.obj (op X))
    ((((fun (x : C) ↦ (Equiv.symm e : Equiv.{w' + 1, w + 1} (P₂.obj (op x)) (P₁.obj (op x)))) X :
            Equiv.{w' + 1, w + 1} (P₂.obj (op X)) (P₁.obj (op X))) :
          (a : P₂.obj (op X)) → P₁.obj (op X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) y : P₂.obj (op Y))) :
      P₁.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
          (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
        ((((fun (x : C) ↦ (Equiv.symm e : Equiv.{w' + 1, w + 1} (P₂.obj (op x)) (P₁.obj (op x)))) Y :
                Equiv.{w' + 1, w + 1} (P₂.obj (op Y)) (P₁.obj (op Y))) :
              (a : P₂.obj (op Y)) → P₁.obj (op Y))
            ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) y) :
          P₁.obj (op Y)) :
      (fun (X : Type w) ↦ X) (P₁.obj (op X)))

Tactic:
e.injective ?_

Premises used: Equiv.injective
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P₁ : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
P₂ : Functor.{v₁, w', u₁, w' + 1} Cᵒᵖ (Type w')
e : ⦃X : C⦄ → Equiv.{w + 1, w' + 1} (P₁.obj (op X)) (P₂.obj (op X))
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    Eq.{w' + 1} (α := P₂.obj (op X))
      ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
              (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
            x) :
        P₂.obj (op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
            (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
          ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) x : P₂.obj (op Y)) :
        (fun (X : Type w') ↦ X) (P₂.obj (op X)))
X_1 : C
R : Presieve.{v₁, u₁} X_1
h : IsSheafFor P₂ R
X Y : C
f : X ⟶ Y
y : P₁.obj (op Y)
⊢ Eq.{w' + 1} (α := P₂.obj (op X))
    ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
        ((((fun (x : C) ↦ (Equiv.symm e : Equiv.{w' + 1, w + 1} (P₂.obj (op x)) (P₁.obj (op x)))) X :
              Equiv.{w' + 1, w + 1} (P₂.obj (op X)) (P₁.obj (op X))) :
            (a : P₂.obj (op X)) → P₁.obj (op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₂.map f.op) :
              (a : (fun (X : Type w') ↦ X) (P₂.obj (op Y))) → (fun (X : Type w') ↦ X) (P₂.obj (op X)))
            ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) y : P₂.obj (op Y)))) :
      P₂.obj (op X))
    ((e : (a : P₁.obj (op X)) → P₂.obj (op X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P₁.map f.op) :
            (a : (fun (X : Type w) ↦ X) (P₁.obj (op Y))) → (fun (X : Type w) ↦ X) (P₁.obj (op X)))
          ((((fun (x : C) ↦ (Equiv.symm e : Equiv.{w' + 1, w + 1} (P₂.obj (op x)) (P₁.obj (op x)))) Y :
                  Equiv.{w' + 1, w + 1} (P₂.obj (op Y)) (P₁.obj (op Y))) :
                (a : P₂.obj (op Y)) → P₁.obj (op Y))
              ((e : (a : P₁.obj (op Y)) → P₂.obj (op Y)) y) :
            P₁.obj (op Y))) :
      P₂.obj (op X))

Tactic:
simp only [Equiv.apply_symm_apply, Equiv.symm_apply_apply, he]

Premises used: Equiv.apply_symm_apply, Equiv.symm_apply_apply
-- 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
P' : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
i : P ≅ P'
hP : IsSheafFor P R
⊢ IsSheafFor P' R

Tactic:
isSheafFor_of_nat_equiv (fun X ↦ (i.app (op X)).toEquiv)
    (fun _ _ f x ↦ ConcreteCategory.congr_hom (i.hom.naturality f.op) x) hP

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.Presieve.isSheafFor_of_nat_equiv, Opposite.op, CategoryTheory.Iso.app
-- 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
P' : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
i : P ≅ P'
⊢ IsSheafFor P R ↔ IsSheafFor P' R

Tactic:
⟨isSheafFor_iso i, isSheafFor_iso i.symm⟩

Premises used: CategoryTheory.Presieve.isSheafFor_iso, Iff.intro, CategoryTheory.Iso.symm
-- 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
P' : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
i : P ≅ P'
hP : IsSeparatedFor P R
x : FamilyOfElements P' R
t₁ t₂ : P'.obj (op X)
ht₁ : x.IsAmalgamation (R := R) t₁
ht₂ : x.IsAmalgamation (R := R) t₂
⊢ t₁ = t₂

Tactic:
simpa using congrArg (i.hom.app _) <| hP (x.map i.inv) _ _ (ht₁.map i.inv) (ht₂.map i.inv)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Presieve.FamilyOfElements.map, CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation.map, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- 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)
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
rw :
  IsSeparatedFor P R ∧
    ∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t
⊢ IsSheafFor P R

Tactic:
rw [← isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]

Premises used: CategoryTheory.Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor
-- 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)
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
left : IsSeparatedFor P R
right : ∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t
⊢ IsSeparatedFor P R ∧
    ∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t

Tactic:
constructor
-- 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)
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation (R := R) t₁
ht₂ : x.IsAmalgamation (R := R) t₂
⊢ t₁ = t₂

Tactic:
hS.isSeparatedFor _ _ _ (isAmalgamation_restrict h x t₁ ht₁)
        (isAmalgamation_restrict h x t₂ ht₂)

Premises used: CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.Presieve.isAmalgamation_restrict
-- 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)
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation (R := R) t₁
ht₂ : x.IsAmalgamation (R := R) t₂
⊢ t₁ = t₂

Tactic:
exact
      hS.isSeparatedFor _ _ _ (isAmalgamation_restrict h x t₁ ht₁)
        (isAmalgamation_restrict h x t₂ ht₂)

Premises used: CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.Presieve.isAmalgamation_restrict
-- 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)
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible (R := R)
h₁ :
  x.IsAmalgamation (R := R) (hS.amalgamate (R := S.arrows) (FamilyOfElements.restrict (R₁ := S.arrows) (R₂ := R) h x) ⋯)
⊢ ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t

Tactic:
use hS.amalgamate _ (hx.restrict h)

Premises used: CategoryTheory.Presieve.IsSheafFor.amalgamate, CategoryTheory.Presieve.FamilyOfElements.Compatible.restrict
-- 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)
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible (R := R)
W : C
j : W ⟶ X
hj : R j
h₁ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ W⦄,
    (Sieve.pullback j S).arrows 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 W))) → (fun (X : Type w) ↦ X) (P.obj (op Y)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
                (hS.amalgamate (R := S.arrows) (FamilyOfElements.restrict (R₁ := S.arrows) (R₂ := R) h x) ⋯) :
              (fun (X : Type w) ↦ X) (P.obj (op W))) :
          (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 W))) → (fun (X : Type w) ↦ X) (P.obj (op Y)))
            (x j hj) :
          (fun (X : Type w) ↦ X) (P.obj (op Y)))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.op) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
      (hS.amalgamate (R := S.arrows) (FamilyOfElements.restrict (R₁ := S.arrows) (R₂ := R) h x) ⋯) =
    x j hj

Tactic:
apply (trans hj).ext

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext
-- 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)
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible (R := R)
W : C
j : W ⟶ X
hj : R j
Y : C
f : Y ⟶ W
hf : (Sieve.pullback j S).arrows f
h₁ :
  x (f ≫ j) ⋯ =
    (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 ≫ j) ⋯)
⊢ 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 W))) → (fun (X : Type w) ↦ X) (P.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map j.op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op W)))
            (hS.amalgamate (R := S.arrows) (FamilyOfElements.restrict (R₁ := S.arrows) (R₂ := R) h x) ⋯) :
          (fun (X : Type w) ↦ X) (P.obj (op W))) :
      (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 W))) → (fun (X : Type w) ↦ X) (P.obj (op Y)))
        (x j hj) :
      (fun (X : Type w) ↦ X) (P.obj (op Y)))

Tactic:
rw [← comp_apply, ← Functor.map_comp, ← op_comp, hS.valid_glue (hx.restrict h) _ hf,
      FamilyOfElements.restrict, ← hx (𝟙 _) f (h _ _ hf) _ (id_comp _)]

Premises used: CategoryTheory.op_comp, CategoryTheory.CategoryStruct.id, CategoryTheory.Presieve.FamilyOfElements.restrict, CategoryTheory.comp_apply, CategoryTheory.Presieve.FamilyOfElements.Compatible.restrict, CategoryTheory.Functor.map_comp, CategoryTheory.Presieve.IsSheafFor.valid_glue, CategoryTheory.Category.id_comp
-- 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)
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible (R := R)
W : C
j : W ⟶ X
hj : R j
Y : C
f : Y ⟶ W
hf : (Sieve.pullback j S).arrows f
⊢ x (f ≫ j) ⋯ =
    (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 ≫ j) ⋯)

Tactic:
simp
-- 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)
S : Sieve.{v₁, u₁} X
R : Presieve.{v₁, u₁} X
h : S.arrows ≤ R
trans : ∀ ⦃Y : C⦄ (f : Y ⟶ X), IsSheafFor P (Sieve.pullback f S).arrows
⊢ IsSheafFor P S.arrows

Tactic:
simpa using trans (𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : FamilyOfElements P (ofArrows X π)
t : P.obj (op B)
⊢ x.IsAmalgamation (R := ofArrows X π) t ↔
    ∀ (i : I),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
          t =
        x (π i) ⋯

Tactic:
⟨fun h i ↦ h _ (ofArrows.mk i), fun h _ f ⟨i⟩ ↦ h i⟩

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, Iff.intro, Eq, DFunLike.coe, _private.0.CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_iff_ofArrows.match_1
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
choose :
  ∀ (i : {Z : C} → (g : Z ⟶ B) → (hg : ofArrows X π g) → I)
    (h : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), X (i g hg) = Z)
    (h' : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), g = eqToHom ⋯ ≫ π (i g hg)),
    ∃ (x' : FamilyOfElements P (ofArrows X π)), ∀ (i : I), x' (π i) ⋯ = x i
⊢ ∃ (x' : FamilyOfElements P (ofArrows X π)), ∀ (i : I), x' (π i) ⋯ = x i

Tactic:
choose i h h' using @ofArrows_surj _ _ _ _ _ π

Premises used: CategoryTheory.Presieve.ofArrows_surj
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
i : {Z : C} → (g : Z ⟶ B) → (hg : ofArrows X π g) → I
h : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), X (i g hg) = Z
h' : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), g = eqToHom ⋯ ≫ π (i g hg)
j : I
rw : π j = 𝟙 (X j) ≫ π j
rw₁ rw₂ : π j = π j
⊢ CategoryStruct.comp (Y := X (i (π j) ⋯)) (eqToHom ⋯) (π (i (π j) ⋯)) = 𝟙 (X j) ≫ π j

Tactic:
rw [← h', 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)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
i : {Z : C} → (g : Z ⟶ B) → (hg : ofArrows X π g) → I
h : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), X (i g hg) = Z
h' : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), g = eqToHom ⋯ ≫ π (i g hg)
j : I
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (𝟙 (X j)))) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) → (fun (X : Type w) ↦ X) (P.obj (op (X j))))
      (x j) =
    x j

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)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
i : {Z : C} → (g : Z ⟶ B) → (hg : ofArrows X π g) → I
h : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), X (i g hg) = Z
h' : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), g = eqToHom ⋯ ≫ π (i g hg)
⊢ ∃ (x' : FamilyOfElements P (ofArrows X π)), ∀ (i : I), x' (π i) ⋯ = x i

Tactic:
exact ⟨fun Y f hf ↦ P.map (eqToHom (h f hf).symm).op (x _),
    fun j ↦ (hx _ j (X j) _ (𝟙 _) <| by rw [← h', id_comp]).trans <| by 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)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
i : I
⊢ hx.familyOfElements (π i) ⋯ = x i

Tactic:
(exists_familyOfElements hx).choose_spec _

Premises used: Exists.choose_spec, CategoryTheory.Presieve.Arrows.Compatible.familyOfElements, CategoryTheory.Presieve.Arrows.Compatible.exists_familyOfElements
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
Z Y_1 : C
i : I
g₁ : Z ⟶ X i
Y : C
j : I
g₂ : Z ⟶ X j
hgf : g₁ ≫ π i = g₂ ≫ π j
⊢ 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 (X i)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (hx.familyOfElements (π i) ⋯) :
      (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 (X j)))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (hx.familyOfElements (π j) ⋯) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))

Tactic:
simp [hx i j Z g₁ g₂ hgf]
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
⊢ IsSheafFor P (ofArrows X π) ↔
    ∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x →
        ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              x i

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

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.IsSheafFor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
refine_1 :
  ∀ (h : IsSheafFor P (ofArrows X π)) (x : (i : I) → P.obj (op (X i))) (hx : Arrows.Compatible P π x),
    ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
      ∀ (i : I),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
            t =
          x i
refine_2 :
  ∀
    (h :
      ∀ (x : (i : I) → P.obj (op (X i))),
        Arrows.Compatible P π x →
          ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
            ∀ (i : I),
              (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                    (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                  t =
                x i)
    (x : FamilyOfElements P (ofArrows X π)) (hx : x.Compatible (R := ofArrows X π)),
    ∃! t : P.obj (op B), x.IsAmalgamation (R := ofArrows X π) t
⊢ IsSheafFor P (ofArrows X π) ↔
    ∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x →
        ∃! t : (fun (X : Type w) ↦ X) (P.obj (op B)),
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op B))) → (fun (X : Type w) ↦ X) (P.obj (op (X i))))
                t =
              x i

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