ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : A<VAR>hX : CategoryTheory.Limits.IsTerminal X<GOAL>CategoryTheory.Presheaf.IsSheaf J ((CategoryTheory.Functor.const Cᵒᵖ).obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>self : CategoryTheory.Sheaf J A<GOAL>CategoryTheory.Presheaf.IsSheaf J self.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<GOAL>∀ (x : CategoryTheory.Sheaf J A), (CategoryTheory.CategoryStruct.id x).val = CategoryTheory.CategoryStruct.id x.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<GOAL>∀ {X Y Z : CategoryTheory.Sheaf J A} (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).val = CategoryTheory.CategoryStruct.comp f.val g.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>X Y : CategoryTheory.Sheaf J A<VAR>x y : X ⟶ Y<VAR>h : x.val = y.val<GOAL>x = y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>self : CategoryTheory.Sheaf J A<GOAL>(CategoryTheory.sheafToPresheaf J A).obj self = self.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<GOAL>∀ {X Y : CategoryTheory.Sheaf J A} (f : X ⟶ Y), (CategoryTheory.sheafToPresheaf J A).map f = f.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<GOAL>∀ {X Y : CategoryTheory.Sheaf J A} (f : (CategoryTheory.sheafToPresheaf J A).obj X ⟶ (CategoryTheory.sheafToPresheaf J A).obj Y), ((CategoryTheory.fullyFaithfulSheafToPresheaf J A).preimage f).val = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>F G : CategoryTheory.Sheaf J A<VAR>f : F ⟶ G<VAR>h : CategoryTheory.Mono f.val<GOAL>CategoryTheory.Mono f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>ℱ : CategoryTheory.Sheaf J A<VAR>E : A<GOAL>(CategoryTheory.sheafOver ℱ E).val = ℱ.val.comp (CategoryTheory.coyoneda.obj (Opposite.op E))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<GOAL>CategoryTheory.Presheaf.IsSheaf J P ↔ CategoryTheory.Presieve.IsSheaf J P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>hS : S ∈ J.sieves X<GOAL>CategoryTheory.Presieve.IsSheafFor P S.arrows
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<GOAL>(CategoryTheory.sheafEquivSheafOfTypes J).unitIso = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Sheaf J (Type w))).obj X)) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<GOAL>(CategoryTheory.sheafEquivSheafOfTypes J).counitIso = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl (({ obj := fun S => { val := S.val, cond := ⋯ }, map := fun {X Y} f => { val := f.val }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun S => { val := S.val, cond := ⋯ }, map := fun {X Y} f => { val := f.val }, map_id := ⋯, map_comp := ⋯ }).obj X)) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : CategoryTheory.Sheaf J (Type w)<GOAL>((CategoryTheory.sheafEquivSheafOfTypes J).functor.obj S).val = S.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<GOAL>∀ {X Y : CategoryTheory.SheafOfTypes J} (f : X ⟶ Y), ((CategoryTheory.sheafEquivSheafOfTypes J).inverse.map f).val = f.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<GOAL>∀ {X Y : CategoryTheory.Sheaf J (Type w)} (f : X ⟶ Y), ((CategoryTheory.sheafEquivSheafOfTypes J).functor.map f).val = f.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : CategoryTheory.SheafOfTypes J<GOAL>((CategoryTheory.sheafEquivSheafOfTypes J).inverse.obj S).val = S.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>CategoryTheory.Preadditive A<VAR>P Q : CategoryTheory.Sheaf J A<VAR>f g : P ⟶ Q<VAR>U : Cᵒᵖ<GOAL>(f + g).val.app U = f.val.app U + g.val.app U
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P : CategoryTheory.Functor Cᵒᵖ A<GOAL>CategoryTheory.Presheaf.IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), Nonempty (CategoryTheory.Limits.IsLimit (S.multifork P))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>∀ (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<GOAL>CategoryTheory.Presheaf.IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), CategoryTheory.IsIso (S.toMultiequalizer P)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>U : C<VAR>R : CategoryTheory.Presieve U<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>CategoryTheory.Limits.HasProducts A<VAR>CategoryTheory.Limits.HasPullbacks C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.forkMap R P) (CategoryTheory.Presheaf.firstMap R P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.forkMap R P) (CategoryTheory.Presheaf.secondMap R P)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A' : Type u₂<VAR>CategoryTheory.Category.{max v₁ u₁, u₂} A'<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P' : CategoryTheory.Functor Cᵒᵖ A'<VAR>CategoryTheory.Limits.HasProducts A'<VAR>CategoryTheory.Limits.HasPullbacks C<GOAL>CategoryTheory.Presheaf.IsSheaf J P' ↔ CategoryTheory.Presheaf.IsSheaf' J P'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>B : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} B<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>s : CategoryTheory.Functor A B<VAR>CategoryTheory.Limits.ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s<VAR>h : CategoryTheory.Presheaf.IsSheaf J (P.comp s)<GOAL>CategoryTheory.Presheaf.IsSheaf J P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>B : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} B<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>s : CategoryTheory.Functor A B<VAR>CategoryTheory.Limits.PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s<VAR>h : CategoryTheory.Presheaf.IsSheaf J P<GOAL>CategoryTheory.Presheaf.IsSheaf J (P.comp s)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>B : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} B<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>s : CategoryTheory.Functor A B<VAR>CategoryTheory.Limits.HasLimitsOfSize.{v₁, max v₁ u₁, v₂, u₂} A<VAR>CategoryTheory.Limits.PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s<VAR>s.ReflectsIsomorphisms<GOAL>CategoryTheory.Presheaf.IsSheaf J P ↔ CategoryTheory.Presheaf.IsSheaf J (P.comp s)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A' : Type u₂<VAR>CategoryTheory.Category.{max v₁ u₁, u₂} A'<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P' : CategoryTheory.Functor Cᵒᵖ A'<VAR>s : CategoryTheory.Functor A' (Type (max v₁ u₁))<VAR>CategoryTheory.Limits.HasLimits A'<VAR>CategoryTheory.Limits.PreservesLimits s<VAR>s.ReflectsIsomorphisms<GOAL>CategoryTheory.Presheaf.IsSheaf J P' ↔ CategoryTheory.Presheaf.IsSheaf J (P'.comp s)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>self : CategoryTheory.Congruence r<VAR>X Y : C<GOAL>Equivalence r
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>self : CategoryTheory.Congruence r<VAR>X Y Z : C<VAR>f f' : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>r f f' → r (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f' g)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>self : CategoryTheory.Congruence r<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g g' : Y ⟶ Z<GOAL>r g g' → r (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f g')
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>r : HomRel C<VAR>a b : C<VAR>m₁ m₂ : a ⟶ b<VAR>h : r m₁ m₂<GOAL>CategoryTheory.Quotient.CompClosure r m₁ m₂
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>r : HomRel C<VAR>a b c : C<VAR>f : a ⟶ b<VAR>g₁ g₂ : b ⟶ c<GOAL>CategoryTheory.Quotient.CompClosure r g₁ g₂ → CategoryTheory.Quotient.CompClosure r (CategoryTheory.CategoryStruct.comp f g₁) (CategoryTheory.CategoryStruct.comp f g₂)
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>r : HomRel C<VAR>a b c : C<VAR>g : b ⟶ c<VAR>f₁ f₂ : a ⟶ b<GOAL>CategoryTheory.Quotient.CompClosure r f₁ f₂ → CategoryTheory.Quotient.CompClosure r (CategoryTheory.CategoryStruct.comp f₁ g) (CategoryTheory.CategoryStruct.comp f₂ g)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>a b c : CategoryTheory.Quotient r<VAR>f : a.as ⟶ b.as<VAR>g : b.as ⟶ c.as<GOAL>CategoryTheory.Quotient.comp r (Quot.mk (CategoryTheory.Quotient.CompClosure r) f) (Quot.mk (CategoryTheory.Quotient.CompClosure r) g) = Quot.mk (CategoryTheory.Quotient.CompClosure r) (CategoryTheory.CategoryStruct.comp f g)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>P : {a b : CategoryTheory.Quotient r} → (a ⟶ b) → Prop<VAR>h : ∀ {x y : C} (f : x ⟶ y), P ((CategoryTheory.Quotient.functor r).map f)<VAR>a b : CategoryTheory.Quotient r<VAR>f : a ⟶ b<GOAL>P f
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>r : HomRel C<VAR>a b : C<VAR>f₁ f₂ : a ⟶ b<VAR>h : r f₁ f₂<GOAL>(CategoryTheory.Quotient.functor r).map f₁ = (CategoryTheory.Quotient.functor r).map f₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>h : CategoryTheory.Congruence r<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>CategoryTheory.Quotient.CompClosure r f g ↔ r f g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>h : CategoryTheory.Congruence r<GOAL>CategoryTheory.Quotient.CompClosure r = r
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>h : CategoryTheory.Congruence r<VAR>X Y : C<VAR>f f' : X ⟶ Y<GOAL>(CategoryTheory.Quotient.functor r).map f = (CategoryTheory.Quotient.functor r).map f' ↔ r f f'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} D<VAR>F : CategoryTheory.Functor C D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<GOAL>(CategoryTheory.Quotient.functor r).comp (CategoryTheory.Quotient.lift r F H) = F
<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_1, u_3} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>CategoryTheory.Category.{u_2, u_4} D<VAR>F : CategoryTheory.Functor C D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>Φ : CategoryTheory.Functor (CategoryTheory.Quotient r) D<VAR>hΦ : (CategoryTheory.Quotient.functor r).comp Φ = F<GOAL>Φ = CategoryTheory.Quotient.lift r F H
<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_1, u_3} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>CategoryTheory.Category.{u_2, u_4} D<VAR>F₁ F₂ : CategoryTheory.Functor (CategoryTheory.Quotient r) D<VAR>h : (CategoryTheory.Quotient.functor r).comp F₁ = (CategoryTheory.Quotient.functor r).comp F₂<GOAL>F₁ = F₂
<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_3, u_4} C<VAR>r : HomRel C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>X : C<GOAL>(CategoryTheory.Quotient.lift.isLift r F H).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_3, u_4} C<VAR>r : HomRel C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>X : C<GOAL>(CategoryTheory.Quotient.lift.isLift r F H).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_2, u_4} C<VAR>r : HomRel C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} D<VAR>F : CategoryTheory.Functor C D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>X : C<GOAL>(CategoryTheory.Quotient.lift r F H).obj ((CategoryTheory.Quotient.functor r).obj X) = F.obj X
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>CategoryTheory.Category.{u_3, u_4} D<VAR>F : CategoryTheory.Functor C D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Quotient.lift r F H).map ((CategoryTheory.Quotient.functor r).map f) = F.map f
<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_1, u_3} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>CategoryTheory.Category.{u_2, u_4} D<VAR>F G : CategoryTheory.Functor (CategoryTheory.Quotient r) D<VAR>τ₁ τ₂ : F ⟶ G<VAR>h : CategoryTheory.whiskerLeft (CategoryTheory.Quotient.functor r) τ₁ = CategoryTheory.whiskerLeft (CategoryTheory.Quotient.functor r) τ₂<GOAL>τ₁ = τ₂
<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_1, u_3} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>CategoryTheory.Category.{u_2, u_4} D<VAR>F G : CategoryTheory.Functor (CategoryTheory.Quotient r) D<VAR>τ : (CategoryTheory.Quotient.functor r).comp F ⟶ (CategoryTheory.Quotient.functor r).comp G<VAR>X : C<GOAL>(CategoryTheory.Quotient.natTransLift r τ).app ((CategoryTheory.Quotient.functor r).obj X) = τ.app X
<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_1, u_3} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>CategoryTheory.Category.{u_2, u_4} D<VAR>F G H : CategoryTheory.Functor (CategoryTheory.Quotient r) D<VAR>τ : (CategoryTheory.Quotient.functor r).comp F ⟶ (CategoryTheory.Quotient.functor r).comp G<VAR>τ' : (CategoryTheory.Quotient.functor r).comp G ⟶ (CategoryTheory.Quotient.functor r).comp H<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Quotient.natTransLift r τ) (CategoryTheory.Quotient.natTransLift r τ') = CategoryTheory.Quotient.natTransLift r (CategoryTheory.CategoryStruct.comp τ τ')
<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_1, u_3} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>CategoryTheory.Category.{u_2, u_4} D<VAR>F : CategoryTheory.Functor (CategoryTheory.Quotient r) D<GOAL>CategoryTheory.Quotient.natTransLift r (CategoryTheory.CategoryStruct.id ((CategoryTheory.Quotient.functor r).comp F)) = CategoryTheory.CategoryStruct.id F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} D<VAR>F G : CategoryTheory.Functor (CategoryTheory.Quotient r) D<VAR>τ : (CategoryTheory.Quotient.functor r).comp F ≅ (CategoryTheory.Quotient.functor r).comp G<GOAL>(CategoryTheory.Quotient.natIsoLift r τ).hom = CategoryTheory.Quotient.natTransLift r τ.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>r : HomRel C<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} D<VAR>F G : CategoryTheory.Functor (CategoryTheory.Quotient r) D<VAR>τ : (CategoryTheory.Quotient.functor r).comp F ≅ (CategoryTheory.Quotient.functor r).comp G<GOAL>(CategoryTheory.Quotient.natIsoLift r τ).inv = CategoryTheory.Quotient.natTransLift r τ.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} E<VAR>F : CategoryTheory.Functor D E<VAR>G : CategoryTheory.Functor E D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>J.HasSheafCompose F<VAR>adj : G ⊣ F<VAR>X : CategoryTheory.Sheaf J E<VAR>Y : CategoryTheory.Sheaf J D<VAR>η : (CategoryTheory.Sheaf.composeAndSheafify J G).obj X ⟶ Y<GOAL>((CategoryTheory.Sheaf.composeEquiv J adj X Y) η).val = ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).homEquiv X.val Y.val) (CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (((CategoryTheory.whiskeringRight Cᵒᵖ E D).obj G).obj X.val)) η.val)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} E<VAR>F : CategoryTheory.Functor D E<VAR>G : CategoryTheory.Functor E D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>J.HasSheafCompose F<VAR>adj : G ⊣ F<VAR>X : CategoryTheory.Sheaf J E<VAR>Y : CategoryTheory.Sheaf J D<VAR>γ : X ⟶ (CategoryTheory.sheafCompose J F).obj Y<GOAL>((CategoryTheory.Sheaf.composeEquiv J adj X Y).symm γ).val = CategoryTheory.sheafifyLift J (((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).homEquiv ((CategoryTheory.sheafToPresheaf J E).obj X) Y.val).symm ((CategoryTheory.sheafToPresheaf J E).map γ)) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} E<VAR>F : CategoryTheory.Functor D E<VAR>G : CategoryTheory.Functor E D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>J.HasSheafCompose F<VAR>adj : G ⊣ F<VAR>X : CategoryTheory.Sheaf J E<GOAL>((CategoryTheory.Sheaf.adjunction J adj).unit.app X).val = ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).homEquiv X.val ((CategoryTheory.presheafToSheaf J D).obj (X.val.comp G)).val) (CategoryTheory.toSheafify J (X.val.comp G))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} E<VAR>F : CategoryTheory.Functor D E<VAR>G : CategoryTheory.Functor E D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>J.HasSheafCompose F<VAR>adj : G ⊣ F<VAR>Y : CategoryTheory.Sheaf J D<GOAL>((CategoryTheory.Sheaf.adjunction J adj).counit.app Y).val = CategoryTheory.sheafifyLift J (((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).homEquiv (Y.val.comp F) Y.val).symm (CategoryTheory.CategoryStruct.id (Y.val.comp F))) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} E<VAR>F : CategoryTheory.Functor D E<VAR>G : CategoryTheory.Functor E D<VAR>adj : G ⊣ F<GOAL>J.PreservesSheafification G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>CategoryTheory.ConcreteCategory D<VAR>J.HasSheafCompose (CategoryTheory.forget D)<VAR>G : CategoryTheory.Functor (Type (max v₁ u₁)) D<VAR>adj : G ⊣ CategoryTheory.forget D<VAR>Y : CategoryTheory.SheafOfTypes J<GOAL>((CategoryTheory.Sheaf.adjunctionToTypes J adj).unit.app Y).val = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).unit.app ((CategoryTheory.sheafOfTypesToPresheaf J).obj Y)) (CategoryTheory.whiskerRight (CategoryTheory.toSheafify J (((CategoryTheory.whiskeringRight Cᵒᵖ (Type (max v₁ u₁)) D).obj G).obj ((CategoryTheory.sheafOfTypesToPresheaf J).obj Y))) (CategoryTheory.forget D))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>CategoryTheory.ConcreteCategory D<VAR>J.HasSheafCompose (CategoryTheory.forget D)<VAR>G : CategoryTheory.Functor (Type (max v₁ u₁)) D<VAR>adj : G ⊣ CategoryTheory.forget D<VAR>X : CategoryTheory.Sheaf J D<GOAL>((CategoryTheory.Sheaf.adjunctionToTypes J adj).counit.app X).val = CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.comp (X.1.associator (CategoryTheory.forget D) G).hom ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).counit.app X.1)) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>F G : CategoryTheory.Functor Cᵒᵖ A<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.presheafHom F G).obj X = ((CategoryTheory.Over.forget (Opposite.unop X)).op.comp F ⟶ (CategoryTheory.Over.forget (Opposite.unop X)).op.comp G)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>F G : CategoryTheory.Functor Cᵒᵖ A<VAR>X Y Z : C<VAR>f : Z ⟶ Y<VAR>g : Y ⟶ X<VAR>h : Z ⟶ X<VAR>w : CategoryTheory.CategoryStruct.comp f g = h<VAR>α : (CategoryTheory.presheafHom F G).obj (Opposite.op X)<GOAL>((CategoryTheory.presheafHom F G).map g.op α).app (Opposite.op (CategoryTheory.Over.mk f)) = α.app (Opposite.op (CategoryTheory.Over.mk h))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>F G : CategoryTheory.Functor Cᵒᵖ A<VAR>X Y : C<VAR>g : Y ⟶ X<VAR>α : (CategoryTheory.presheafHom F G).obj (Opposite.op X)<GOAL>((CategoryTheory.presheafHom F G).map g.op α).app (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id Y))) = α.app (Opposite.op (CategoryTheory.Over.mk g))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>F G : CategoryTheory.Functor Cᵒᵖ A<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.presheafHom F G) S.arrows<VAR>hx : x.Compatible<VAR>y : (CategoryTheory.presheafHom F G).obj (Opposite.op X)<GOAL>x.IsAmalgamation y ↔ ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (Opposite.op (CategoryTheory.Over.mk g)) = (x g hg).app (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id Y)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>F G : CategoryTheory.Functor Cᵒᵖ A<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>hG : ⦃Y : C⦄ → (f : Y ⟶ X) → CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Sieve.pullback f S).arrows.cocone.op)<VAR>x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.presheafHom F G) S.arrows<VAR>hx : x.Compatible<VAR>Y : C<VAR>g : Y ⟶ X<GOAL>∃ φ, ∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (CategoryTheory.CategoryStruct.comp p g)), CategoryTheory.CategoryStruct.comp φ (G.map p.op) = CategoryTheory.CategoryStruct.comp (F.map p.op) ((x (CategoryTheory.CategoryStruct.comp p g) hp).app (Opposite.op (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id Z))))