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
P : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
a : S.functor ⟶ P
rw :
  (∃! b : Functor.obj yoneda 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) ≫
          (Equiv.symm (Iso.homFromEquiv (Iso.app shrinkYonedaIsoYoneda X)) :
              (a : yoneda.obj X ⟶ P) → shrinkYoneda.{v₁, v₁, u₁}.obj X ⟶ P)
            b)
        ((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
⊢ (∃! 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

Tactic:
rw [Equiv.existsUnique_congr_left (shrinkYonedaIsoYoneda.app X).homFromEquiv]

Premises used: CategoryTheory.shrinkYonedaIsoYoneda, Equiv.existsUnique_congr_left, CategoryTheory.Iso.app, CategoryTheory.Iso.homFromEquiv
-- 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₁)
a : S.functor ⟶ P
⊢ (∃! b : Functor.obj yoneda 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) ≫
          (Equiv.symm (Iso.homFromEquiv (Iso.app shrinkYonedaIsoYoneda X)) :
              (a : yoneda.obj X ⟶ P) → shrinkYoneda.{v₁, v₁, u₁}.obj X ⟶ P)
            b)
        ((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

Tactic:
existsUnique_congr fun b ↦ ?_

Premises used: existsUnique_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₁)
a : S.functor ⟶ P
refine :
  ∀ (b : Functor.obj yoneda 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) ≫
          (Equiv.symm (Iso.homFromEquiv (Iso.app shrinkYonedaIsoYoneda X)) :
              (a : yoneda.obj X ⟶ P) → shrinkYoneda.{v₁, v₁, u₁}.obj X ⟶ P)
            b)
        ((Equiv.symm S.shrinkFunctorIsoFunctor.homFromEquiv :
            (a : S.functor ⟶ P) → (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor ⟶ P)
          a) ↔
      S.functorInclusion ≫ b = a
⊢ (∃! b : Functor.obj yoneda 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) ≫
          (Equiv.symm (Iso.homFromEquiv (Iso.app shrinkYonedaIsoYoneda X)) :
              (a : yoneda.obj X ⟶ P) → shrinkYoneda.{v₁, v₁, u₁}.obj X ⟶ P)
            b)
        ((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

Tactic:
refine existsUnique_congr fun b ↦ ?_

Premises used: existsUnique_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₁)
a : S.functor ⟶ P
b : Functor.obj yoneda X ⟶ P
rw :
  (∀ (x : Cᵒᵖ),
      NatTrans.app
          (Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫
            Iso.hom (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) ⋯) ≫ b)
          x =
        (S.shrinkFunctorIsoFunctor.hom ≫ a).app x) ↔
    ∀ (x : Cᵒᵖ), (S.functorInclusion ≫ b).app x = a.app x
⊢ Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫
        Iso.hom (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) ⋯) ≫ b =
      S.shrinkFunctorIsoFunctor.hom ≫ a ↔
    S.functorInclusion ≫ b = a

Tactic:
rw [NatTrans.ext_iff, NatTrans.ext_iff, funext_iff, funext_iff]

Premises used: funext_iff, CategoryTheory.NatTrans.ext_iff
-- 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₁)
a : S.functor ⟶ P
b : Functor.obj yoneda X ⟶ P
a₁ :
  ∀ (a_1 : Cᵒᵖ),
    NatTrans.app
          (Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫
            Iso.hom (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) ⋯) ≫ b)
          a_1 =
        (S.shrinkFunctorIsoFunctor.hom ≫ a).app a_1 ↔
      (S.functorInclusion ≫ b).app a_1 = a.app a_1
⊢ (∀ (x : Cᵒᵖ),
      NatTrans.app
          (Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫
            Iso.hom (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) ⋯) ≫ b)
          x =
        (S.shrinkFunctorIsoFunctor.hom ≫ a).app x) ↔
    ∀ (x : Cᵒᵖ), (S.functorInclusion ≫ b).app x = a.app x

Tactic:
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₁)
a : S.functor ⟶ P
b : Functor.obj yoneda X ⟶ P
a_1 : Cᵒᵖ
a₁ :
  (∀ (x : (Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) (shrinkFunctor.{v₁, v₁, u₁} S)).obj a_1),
      Eq (α := P.obj a_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app
                  (Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫
                    Iso.hom (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) ⋯) ≫ b)
                  a_1) :
              (a : (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor.obj a_1) → P.obj a_1)
            x :
          P.obj a_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((S.shrinkFunctorIsoFunctor.hom ≫ a).app a_1) :
              (a : (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor.obj a_1) → P.obj a_1)
            x :
          P.obj a_1)) ↔
    ∀ (x : S.functor.obj a_1),
      Eq (α := P.obj a_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((S.functorInclusion ≫ b).app a_1) :
              (a : S.functor.obj a_1) → P.obj a_1)
            x :
          P.obj a_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (a.app a_1) : (a : S.functor.obj a_1) → P.obj a_1) x : P.obj a_1)
⊢ NatTrans.app
        (Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫
          Iso.hom (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) ⋯) ≫ b)
        a_1 =
      (S.shrinkFunctorIsoFunctor.hom ≫ a).app a_1 ↔
    (S.functorInclusion ≫ b).app a_1 = a.app a_1

Tactic:
rw [ConcreteCategory.hom_ext_iff, ConcreteCategory.hom_ext_iff]

Premises used: CategoryTheory.ConcreteCategory.hom_ext_iff
-- 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₁)
a : S.functor ⟶ P
b : Functor.obj yoneda X ⟶ P
a_1 : Cᵒᵖ
a_2 : unop a_1 ⟶ X
h : S.arrows a_2
⊢ (↑((Equiv.subtypeEquiv (p :=
              Membership.mem (γ := Set (Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) a_1))
                {f : Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) a_1 |
                  S.arrows (Y := unop a_1)
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj a_1) → unop a_1 ⟶ X) f)})
              (q := S.arrows) shrinkYonedaObjObjEquiv ⋯ :
            (a :
                { x : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj a_1 //
                  S.arrows
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj a_1) → unop a_1 ⟶ X) x) }) →
              { g : unop a_1 ⟶ X // S.arrows g })
          (Subtype.mk (p := fun (a : Functor.obj (Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) a_1) ↦
            S.arrows (Y := unop a_1)
              ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj a_1) → unop a_1 ⟶ X) a))
            ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop a_1 ⟶ X) → (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj a_1) a_2)
            ⋯)) :
      unop a_1 ⟶ X) =
    a_2

Tactic:
simp [Equiv.subtypeEquiv]

Premises used: Equiv.subtypeEquiv
-- 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₁)
h : IsSheafFor P S.arrows
f : S.functor ⟶ P
⊢ S.functorInclusion ≫ h.extend f = f

Tactic:
(isSheafFor_iff_yonedaSheafCondition.1 h f).exists.choose_spec

Premises used: Exists.choose_spec, ExistsUnique.exists, CategoryTheory.Presieve.IsSheafFor.extend, CategoryTheory.Presieve.isSheafFor_iff_yonedaSheafCondition, Iff.mp
-- 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₁)
h : IsSheafFor P S.arrows
f : S.functor ⟶ P
t : Functor.obj yoneda X ⟶ P
ht : S.functorInclusion ≫ t = f
⊢ t = h.extend f

Tactic:
(isSheafFor_iff_yonedaSheafCondition.1 h f).unique ht (h.functorInclusion_comp_extend f)

Premises used: CategoryTheory.Presieve.isSheafFor_iff_yonedaSheafCondition, CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend, Iff.mp, ExistsUnique.unique
-- 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₁)
h : IsSheafFor P S.arrows
t₁ t₂ : Functor.obj yoneda X ⟶ P
ht : S.functorInclusion ≫ t₁ = S.functorInclusion ≫ t₂
⊢ t₁ = t₂

Tactic:
(h.unique_extend t₁ ht).trans (h.unique_extend t₂ rfl).symm

Premises used: CategoryTheory.Presieve.IsSheafFor.unique_extend, Eq.symm, rfl, 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
rw :
  (∀ (x : FamilyOfElements P R),
      (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation (R := R) t₁ → x.IsAmalgamation (R := R) t₂ → t₁ = t₂) ∧
        (x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t)) ↔
    IsSheafFor P R
⊢ (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, ← forall_and]

Premises used: CategoryTheory.Presieve.IsSeparatedFor, forall_and
-- 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 :
  ∀ (a : FamilyOfElements P R),
    (∀ (t₁ t₂ : P.obj (op X)), a.IsAmalgamation (R := R) t₁ → a.IsAmalgamation (R := R) t₂ → t₁ = t₂) ∧
        (a.Compatible (R := R) → ∃ (t : P.obj (op X)), a.IsAmalgamation (R := R) t) ↔
      a.Compatible (R := R) → ∃! t : P.obj (op X), a.IsAmalgamation (R := R) t
⊢ (∀ (x : FamilyOfElements P R),
      (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation (R := R) t₁ → x.IsAmalgamation (R := R) t₂ → t₁ = t₂) ∧
        (x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t)) ↔
    IsSheafFor P R

Tactic:
apply forall_congr'

Premises used: forall_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 R
h :
  (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation (R := R) t₁ → x.IsAmalgamation (R := R) t₂ → t₁ = t₂) ∧
      (x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t) →
    x.Compatible (R := R) → ∃! t : P.obj (op X), x.IsAmalgamation (R := R) t
h₁ :
  (x.Compatible (R := R) → ∃! t : P.obj (op X), x.IsAmalgamation (R := R) t) →
    (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation (R := R) t₁ → x.IsAmalgamation (R := R) t₂ → t₁ = t₂) ∧
      (x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t)
⊢ (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation (R := R) t₁ → x.IsAmalgamation (R := R) t₂ → t₁ = t₂) ∧
      (x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t) ↔
    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
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
z :
  (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation (R := R) t₁ → x.IsAmalgamation (R := R) t₂ → t₁ = t₂) ∧
    (x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t)
hx : x.Compatible (R := R)
⊢ ∃! t : P.obj (op X), x.IsAmalgamation (R := R) t

Tactic:
existsUnique_of_exists_of_unique (z.2 hx) z.1

Premises used: existsUnique_of_exists_of_unique, And.right, And.left
-- 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
z :
  (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation (R := R) t₁ → x.IsAmalgamation (R := R) t₂ → t₁ = t₂) ∧
    (x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t)
hx : x.Compatible (R := R)
⊢ ∃! t : P.obj (op X), x.IsAmalgamation (R := R) t

Tactic:
exact existsUnique_of_exists_of_unique (z.2 hx) z.1

Premises used: existsUnique_of_exists_of_unique, And.right, And.left
-- 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
h : x.Compatible (R := R) → ∃! t : P.obj (op X), x.IsAmalgamation (R := R) t
⊢ (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation (R := R) t₁ → x.IsAmalgamation (R := R) t₂ → t₁ = t₂) ∧
    (x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t)

Tactic:
⟨?_, ExistsUnique.exists ∘ h⟩

Premises used: ExistsUnique.exists, Function.comp, And.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)
X : C
R : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
h : x.Compatible (R := R) → ∃! t : P.obj (op X), x.IsAmalgamation (R := R) t
h₁ : ∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation (R := R) t₁ → x.IsAmalgamation (R := R) t₂ → t₁ = t₂
⊢ (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation (R := R) t₁ → x.IsAmalgamation (R := R) t₂ → t₁ = t₂) ∧
    (x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t)

Tactic:
refine ⟨?_, ExistsUnique.exists ∘ 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 R
h : x.Compatible (R := R) → ∃! t : P.obj (op X), x.IsAmalgamation (R := R) t
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation (R := R) t₁
ht₂ : x.IsAmalgamation (R := R) t₂
apply : x.Compatible (R := R)
⊢ t₁ = t₂

Tactic:
apply (h _).unique ht₁ ht₂

Premises used: ExistsUnique.unique
-- 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
h : x.Compatible (R := R) → ∃! t : P.obj (op X), x.IsAmalgamation (R := R) t
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation (R := R) t₁
ht₂ : x.IsAmalgamation (R := R) t₂
⊢ x.Compatible (R := R)

Tactic:
is_compatible_of_exists_amalgamation x ⟨_, ht₂⟩

Premises used: CategoryTheory.Presieve.is_compatible_of_exists_amalgamation, Exists.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)
X : C
R : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
h : x.Compatible (R := R) → ∃! t : P.obj (op X), x.IsAmalgamation (R := R) t
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation (R := R) t₁
ht₂ : x.IsAmalgamation (R := R) t₂
⊢ x.Compatible (R := R)

Tactic:
exact is_compatible_of_exists_amalgamation x ⟨_, ht₂⟩

Premises used: CategoryTheory.Presieve.is_compatible_of_exists_amalgamation, Exists.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)
X : C
R : Presieve.{v₁, u₁} X
t : IsSeparatedFor P R
rw :
  (∀ (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
⊢ (∀ (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
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
t : IsSeparatedFor P R
⊢ (∀ (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:
And.intro t

Premises used: And.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)
X : C
R : Presieve.{v₁, u₁} X
t : IsSeparatedFor P R
⊢ (∀ (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:
exact And.intro t

Premises used: And.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)
X : C
R : Presieve.{v₁, u₁} X
⊢ IsSheafFor P R → IsSeparatedFor P R

Tactic:
fun q =>
  (isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor.2 q).1

Premises used: Iff.mpr, CategoryTheory.Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor, And.left
-- 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
t : IsSheafFor P R
x : FamilyOfElements P R
hx : x.Compatible (R := R)
⊢ x.IsAmalgamation (R := R) (t.amalgamate (R := R) x hx)

Tactic:
(t x hx).exists.choose_spec

Premises used: Exists.choose_spec, ExistsUnique.exists, CategoryTheory.Presieve.IsSheafFor.amalgamate
-- 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
t : IsSheafFor P R
x : FamilyOfElements P R
hx : x.Compatible (R := R)
f : Y ⟶ X
Hf : R f
⊢ (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.amalgamate (R := R) x hx) =
    x f Hf

Tactic:
t.isAmalgamation hx f Hf

Premises used: CategoryTheory.Presieve.IsSheafFor.isAmalgamation
-- 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
rw :
  (IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t) ↔
    IsSheafFor P (generate R).arrows
⊢ IsSheafFor P R ↔ IsSheafFor P (generate R).arrows

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
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
rw :
  (IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t) ↔
    IsSeparatedFor P (generate R).arrows ∧
      ∀ (x : FamilyOfElements P (generate R).arrows),
        x.Compatible (R := (generate R).arrows) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := (generate R).arrows) t
⊢ (IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t) ↔
    IsSheafFor P (generate R).arrows

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
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
rw :
  (IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t) ↔
    IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P (generate R).arrows),
        x.Compatible (R := (generate R).arrows) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := (generate R).arrows) t
⊢ (IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t) ↔
    IsSeparatedFor P (generate R).arrows ∧
      ∀ (x : FamilyOfElements P (generate R).arrows),
        x.Compatible (R := (generate R).arrows) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := (generate R).arrows) t

Tactic:
rw [← isSeparatedFor_iff_generate]

Premises used: CategoryTheory.Presieve.isSeparatedFor_iff_generate
-- 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
apply :
  (∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t) ↔
    ∀ (x : FamilyOfElements P (generate R).arrows),
      x.Compatible (R := (generate R).arrows) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := (generate R).arrows) t
⊢ (IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t) ↔
    IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P (generate R).arrows),
        x.Compatible (R := (generate R).arrows) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := (generate R).arrows) t

Tactic:
apply and_congr (Iff.refl _)

Premises used: Iff.refl, and_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
mp :
  (∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t) →
    ∀ (x : FamilyOfElements P (generate R).arrows),
      x.Compatible (R := (generate R).arrows) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := (generate R).arrows) t
mpr :
  (∀ (x : FamilyOfElements P (generate R).arrows),
      x.Compatible (R := (generate R).arrows) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := (generate R).arrows) t) →
    ∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t
⊢ (∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t) ↔
    ∀ (x : FamilyOfElements P (generate R).arrows),
      x.Compatible (R := (generate R).arrows) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := (generate R).arrows) t

Tactic:
constructor