awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
f : Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⟶ F
g : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F
h :
  ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
    Eq (α := F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1.op) : (a : F.obj (op X)) → F.obj (op Y))
          ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) g : F.obj (op X)) :
        F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
            (a :
                { x : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y) //
                  S.arrows
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) →
              F.obj (op Y))
          (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)) ↦
              S.arrows (Y := Y)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x))
              ((Equiv.symm shrinkYonedaObjObjEquiv : (a : Y ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) f_1) ⋯ :
            { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y) //
              S.arrows (Y := Y)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) :
        F.obj (op Y))
⊢ Subfunctor.ι (shrinkFunctor.{w, v₁, u₁} S) ≫ g = f
have refine_2 : ∀ (Y : Cᵒᵖ) (u : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y)
  (hu :
    Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
      (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) u),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Subfunctor.ι (shrinkFunctor.{w, v₁, u₁} S) ≫ g) Y))
      (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y) ↦
        Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
          (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) x)
        u hu) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y)).toFun
      (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y) ↦
        Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
          (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) x)
        u hu)
Tactic: ext Y ⟨u, hu⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
f : Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⟶ F
g : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F
h :
  ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
    Eq (α := F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1.op) : (a : F.obj (op X)) → F.obj (op Y))
          ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) g : F.obj (op X)) :
        F.obj (op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op Y)) :
            (a :
                { x : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y) //
                  S.arrows
                    ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) →
              F.obj (op Y))
          (Subtype.mk (p := fun (x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y)) ↦
              S.arrows (Y := Y)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x))
              ((Equiv.symm shrinkYonedaObjObjEquiv : (a : Y ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) f_1) ⋯ :
            { x : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) (op Y) //
              S.arrows (Y := Y)
                ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op Y)) → Y ⟶ X) x) }) :
        F.obj (op Y))
Y : Cᵒᵖ
u : Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y
hu :
  Membership.mem (γ := Set (Functor.obj.{v₁, w, u₁, w + 1} (Functor.obj shrinkYoneda.{w, v₁, u₁} X) Y))
    (Subfunctor.obj (shrinkFunctor.{w, v₁, u₁} S) Y) u
⊢ u =
    (Equiv.symm shrinkYonedaObjObjEquiv : (a : unop Y ⟶ X) → (shrinkYoneda.{w, v₁, u₁}.obj X).obj (op (unop Y)))
      ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y) → unop Y ⟶ X) u)
have h₁ : u = u
Tactic: rw! [Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
F : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
⊢ IsSheafFor F S.arrows ↔
    Function.Bijective (β :=
      Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{w, v₁, u₁} X) (shrinkFunctor.{w, v₁, u₁} S) ⟶ F)
      fun (g : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F) ↦ Subfunctor.ι (shrinkFunctor.{w, v₁, u₁} S) ≫ g
have simp : (∀ (x : FamilyOfElements F S.arrows),
    x.Compatible (R := S.arrows) → ∃! t : F.obj (op X), x.IsAmalgamation (R := S.arrows) t) ↔
  ∀ (a : FamilyOfElements F S.arrows) (b : a.Compatible (R := S.arrows)),
    ∃! a_1 : Functor.obj shrinkYoneda.{w, v₁, u₁} X ⟶ F,
      FamilyOfElements.IsAmalgamation.{w, v₁, u₁} (P := F) (R := S.arrows)
        (↑((shrinkFunctorHomEquiv :
                (a : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F) → { x : FamilyOfElements F S.arrows // x.Compatible })
              ((Equiv.symm shrinkFunctorHomEquiv :
                  (a : { x : FamilyOfElements F S.arrows // x.Compatible }) →
                    (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F)
                (Subtype.mk (p := fun (a : FamilyOfElements F S.arrows) ↦ a.Compatible (R := S.arrows)) a b))) :
          FamilyOfElements F S.arrows)
        ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) a_1)
Tactic: simp only [IsSheafFor, Function.bijective_iff_existsUnique,
    shrinkFunctor_ι_comp_eq_iff_isAmalgamation, shrinkFunctorHomEquiv.forall_congr_left,
    Subtype.forall]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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₁)
⊢ IsSheafFor P S.arrows ↔ YonedaSheafCondition P S
have rw : (∀ (b : S.functor ⟶ P),
    ∃! a : Functor.obj shrinkYoneda.{v₁, v₁, u₁} X ⟶ P,
      Eq (α := Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) (shrinkFunctor.{v₁, v₁, u₁} S) ⟶ P)
        (Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫ a)
        ((Equiv.symm S.shrinkFunctorIsoFunctor.homFromEquiv :
            (a : S.functor ⟶ P) → (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor ⟶ P)
          b)) ↔
  ∀ (f : S.functor ⟶ P), ∃! g : Functor.obj yoneda X ⟶ P, S.functorInclusion ≫ g = f
Tactic: rw [isSheafFor_iff_bijective_shrinkFunctor_ι_comp, YonedaSheafCondition,
    Function.bijective_iff_existsUnique,
    Equiv.forall_congr_left S.shrinkFunctorIsoFunctor.homFromEquiv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
S : Sieve.{v₁, u₁} X
P : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
⊢ (∀ (b : S.functor ⟶ P),
      ∃! a : Functor.obj shrinkYoneda.{v₁, v₁, u₁} X ⟶ P,
        Eq (α := Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) (shrinkFunctor.{v₁, v₁, u₁} S) ⟶ P)
          (Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫ a)
          ((Equiv.symm S.shrinkFunctorIsoFunctor.homFromEquiv :
              (a : S.functor ⟶ P) → (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor ⟶ P)
            b)) ↔
    ∀ (f : S.functor ⟶ P), ∃! g : Functor.obj yoneda X ⟶ P, S.functorInclusion ≫ g = f
have refine : ∀ (a : S.functor ⟶ P),
  (∃! a_1 : Functor.obj shrinkYoneda.{v₁, v₁, u₁} X ⟶ P,
      Eq (α := Subfunctor.toFunctor (F := Functor.obj shrinkYoneda.{v₁, v₁, u₁} X) (shrinkFunctor.{v₁, v₁, u₁} S) ⟶ P)
        (Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫ a_1)
        ((Equiv.symm S.shrinkFunctorIsoFunctor.homFromEquiv :
            (a : S.functor ⟶ P) → (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor ⟶ P)
          a)) ↔
    ∃! g : Functor.obj yoneda X ⟶ P, S.functorInclusion ≫ g = a
Tactic: refine forall_congr' fun a ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
⊢ (∃! 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
have 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
Tactic: rw [Equiv.existsUnique_congr_left (shrinkYonedaIsoYoneda.app X).homFromEquiv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
have 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
Tactic: refine existsUnique_congr fun b ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
⊢ 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
have rw : (∀ (x : Cᵒᵖ),
    NatTrans.app
        (Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫
          Iso.hom (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) sorry) ≫ b)
        x =
      (S.shrinkFunctorIsoFunctor.hom ≫ a).app x) ↔
  ∀ (x : Cᵒᵖ), (S.functorInclusion ≫ b).app x = a.app x
Tactic: rw [NatTrans.ext_iff, NatTrans.ext_iff, funext_iff, funext_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
⊢ (∀ (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
have a₁ : ∀ (a_1 : Cᵒᵖ),
  NatTrans.app
        (Subfunctor.ι (shrinkFunctor.{v₁, v₁, u₁} S) ≫
          Iso.hom (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) sorry) ≫ b)
        a_1 =
      (S.shrinkFunctorIsoFunctor.hom ≫ a).app a_1 ↔
    (S.functorInclusion ≫ b).app a_1 = a.app a_1
Tactic: congr!
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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ᵒᵖ
⊢ 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
have 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) sorry) ≫ 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)
Tactic: rw [ConcreteCategory.hom_ext_iff, ConcreteCategory.hom_ext_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
⊢ (IsSeparatedFor P R ∧
      ∀ (x : FamilyOfElements P R), x.Compatible (R := R) → ∃ (t : P.obj (op X)), x.IsAmalgamation (R := R) t) ↔
    IsSheafFor P R
have 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
Tactic: rw [IsSeparatedFor, ← forall_and]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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₁ 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
have 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
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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₁ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
⊢ (∀ (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
have 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: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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)
have h₁ : ∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation (R := R) t₁ → x.IsAmalgamation (R := R) t₂ → t₁ = t₂
Tactic: refine ⟨?_, ExistsUnique.exists ∘ h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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₂
⊢ t₁ = t₂
have apply : x.Compatible (R := R)
Tactic: apply (h _).unique ht₁ ht₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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) →
    IsSheafFor P R
have 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
Tactic: rw [← isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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 ↔ IsSheafFor P (generate R).arrows
have 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
Tactic: rw [← isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
⊢ (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
have 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
Tactic: rw [← isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
⊢ (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
have 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
Tactic: rw [← isSeparatedFor_iff_generate]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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
⊢ (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
have 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
Tactic: apply and_congr (Iff.refl _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
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), 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
have 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
Tactic: constructor